#!/usr/bin/env python3
# -----------------------------------------------------------------------------
# reputation_gate_smt.py
#
# SMT proof (z3) of the M1-FIX authorization + delta-clamp invariant of
# AereReputationRegistry8004, the ERC-8004 Reputation adapter over the LIVE
# AereAIReputation. Plus load-bearing NEGATIVE CONTROLS for the author gate (the
# M1 bug: anyone could drive a score) and for the delta clamp.
#
# Contract: contracts/contracts/erc8004/AereReputationRegistry8004.sol
#
# Because every caller of this adapter collapses into ONE on-chain attestor identity
# (the adapter) on the live AereAIReputation, an UNGATED write path (the pre-fix M1
# state) would let ANY address inflate or tank any agent's reputation. The M1 fix
# gates giveFeedback to an owner-curated allowlist AND keeps the existing delta clamp,
# so a forwarded attestation is authorized AND a bounded unit step, never an arbitrary
# value set. giveFeedback fail-closes on each guard (else revert, forwards nothing):
#   G0 author gate (M1 fix):  isAuthorizedFeedbackAuthor[msg.sender]  (NotAuthorizedFeedbackAuthor)
#   G1 agent registered:      IDENTITY.isRegistered(agentId)         (AgentNotRegistered)
#   G2 delta clamp:           -1 <= delta <= 1                       (InvalidDelta)
#   G3 adapter is attestor:   REPUTATION.isAttestor(this)            (AdapterNotAttestor)
# then forwards REPUTATION.attest(operator, key, delta, ...).
#
#   FORWARD-SAFETY INVARIANT (the M1 target):
#     a forwarded attestation happens  =>  (author is authorized) AND (delta in {-1,0,+1})
#
#   So the ONLY way this adapter moves an agent's live reputation is an authorized
#   author submitting a clamped unit delta; the owner curates WHO may write but can
#   neither set a reputation value directly nor exceed the clamp every author is held
#   to, and moves no funds.
#
# Method: model the fail-closed guards as first-order constraints and prove each
# property by asserting its NEGATION under the guards (UNSAT). Each NEG-CTRL removes
# exactly one guard and shows the corresponding attack becomes SAT.
#
# HONEST SCOPE / OVERLAP. The authorization half of this property is also exercised
# directly by the Hardhat test "gates giveFeedback to owner-authorized feedback
# authors (M1)" in test/erc8004-adapters.test.js. The z3 value-add here is (a) proving
# the COMPOSITE invariant (authorized AND unit-clamped) is the only way a forward can
# occur, and (b) the firing negative control that reproduces the exact M1 "anyone
# drives the score" bug, showing the gate is load-bearing. The live AereAIReputation
# computes the actual score FROM the delta; this model bounds only what the adapter
# forwards (an authorized, clamped delta), not the live contract's internal score
# formula. Application-layer, no funds, consensus classical ECDSA. DESIGN-level logic,
# NOT the compiled EVM bytecode.
# -----------------------------------------------------------------------------
from z3 import Int, Bool, Solver, And, Or, Not, Implies, sat, unsat

results = []
def check(name, s, expect_unsat=True, kind="PROOF"):
    r = s.check()
    if expect_unsat:
        ok = (r == unsat); tag = "PROVED" if ok else "FAILED"
    else:
        ok = (r == sat);   tag = "CEX-FOUND" if ok else "FAILED"
    results.append((name, tag, ok, kind))
    print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})")
    if r == sat:
        m = s.model()
        print("             witness:", {str(d): m[d] for d in m.decls()})
    return ok

def clamped(delta):
    """InvalidDelta guard: delta in {-1, 0, +1}."""
    return And(delta >= -1, delta <= 1)

def forward_ok(authorized, registered, delta, adapterIsAttestor):
    """giveFeedback's fail-closed guards G0..G3. A forwarded attest happens iff all hold."""
    return And(authorized, registered, clamped(delta), adapterIsAttestor)

print("### AereReputationRegistry8004 -- M1 AUTHOR GATE + DELTA CLAMP (forward-safety)\n")

# ---- G0  AUTHORIZATION REQUIRED (M1 fix): a forwarded attestation requires an
#      authorized author. Negation: a forward happens with an unauthorized caller. UNSAT.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
s.add(forward_ok(authorized, registered, delta, adapterIsAttestor))
s.add(Not(authorized))                                   # NEGATION: unauthorized caller moved a score
check("G0 only an authorized feedback author can move a score (M1 gate)", s)

# ---- G2  DELTA CLAMP: a forwarded attestation carries delta in {-1,0,+1}, so no
#      author (nor the owner) can forge an arbitrary reputation move. Negation: a
#      forward happens with an out-of-range delta. UNSAT.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
s.add(forward_ok(authorized, registered, delta, adapterIsAttestor))
s.add(Or(delta < -1, delta > 1))                         # NEGATION: arbitrary delta forwarded
check("G2 a forwarded delta is clamped to {-1,0,+1} (no arbitrary value set)", s)

# ---- M1 COMPOSITE forward-safety: any score move through the adapter is BOTH by an
#      authorized author AND a clamped unit step. Negation: a forward happens yet the
#      author is unauthorized OR the delta is out of range. UNSAT.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
s.add(forward_ok(authorized, registered, delta, adapterIsAttestor))
s.add(Or(Not(authorized), delta < -1, delta > 1))        # NEGATION
check("M1 a score move requires (authorized author) AND (clamped unit delta)", s)

# ---- G1  REGISTERED AGENT required (fail-closed): a forward requires a registered
#      agentId. Negation: a forward about an unregistered agent. UNSAT.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
s.add(forward_ok(authorized, registered, delta, adapterIsAttestor))
s.add(Not(registered))                                   # NEGATION: feedback about an unknown agent
check("G1 feedback requires a registered agent (fail-closed)", s)

# ---- G3  ADAPTER-IS-ATTESTOR required (fail-closed): a forward requires this adapter
#      to be an authorized attestor on the live reputation. Negation: forward without
#      the adapter being an attestor. UNSAT.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
s.add(forward_ok(authorized, registered, delta, adapterIsAttestor))
s.add(Not(adapterIsAttestor))                            # NEGATION: writes through a non-attestor adapter
check("G3 forwarding requires the adapter to be a live attestor (fail-closed)", s)

# ============================ NEGATIVE CONTROLS ==============================

# ---- NEG-CTRL 1 (drop the author gate -> the M1 bug): an UNGATED giveFeedback (the
#      pre-fix state) lets ANY caller drive an agent's score. Since every caller
#      collapses into the single adapter attestor, an unauthorized address writes.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
# BUG: the G0 author gate is removed; a forward needs only registered + clamp + attestor.
buggy_forward = And(registered, clamped(delta), adapterIsAttestor)
s.add(buggy_forward)
s.add(Not(authorized))                                   # an UNauthorized caller still drives the score
check("no-author-gate adapter CAN let anyone drive an agent's score (reproduces M1)", s,
      expect_unsat=False, kind="NEG-CTRL")

# ---- NEG-CTRL 2 (drop the delta clamp): a BUGGY adapter without the {-1,0,+1} clamp
#      forwards an arbitrary delta, letting even an authorized author forge a large
#      reputation swing in one call. z3 finds the out-of-range delta.
s = Solver()
authorized, registered, adapterIsAttestor = Bool('authorized'), Bool('registered'), Bool('adapterIsAttestor')
delta = Int('delta')
# BUG: the G2 clamp is removed; a forward needs only author + registered + attestor.
buggy_forward = And(authorized, registered, adapterIsAttestor)
s.add(buggy_forward)
s.add(delta > 1)                                         # an arbitrary large delta is forwarded
check("no-delta-clamp adapter CAN forward an arbitrary reputation delta", s,
      expect_unsat=False, kind="NEG-CTRL")

# ------------------------------------------------------------------------------
print("\n=== SUMMARY ===")
allok = True
for name, tag, ok, kind in results:
    print(f"  {tag:9} [{kind}]  {name}")
    allok = allok and ok
print()
if allok:
    print("AereReputationRegistry8004 M1 forward-safety:")
    print("  PROVED -- a forwarded attestation requires an authorized feedback author (G0, the M1")
    print("  fix), a delta clamped to {-1,0,+1} (G2, no arbitrary value set), a registered agent")
    print("  (G1) and the adapter being a live attestor (G3); the composite M1 property holds: the")
    print("  ONLY way to move an agent's score through the adapter is an authorized author with a")
    print("  clamped unit delta. Two NEG-CTRLs fire: dropping the author gate reproduces the exact")
    print("  M1 bug (anyone drives the score), and dropping the clamp lets an arbitrary delta")
    print("  through, so both guards are load-bearing.")
    print("  OVERLAP / SCOPE (honest): the authorization half is also covered directly by the")
    print("  Hardhat test 'gates giveFeedback to owner-authorized feedback authors (M1)'; the z3")
    print("  value-add is the composite invariant and the firing non-vacuity control. The owner")
    print("  curates WHO may write but cannot set a reputation value or exceed the clamp. The live")
    print("  AereAIReputation computes the score FROM the delta; this model bounds what the adapter")
    print("  forwards (authorized + clamped), not the live contract's score formula. Application-")
    print("  layer, no funds, consensus classical ECDSA. DESIGN-level guard logic, not the bytecode.")
else:
    print("  NOT fully established (see FAILED / unexpected CEX above).")
import sys
sys.exit(0 if allok else 1)