Proven in Lean 4Proven in Lean 4

/-
  Trust Receipt: the sign-off protocol, proven.

  The app's sign-off state machine (src/domain/signoff.machine.ts) is modelled here.
  The theorems hold for every possible sequence of events, of any length,
  not only for the states that the bounded machine checks explore.

  Check: nix shell nixpkgs#lean4 -c lean lean/TrustReceipt.lean
-/

namespace TrustReceipt

inductive Actor where
  | ai
  | human
  deriving DecidableEq, Repr

inductive Decision where
  | accept
  | change
  deriving DecidableEq, Repr

inductive Action where
  | setOwner (name : String)
  | markRead (hunk : String) (read : Bool)
  | decide (claim : String) (decision : Decision)
  | acceptRisk (accepted : Bool)
  | sign
  | reopen

structure Event where
  actor : Actor
  action : Action

structure Receipt where
  owner : String
  read : List String
  decided : List String
  riskAccepted : Bool
  requiredHunks : List String
  requiredClaims : List String
  signed : Bool

/-- Ready to sign: a named owner, every flagged hunk read, every refused claim decided, the residual risk accepted. -/
def Ready (r : Receipt) : Prop :=
  r.owner.length > 1 ∧
  r.riskAccepted = true ∧
  (∀ h ∈ r.requiredHunks, h ∈ r.read) ∧
  (∀ c ∈ r.requiredClaims, c ∈ r.decided)

instance (r : Receipt) : Decidable (Ready r) := by
  unfold Ready
  infer_instance

/-- What a human action does while the receipt is still a draft. -/
def apply (r : Receipt) : Action → Receipt
  | .setOwner name => { r with owner := name }
  | .markRead hunk true => { r with read := hunk :: r.read }
  | .markRead hunk false => { r with read := r.read.filter (fun h => h != hunk) }
  | .decide claim _ =>
      if claim ∈ r.requiredClaims then { r with decided := claim :: r.decided } else r
  | .acceptRisk accepted => { r with riskAccepted := accepted }
  | .sign => if Ready r then { r with signed := true } else r
  | .reopen => r

/-- One event. The AI has no action in the protocol. A signed receipt only reopens. -/
def step (r : Receipt) (e : Event) : Receipt :=
  match e.actor with
  | .ai => r
  | .human =>
      if r.signed then
        match e.action with
        | .reopen => { r with signed := false }
        | _ => r
      else apply r e.action

def run (r : Receipt) : List Event → Receipt
  | [] => r
  | e :: es => run (step r e) es

/-- A fresh draft for one review. -/
def draft (requiredHunks requiredClaims : List String) : Receipt :=
  { owner := "", read := [], decided := [], riskAccepted := false,
    requiredHunks, requiredClaims, signed := false }

def Safe (r : Receipt) : Prop := r.signed = true → Ready r

theorem apply_keeps_signed (r : Receipt) (a : Action) (h : a ≠ .sign) :
    (apply r a).signed = r.signed := by
  cases a with
  | setOwner => rfl
  | markRead hunk read => cases read <;> rfl
  | decide claim d =>
      simp only [apply]
      split <;> rfl
  | acceptRisk => rfl
  | sign => exact absurd rfl h
  | reopen => rfl

theorem apply_safe (r : Receipt) (a : Action) (hs : r.signed = false) : Safe (apply r a) := by
  intro hsigned
  by_cases ha : a = .sign
  · subst ha
    simp only [apply] at hsigned ⊢
    by_cases hr : Ready r
    · simp only [hr, ite_true] at hsigned ⊢
      exact hr
    · simp only [hr, ite_false] at hsigned
      rw [hs] at hsigned
      contradiction
  · rw [apply_keeps_signed r a ha, hs] at hsigned
    contradiction

theorem step_draft (r : Receipt) (a : Action) (hf : r.signed = false) :
    step r ⟨.human, a⟩ = apply r a := by
  simp [step, hf]

theorem step_safe (r : Receipt) (e : Event) (h : Safe r) : Safe (step r e) := by
  cases e with
  | mk actor action =>
    cases actor with
    | ai => exact h
    | human =>
      by_cases hs : r.signed = true
      · cases action with
        | reopen =>
            intro hsigned
            simp [step, hs] at hsigned
        | setOwner => simpa [step, hs] using h
        | markRead => simpa [step, hs] using h
        | decide => simpa [step, hs] using h
        | acceptRisk => simpa [step, hs] using h
        | sign => simpa [step, hs] using h
      · have hf : r.signed = false := by simpa using hs
        rw [step_draft r action hf]
        exact apply_safe r action hf

theorem run_safe (r : Receipt) (es : List Event) (h : Safe r) : Safe (run r es) := by
  induction es generalizing r with
  | nil => exact h
  | cons e es ih => exact ih (step r e) (step_safe r e h)

/-- Main theorem. From any draft, after any sequence of events, a signed receipt has a named
    owner, every flagged hunk read, every refused claim decided and the risk accepted. -/
theorem no_signature_without_evidence (hunks claims : List String) (es : List Event)
    (hsigned : (run (draft hunks claims) es).signed = true) :
    Ready (run (draft hunks claims) es) :=
  run_safe (draft hunks claims) es (by intro h; simp [draft] at h) hsigned

theorem signed_means_every_flagged_hunk_read (hunks claims : List String) (es : List Event)
    (hsigned : (run (draft hunks claims) es).signed = true) :
    ∀ h ∈ (run (draft hunks claims) es).requiredHunks, h ∈ (run (draft hunks claims) es).read :=
  (no_signature_without_evidence hunks claims es hsigned).2.2.1

theorem signed_means_every_refusal_decided (hunks claims : List String) (es : List Event)
    (hsigned : (run (draft hunks claims) es).signed = true) :
    ∀ c ∈ (run (draft hunks claims) es).requiredClaims, c ∈ (run (draft hunks claims) es).decided :=
  (no_signature_without_evidence hunks claims es hsigned).2.2.2

/-- The AI has no move in the protocol: no AI event changes a receipt. -/
theorem ai_changes_nothing (r : Receipt) (a : Action) : step r ⟨.ai, a⟩ = r := rfl

/-- A signed receipt is frozen. Only a human reopening it changes anything. -/
theorem signed_is_frozen (r : Receipt) (e : Event) (hs : r.signed = true)
    (hnot : e.action ≠ .reopen) : step r e = r := by
  cases e with
  | mk actor action =>
    cases actor with
    | ai => rfl
    | human =>
      cases action with
      | reopen => exact absurd rfl hnot
      | setOwner => simp [step, hs]
      | markRead => simp [step, hs]
      | decide => simp [step, hs]
      | acceptRisk => simp [step, hs]
      | sign => simp [step, hs]

theorem step_signs_only_by_human_sign (r : Receipt) (e : Event) (hs : r.signed = false)
    (h : (step r e).signed = true) : e.actor = .human ∧ e.action = .sign := by
  cases e with
  | mk actor action =>
    cases actor with
    | ai =>
        simp [step, hs] at h
    | human =>
        refine ⟨rfl, ?_⟩
        rw [step_draft r action hs] at h
        by_cases ha : action = .sign
        · exact ha
        · rw [apply_keeps_signed r action ha, hs] at h
          contradiction

/-- Every signature is a human act: a signed receipt has a human sign event in its history. -/
theorem every_signature_is_human (r : Receipt) (es : List Event) (h0 : r.signed = false)
    (h : (run r es).signed = true) : ∃ e ∈ es, e.actor = .human ∧ e.action = .sign := by
  induction es generalizing r with
  | nil =>
      simp [run, h0] at h
  | cons e es ih =>
      by_cases hs : (step r e).signed = true
      · exact ⟨e, by simp, step_signs_only_by_human_sign r e h0 hs⟩
      · have hf : (step r e).signed = false := by simpa using hs
        obtain ⟨e', he', hh⟩ := ih (step r e) hf h
        exact ⟨e', by simp [he'], hh⟩

/-- A trace with only AI events never produces a signature. -/
theorem ai_alone_never_signs (r : Receipt) (es : List Event) (h0 : r.signed = false)
    (hai : ∀ e ∈ es, e.actor = .ai) : (run r es).signed = false := by
  cases hrun : (run r es).signed with
  | false => rfl
  | true =>
      obtain ⟨e, he, hh, _⟩ := every_signature_is_human r es h0 hrun
      have := hai e he
      rw [hh] at this
      contradiction

end TrustReceipt

/-
  The merge gate, proven for histories of any length.

  hardening/tla/MergeGate.tla is the same gate as a TLA+ spec. TLC explores it with
  MaxPush = 3: 22 reachable states. That is a bounded check. Here the agent may push
  any number of times, and the invariant still holds.

  The planted bug of MergeGate-seeded.cfg (the gate checks "has evidence" instead of
  "has evidence for this head") is here as checksHead = false. Lean evaluates the same
  5-step trace that TLC printed and shows that it breaks the invariant.

  Check: nix shell nixpkgs#lean4 -c lean lean/MergeGate.lean
-/

namespace MergeGate

/-- Commit numbers start at 1. 0 means none. -/
structure Gate where
  head : Nat
  evidenceFor : Nat
  signedFor : Nat
  merged : Nat
  deriving DecidableEq, Repr

inductive Act where
  | agentPushes
  | reviewerAttachesEvidence
  | ownerSigns
  | gateMerges
  deriving DecidableEq, Repr

def init : Gate := ⟨1, 0, 0, 0⟩

/-- The sound gate wants evidence for the current head. The planted bug accepts any evidence. -/
def fresh (checksHead : Bool) (g : Gate) (c : Nat) : Bool :=
  if checksHead then c == g.head else c != 0

def step (checksHead : Bool) (g : Gate) : Act → Gate
  | .agentPushes => if g.merged = 0 then { g with head := g.head + 1 } else g
  | .reviewerAttachesEvidence => if g.merged = 0 then { g with evidenceFor := g.head } else g
  | .ownerSigns =>
      if g.merged = 0 ∧ fresh checksHead g g.evidenceFor = true then { g with signedFor := g.head } else g
  | .gateMerges =>
      if g.merged = 0 ∧ fresh checksHead g g.evidenceFor = true ∧ fresh checksHead g g.signedFor = true
      then { g with merged := g.head } else g

def run (checksHead : Bool) (g : Gate) : List Act → Gate
  | [] => g
  | a :: as => run checksHead (step checksHead g a) as

/-- MergedCommitHasFreshEvidence of the TLA+ spec. -/
def Inv (g : Gate) : Prop := g.merged ≠ 0 → g.evidenceFor = g.merged ∧ g.signedFor = g.merged

instance (g : Gate) : Decidable (Inv g) := by
  unfold Inv
  infer_instance

/-- After a merge, no action changes the gate. -/
theorem merged_is_frozen (c : Bool) (g : Gate) (a : Act) (h : g.merged ≠ 0) : step c g a = g := by
  cases a <;> simp [step, h]

theorem step_keeps_inv (g : Gate) (a : Act) (h : Inv g) : Inv (step true g a) := by
  by_cases hm : g.merged = 0
  · cases a <;> simp [step, hm, fresh, Inv] <;> split <;> simp_all
  · rw [merged_is_frozen true g a hm]
    exact h

theorem run_keeps_inv (g : Gate) (as : List Act) (h : Inv g) : Inv (run true g as) := by
  induction as generalizing g with
  | nil => exact h
  | cons a as ih => exact ih (step true g a) (step_keeps_inv g a h)

/-- The sound gate never merges a commit on evidence or a signature for an older commit, after any number of pushes. -/
theorem sound_gate_never_merges_stale (as : List Act) : Inv (run true init as) :=
  run_keeps_inv init as (by simp [Inv, init])

/-- The counterexample TLC printed for MergeGate-seeded.cfg, step by step. -/
def tlcTrace : List Act := [.reviewerAttachesEvidence, .agentPushes, .ownerSigns, .gateMerges]

/-- Lean reaches the same final state as TLC: head 2, evidence for 1, signed for 2, merged 2. -/
theorem seeded_trace_matches_tlc : run false init tlcTrace = ⟨2, 1, 2, 2⟩ := by decide

theorem seeded_gate_merges_stale : ¬ Inv (run false init tlcTrace) := by decide

/-- On the sound gate, the same events do not merge: the signature waits for fresh evidence. -/
theorem sound_gate_blocks_the_trace : (run true init tlcTrace).merged = 0 := by decide

end MergeGate

/-
  Issue 2234: how the generator collects keyed members, proven.

  TypeCollector.cs puts each [Key(n)] member of a [MessagePackObject] type into a map.
  Two members with the same key used to crash the analyzer (AD0001). Two agents fixed
  the crash in two different shapes:

  - the original agent (commit 9007cee1): report KeysMustBeUnique if the key is taken,
    then add the member only if the key is free (a ContainsKey guard with no else);
  - the replay agent (hardening/replay.sh): if the key is taken report, else add.

  Our syntax rule (hardening/rules/no-silent-duplicate-drop.yml) blocked the first shape
  and passed the second. Lean shows that the two shapes are the same function, and that
  this function silently drops a member in the source generator, where nobody receives
  the report. A strict version keeps every member or emits an error, for every input.

  The model predicts the output of the dotnet probe in public/evidence/replay/probe-d.log:
  for two members on Key(0), the generated formatter keeps Member1 and drops Member2.
  `pnpm j verify harden` checks that the log still says so.

  Check: nix shell nixpkgs#lean4 -c lean lean/Collector.lean
-/

namespace Collector

abbrev Member := Nat × String

/-- Collected members and reported diagnostics. -/
abbrev State := List Member × List String

def taken (acc : List Member) (m : Member) : Bool := acc.any (fun x => x.1 == m.1)

/-- `report` is false in the source generator: it runs with no diagnostic reporter. -/
def agentStep (report : Bool) (s : State) (m : Member) : State :=
  let d := if report && taken s.1 m then s.2 ++ ["KeysMustBeUnique"] else s.2
  let acc := if !taken s.1 m then s.1 ++ [m] else s.1
  (acc, d)

def replayStep (report : Bool) (s : State) (m : Member) : State :=
  if taken s.1 m then (s.1, if report then s.2 ++ ["KeysMustBeUnique"] else s.2)
  else (s.1 ++ [m], s.2)

def collectAgent (report : Bool) (ms : List Member) : State := ms.foldl (agentStep report) ([], [])
def collectReplay (report : Bool) (ms : List Member) : State := ms.foldl (replayStep report) ([], [])

theorem steps_agree (report : Bool) (s : State) (m : Member) : agentStep report s m = replayStep report s m := by
  unfold agentStep replayStep
  cases taken s.1 m <;> cases report <;> rfl

/-- The syntax rule saw two shapes. They are one function. -/
theorem replay_is_the_same_function : collectReplay = collectAgent := by
  funext report ms
  unfold collectReplay collectAgent
  have : replayStep report = agentStep report := by
    funext s m
    exact (steps_agree report s m).symm
  rw [this]

/-- Every input member reaches the output, or the user gets an error. -/
def NoSilentDrop (ms : List Member) (s : State) : Prop :=
  (∀ m ∈ ms, m.2 ∈ s.1.map Prod.snd) ∨ s.2 ≠ []

instance (ms : List Member) (s : State) : Decidable (NoSilentDrop ms s) := by
  unfold NoSilentDrop
  infer_instance

/-- The input of the dotnet probe: two members on Key(0). -/
def probeInput : List Member := [(0, "Member1"), (0, "Member2")]

/-- The model's prediction of probe D: the generated formatter has Member1 only, and nothing is reported. -/
theorem generator_output_matches_probe : collectAgent false probeInput = ([(0, "Member1")], []) := by decide

theorem agent_drops_silently_in_generator : ¬ NoSilentDrop probeInput (collectAgent false probeInput) := by decide

theorem replay_drops_silently_in_generator : ¬ NoSilentDrop probeInput (collectReplay false probeInput) := by
  rw [replay_is_the_same_function]
  exact agent_drops_silently_in_generator

/-- The fix the fence test asks for: duplicate keys emit an error and no formatter. -/
def collectStrict (ms : List Member) : State :=
  if (ms.map Prod.fst).Nodup then (ms, []) else ([], ["KeysMustBeUnique"])

theorem strict_never_drops_silently (ms : List Member) : NoSilentDrop ms (collectStrict ms) := by
  unfold collectStrict NoSilentDrop
  split
  · left
    intro m hm
    exact List.mem_map_of_mem hm
  · right
    simp

theorem strict_reports_the_probe : collectStrict probeInput = ([], ["KeysMustBeUnique"]) := by decide

end Collector

/-
  Issue 2283: the crash cannot be written here.

  TypeCollector.cs read `item.DeclaringSyntaxReferences[0]` to get a diagnostic location.
  For a symbol from a referenced assembly (metadata) that list is empty, so the generator
  threw IndexOutOfRangeException (warning CS8785) and the resolver was never generated.

  In Lean, `refs[0]` on a list only type-checks with a proof that the list is not empty.
  For a metadata symbol no such proof exists. So the bug class is unrepresentable:
  rung 0 of the enforcement ladder. The agent's fix (FirstOrDefault, a null location) is
  `List.head?`, which is total.

  Check: nix shell nixpkgs#lean4 -c lean lean/Location.lean
-/

namespace Location

/-- A symbol: from source code it has syntax references, from metadata it has none. -/
inductive Origin where
  | source
  | metadata
  deriving DecidableEq, Repr

structure Symbol (Syntax : Type) where
  origin : Origin
  refs : List Syntax
  wellFormed : origin = .metadata → refs = []

-- The old line 985, written in Lean, does not compile: there is no proof that refs is non-empty.
#check_failure (fun {Syntax : Type} (s : Symbol Syntax) => s.refs[0])

/-- Indexing compiles only with that proof in hand. -/
def firstRef {Syntax : Type} (s : Symbol Syntax) (h : 0 < s.refs.length) : Syntax := s.refs[0]

/-- For a metadata symbol the proof cannot exist, so firstRef cannot be called on it. -/
theorem metadata_has_no_index_proof {Syntax : Type} (s : Symbol Syntax) (hm : s.origin = .metadata) :
    ¬ 0 < s.refs.length := by
  rw [s.wellFormed hm]
  simp

/-- The agent's fix: FirstOrDefault, then a null location. Total for every symbol. -/
def location? {Syntax : Type} (s : Symbol Syntax) : Option Syntax := s.refs.head?

theorem metadata_symbol_gets_no_location {Syntax : Type} (s : Symbol Syntax) (hm : s.origin = .metadata) :
    location? s = none := by
  unfold location?
  rw [s.wellFormed hm]
  rfl

theorem source_symbol_keeps_its_location {Syntax : Type} (s : Symbol Syntax) (r : Syntax) (rs : List Syntax)
    (h : s.refs = r :: rs) : location? s = some r := by
  unfold location?
  rw [h]
  rfl

end Location