Controller

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import NimRecurrent2import AttainCircuit34/- Phase 4, Priority 3: one explicit two-pass recurrent controller.  Written by5   Claude (10 October 2026).  Lean 4.26.0, core/Std only.67   Tokens: row x | sep | reset.  Modes: scan / replay.  Registers: acc, prev, valid8   (summary part, as in phase 3), sig (stored summary fed to replay), idx (replay9   counter), sel and fnz (selected cancelling move and fallback move).10     scan,  row x : acc := acc XOR x11     scan,  sep   : emit summary (acc, diff if valid); prev := acc; valid := true;12                    sig := acc; acc := 0; idx := 0; sel := fnz := none; mode := replay13     replay,row x : replay step with summary sig (phase-3 `replayStep`)14     replay,sep   : emit move (sel, else fnz, else halt); idx := 0; sel := fnz := none;15                    mode := scan16     reset        : back to the initial state (between games)17   Input protocol for one decision on board P: rows of P, sep, rows of P again, sep.18   Proved here: the combined protocol (summary THEN the move computed from the stored19   summary), legality / zero successor / terminal handling, winning against every20   legal opponent via the game semantics, reset, reachable-register bounds (no counter21   overflow).  The bit-level per-update circuits and their refinement are in22   ControllerBits.lean. -/2324namespace NimAudit25namespace Controller2627open Game Rollout Prob Attain Recurrent AC0 AC0.Circ2829inductive Tok where30  | row (x : Nat)31  | sep32  | reset3334structure CState where35  replayMode : Bool36  acc : Nat37  prev : Nat38  valid : Bool39  sig : Nat40  idx : Nat41  sel : Option (Nat × Nat)42  fnz : Option (Nat × Nat)4344inductive COut where45  | summary (s : Nat) (diff : Option Nat)46  | move (m : Option (Nat × Nat))4748def cinit : CState := ⟨false, 0, 0, false, 0, 0, none, none⟩4950/-- One update of the controller. -/51def cstep (s : CState) : Tok → CState × Option COut52  | .reset => (cinit, none)53  | .row x =>54    if s.replayMode then55      (⟨s.replayMode, s.acc, s.prev, s.valid, s.sig, (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).idx,56        (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).sel, (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).fnz⟩,57       none)58    else (⟨s.replayMode, s.acc ^^^ x, s.prev, s.valid, s.sig, s.idx, s.sel, s.fnz⟩, none)59  | .sep =>60    if s.replayMode then61      (⟨false, s.acc, s.prev, s.valid, s.sig, 0, none, none⟩, some (.move (firstSome s.sel s.fnz)))62    else63      (⟨true, 0, s.acc, true, s.acc, 0, none, none⟩,64       some (.summary s.acc (if s.valid then some (s.prev ^^^ s.acc) else none)))6566def crun : CState → List Tok → CState × List COut67  | s, [] => (s, [])68  | s, t :: ts => ((crun (cstep s t).1 ts).1, (cstep s t).2.toList ++ (crun (cstep s t).1 ts).2)6970/-- All states visited (initial state included). -/71def crunStates : CState → List Tok → List CState72  | s, [] => [s]73  | s, t :: ts => s :: crunStates (cstep s t).1 ts7475/-- The tokens of one decision: scan, separator, replay, separator. -/76def dtoks (P : List Nat) : List Tok := P.map Tok.row ++ [Tok.sep] ++ P.map Tok.row ++ [Tok.sep]7778def stream (Ps : List (List Nat)) : List Tok := Ps.flatMap dtoks7980/-- Games separated by reset tokens (a reset precedes every game). -/81def gameStream (gs : List (List (List Nat))) : List Tok := gs.flatMap (fun g => Tok.reset :: stream g)8283/-- Idle: scan mode with empty accumulator and cleared replay registers. -/84def Idle (s : CState) : Prop := s.replayMode = false ∧ s.acc = 0 ∧ s.idx = 0 ∧ s.sel = none ∧ s.fnz = none8586theorem crun_append (s : CState) (ts us : List Tok) :87    crun s (ts ++ us) = ((crun (crun s ts).1 us).1, (crun s ts).2 ++ (crun (crun s ts).1 us).2) := by88  induction ts generalizing s with89  | nil => simp [crun]90  | cons t ts ih => simp only [List.cons_append, crun, ih, List.append_assoc]9192theorem crunStates_append (s : CState) (ts us : List Tok) :93    ∀ st ∈ crunStates s (ts ++ us), st ∈ crunStates s ts ∨ st ∈ crunStates (crun s ts).1 us := by94  induction ts generalizing s with95  | nil => intro st h; right; simpa [crun] using h96  | cons t ts ih =>97    intro st h98    simp only [List.cons_append, crunStates, List.mem_cons] at h99    rcases h with rfl | h100    · left; simp [crunStates]101    · rcases ih _ st h with h' | h'102      · left; simp [crunStates, h']103      · right; simpa [crun] using h'104105theorem crun_mem_states (s : CState) (ts : List Tok) : (crun s ts).1 ∈ crunStates s ts := by106  induction ts generalizing s with107  | nil => simp [crun, crunStates]108  | cons t ts ih => simp only [crun, crunStates, List.mem_cons]; right; exact ih _109110/-! ## The combined protocol -/111112theorem crun_scan_rows (s : CState) (hs : s.replayMode = false) (P : List Nat) :113    crun s (P.map Tok.row) = (⟨false, s.acc ^^^ nimSum P, s.prev, s.valid, s.sig, s.idx, s.sel, s.fnz⟩, []) := by114  induction P generalizing s with115  | nil => cases s; simp_all [crun, nimSum]116  | cons x P ih =>117    simp only [List.map_cons, crun, cstep, hs, Bool.false_eq_true, if_false]118    rw [ih _ rfl]119    simp [nimSum, Nat.xor_assoc, Option.toList]120121theorem crun_replay_rows (s : CState) (hs : s.replayMode = true) (P : List Nat) :122    crun s (P.map Tok.row) =123      (⟨true, s.acc, s.prev, s.valid, s.sig, (replay s.sig ⟨s.idx, s.sel, s.fnz⟩ P).idx,124        (replay s.sig ⟨s.idx, s.sel, s.fnz⟩ P).sel, (replay s.sig ⟨s.idx, s.sel, s.fnz⟩ P).fnz⟩, []) := by125  induction P generalizing s with126  | nil => cases s; simp_all [crun, replay]127  | cons x P ih =>128    simp only [List.map_cons, crun, cstep, hs, if_true]129    rw [ih _ (by rfl)]130    simp [replay, Option.toList]131132/-- ONE DECISION: from an idle state, the controller emits the summary and then the133    move computed by replay FROM THE STORED SUMMARY, and returns to an idle state that134    retains the summary. -/135theorem crun_decision (s : CState) (hs : Idle s) (P : List Nat) :136    crun s (dtoks P) =137      (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩,138       [COut.summary (nimSum P) (if s.valid then some (s.prev ^^^ nimSum P) else none),139        COut.move (replayMove (nimSum P) P)]) := by140  obtain ⟨hm, ha, hi, hsel, hf⟩ := hs141  unfold dtoks142  rw [crun_append, crun_append, crun_append, crun_scan_rows s hm]143  simp only [crun, cstep, Bool.false_eq_true, if_false, ha, Nat.zero_xor, Option.toList]144  rw [crun_replay_rows _ rfl]145  simp only [crun, cstep, if_true, Option.toList, List.nil_append, List.append_nil,146    List.cons_append, List.singleton_append]147  unfold replayMove148  simp149150/-- Expected outputs of a stream of decisions. -/151def ctrlOuts : Bool → Nat → List (List Nat) → List COut152  | _, _, [] => []153  | v, q, P :: Ps =>154    COut.summary (nimSum P) (if v then some (q ^^^ nimSum P) else none) ::155      COut.move (replayMove (nimSum P) P) :: ctrlOuts true (nimSum P) Ps156157/-- STREAM THEOREM: for any finite sequence of boards (empty boards allowed), from an158    idle state the outputs are summary/move pairs; every move is computed from the159    summary stored at that board's separator. -/160theorem crun_stream (s : CState) (hs : Idle s) (Ps : List (List Nat)) :161    (crun s (stream Ps)).2 = ctrlOuts s.valid s.prev Ps ∧ Idle (crun s (stream Ps)).1 := by162  induction Ps generalizing s with163  | nil => exact ⟨rfl, hs⟩164  | cons P Ps ih =>165    have e : stream (P :: Ps) = dtoks P ++ stream Ps := by simp [stream]166    rw [e, crun_append, crun_decision s hs P]167    have hidle : Idle (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=168      ⟨rfl, rfl, rfl, rfl, rfl⟩169    obtain ⟨h1, h2⟩ := ih _ hidle170    exact ⟨by simp [ctrlOuts, h1], h2⟩171172theorem cinit_idle : Idle cinit := ⟨rfl, rfl, rfl, rfl, rfl⟩173174/-- RESET: a reset token returns the controller to the initial state from ANY state175    (no accidental persistence between games). -/176theorem crun_reset (s : CState) (ts : List Tok) : crun s (Tok.reset :: ts) = crun cinit ts := by177  simp [crun, cstep, Option.toList]178179/-- GAMES: from any state whatsoever, a stream of games each preceded by a reset180    produces, game by game, the outputs of a fresh controller. -/181theorem crun_games (s : CState) (gs : List (List (List Nat))) :182    (crun s (gameStream gs)).2 = gs.flatMap (ctrlOuts false 0) := by183  induction gs generalizing s with184  | nil => rfl185  | cons g gs ih =>186    have e : gameStream (g :: gs) = (Tok.reset :: stream g) ++ gameStream gs := by187      simp [gameStream]188    rw [e, crun_append, crun_reset]189    obtain ⟨h1, _⟩ := crun_stream cinit cinit_idle g190    simp only [List.flatMap_cons]191    rw [ih, h1]192    rfl193194/-- Empty boards and consecutive separators: an empty board is the token pair195    sep, sep; the controller reports summary 0 and halts (move none). -/196theorem empty_board (s : CState) (hs : Idle s) :197    dtoks [] = [Tok.sep, Tok.sep] ∧198    (crun s (dtoks [])).2 = [COut.summary 0 (if s.valid then some (s.prev ^^^ 0) else none),199      COut.move none] := by200  refine ⟨rfl, ?_⟩201  rw [crun_decision s hs]202  simp [nimSum, replayMove, replay, firstSome]203204/-! ## The decision is correct and wins -/205206/-- The move output of a decision (independent of the retained summary state). -/207def decisionMove (P : List Nat) : Option (Nat × Nat) := replayMove (nimSum P) P208209/-- DECISION CORRECTNESS: legal move; zero successor from nonzero positions; halt210    exactly on terminal boards. -/211theorem decision_correct (P : List Nat) :212    (decisionMove P = none ↔ Terminal P) ∧213    (∀ i v, decisionMove P = some (i, v) → ∃ x, P[i]? = some x ∧ v < x ∧ Move P (P.set i v)) ∧214    (nimSum P ≠ 0 → ∃ i v, decisionMove P = some (i, v) ∧ nimSum (P.set i v) = 0) := by215  obtain ⟨h1, h2, h3⟩ := replay_correct P216  refine ⟨h1, fun i v h => ?_, h3⟩217  obtain ⟨x, hx, hlt⟩ := h2 i v h218  exact ⟨x, hx, hlt, set_move hx hlt⟩219220/-- The controller as a strategy on boards. -/221def ctrlSel (P : List Nat) : Option (List Nat) := (decisionMove P).map (fun m => P.set m.1 m.2)222223/-- WINNING AGAINST EVERY LEGAL OPPONENT (checked game semantics): from every board224    with nonzero nim-sum, the controller's decisions win. -/225theorem ctrl_wins (P : List Nat) (h : nimSum P ≠ 0) : Wins ctrlSel P := by226  obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h227  obtain ⟨x, hx, hlt, hm⟩ := (decision_correct P).2.1 i v hd228  refine Wins.intro P (P.set i v) (by simp [ctrlSel, hd]) hm ?_229  intro r hr230  have h1 := move_sum_lt hm231  have h2 := move_sum_lt hr232  exact ctrl_wins r (move_from_zero hr hz)233termination_by P.sum234235/-! ## Reachable registers fit in B and r bits -/236237/-- Register bounds for N heaps of B bits and an r-bit counter (N < 2^r). -/238def Fits (B N : Nat) (s : CState) : Prop :=239  s.acc < 2 ^ B ∧ s.prev < 2 ^ B ∧ s.sig < 2 ^ B ∧ s.idx ≤ N ∧240  (∀ i v, s.sel = some (i, v) → i < N ∧ v < 2 ^ B) ∧241  (∀ i v, s.fnz = some (i, v) → i < N ∧ v < 2 ^ B)242243theorem replayStep_fits {B σ : Nat} {r : Replay} {x : Nat} (hx : x < 2 ^ B)244    (hsel : ∀ i v, r.sel = some (i, v) → i < r.idx ∧ v < 2 ^ B)245    (hfnz : ∀ i v, r.fnz = some (i, v) → i < r.idx ∧ v < 2 ^ B) :246    (replayStep σ r x).idx = r.idx + 1 ∧247    (∀ i v, (replayStep σ r x).sel = some (i, v) → i < r.idx + 1 ∧ v < 2 ^ B) ∧248    (∀ i v, (replayStep σ r x).fnz = some (i, v) → i < r.idx + 1 ∧ v < 2 ^ B) := by249  refine ⟨rfl, ?_, ?_⟩250  · intro i v h251    simp only [replayStep] at h252    cases hs : r.sel with253    | some m =>254      rw [hs] at h; simp only [Option.some.injEq] at h; subst h255      obtain ⟨h1, h2⟩ := hsel _ _ hs; exact ⟨by omega, h2⟩256    | none =>257      rw [hs] at h258      simp only at h259      split at h260      · next hc => simp only [Option.some.injEq, Prod.mk.injEq] at h261                   obtain ⟨rfl, rfl⟩ := h; exact ⟨by omega, Nat.lt_trans hc.2 hx⟩262      · cases h263  · intro i v h264    simp only [replayStep] at h265    cases hs : r.fnz with266    | some m =>267      rw [hs] at h; simp only [Option.some.injEq] at h; subst h268      obtain ⟨h1, h2⟩ := hfnz _ _ hs; exact ⟨by omega, h2⟩269    | none =>270      rw [hs] at h271      simp only at h272      split at h273      · simp only [Option.some.injEq, Prod.mk.injEq] at h274        obtain ⟨rfl, rfl⟩ := h; exact ⟨by omega, by omega⟩275      · cases h276277theorem scan_rows_fit {B N : Nat} (s : CState) (hm : s.replayMode = false) (hf : Fits B N s)278    (P : List Nat) (hw : Width B P) : ∀ st ∈ crunStates s (P.map Tok.row), Fits B N st := by279  induction P generalizing s with280  | nil => intro st h; simp [crunStates] at h; subst h; exact hf281  | cons x P ih =>282    intro st h283    simp only [List.map_cons, crunStates, List.mem_cons] at h284    rcases h with rfl | h285    · exact hf286    · have hx : x < 2 ^ B := hw x (by simp)287      have hf' : Fits B N (cstep s (Tok.row x)).1 := by288        simp only [cstep, hm, Bool.false_eq_true, if_false]289        exact ⟨Nat.xor_lt_two_pow hf.1 hx, hf.2.1, hf.2.2.1, hf.2.2.2.1, hf.2.2.2.2.1, hf.2.2.2.2.2⟩290      have hm' : (cstep s (Tok.row x)).1.replayMode = false := by simp [cstep, hm]291      exact ih _ hm' hf' (fun y hy => hw y (List.mem_cons_of_mem _ hy)) st h292293theorem replay_rows_fit {B N : Nat} (s : CState) (hm : s.replayMode = true)294    (hregs : s.acc < 2 ^ B ∧ s.prev < 2 ^ B ∧ s.sig < 2 ^ B)295    (hsel : ∀ i v, s.sel = some (i, v) → i < s.idx ∧ v < 2 ^ B)296    (hfnz : ∀ i v, s.fnz = some (i, v) → i < s.idx ∧ v < 2 ^ B)297    (P : List Nat) (hlen : s.idx + P.length ≤ N) (hw : Width B P) :298    ∀ st ∈ crunStates s (P.map Tok.row), Fits B N st := by299  induction P generalizing s with300  | nil =>301    intro st h; simp [crunStates] at h; subst h302    exact ⟨hregs.1, hregs.2.1, hregs.2.2, by simpa using hlen,303      fun i v h => ⟨by have := (hsel i v h).1; simp at hlen; omega, (hsel i v h).2⟩,304      fun i v h => ⟨by have := (hfnz i v h).1; simp at hlen; omega, (hfnz i v h).2⟩⟩305  | cons x P ih =>306    intro st h307    simp only [List.map_cons, crunStates, List.mem_cons] at h308    have hx : x < 2 ^ B := hw x (by simp)309    simp only [List.length_cons] at hlen310    rcases h with rfl | h311    · exact ⟨hregs.1, hregs.2.1, hregs.2.2, by omega,312        fun i v h => ⟨by have := (hsel i v h).1; omega, (hsel i v h).2⟩,313        fun i v h => ⟨by have := (hfnz i v h).1; omega, (hfnz i v h).2⟩⟩314    · obtain ⟨hi, hs', hf'⟩ := replayStep_fits (σ := s.sig) (r := ⟨s.idx, s.sel, s.fnz⟩) hx hsel hfnz315      dsimp only at hi hs' hf'316      apply ih (cstep s (Tok.row x)).1 (by simp [cstep, hm])317      · simp only [cstep, hm, if_true]; exact hregs318      · simp only [cstep, hm, if_true]; rw [hi]; exact hs'319      · simp only [cstep, hm, if_true]; rw [hi]; exact hf'320      · simp only [cstep, hm, if_true]; rw [hi]; omega321      · exact fun y hy => hw y (List.mem_cons_of_mem _ hy)322      · exact h323324/-- REACHABLE-STATE BOUNDS: along a well-formed stream of boards of N heaps below 2^B,325    started from an idle fitting state, EVERY visited state has acc, prev, sig < 2^B,326    counter ≤ N, and selected/fallback moves with index < N and value < 2^B.  With327    N < 2^r, every register fits its r- or B-bit field; the counter never overflows. -/328theorem stream_fits {B N : Nat} (s : CState) (hs : Idle s) (hf : Fits B N s) (Ps : List (List Nat))329    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) : ∀ st ∈ crunStates s (stream Ps), Fits B N st := by330  induction Ps generalizing s with331  | nil => intro st h; simp [stream, crunStates] at h; subst h; exact hf332  | cons P Ps ih =>333    have e : stream (P :: Ps) = dtoks P ++ stream Ps := by simp [stream]334    rw [e]335    intro st h336    obtain ⟨hlenP, hwP⟩ := hP P (by simp)337    rcases crunStates_append s _ _ st h with h1 | h1338    · -- inside the decision339      unfold dtoks at h1340      rcases crunStates_append s _ _ st h1 with h2 | h2341      · rcases crunStates_append s _ _ st h2 with h3 | h3342        · rcases crunStates_append s _ _ st h3 with h4 | h4343          · exact scan_rows_fit s hs.1 hf P hwP st h4344          · rw [crun_scan_rows s hs.1] at h4345            simp only [crunStates, cstep, Bool.false_eq_true, if_false, List.mem_cons,346              List.mem_singleton] at h4347            have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)348            rcases h4 with rfl | rfl | h4349            · exact ⟨ha, hf.2.1, hf.2.2.1, hf.2.2.2.1, hf.2.2.2.2.1, hf.2.2.2.2.2⟩350            · exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩351            · simp at h4352        · rw [crun_append, crun_scan_rows s hs.1] at h3353          simp only [crun, cstep, Bool.false_eq_true, if_false] at h3354          have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)355          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P356            (by simp [hlenP]) hwP st h3357      · rw [crun_append, crun_append, crun_scan_rows s hs.1] at h2358        simp only [crun, cstep, Bool.false_eq_true, if_false] at h2359        have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)360        generalize hS1 : (⟨true, 0, s.acc ^^^ nimSum P, true, s.acc ^^^ nimSum P, 0, none, none⟩ :361          CState) = S1 at h2362        have hS1m : S1.replayMode = true := by rw [← hS1]363        simp only [crunStates, List.mem_cons, List.mem_singleton] at h2364        rcases h2 with rfl | rfl | h2365        · subst hS1366          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P367            (by simp [hlenP]) hwP _ (crun_mem_states _ _)368        · rw [crun_replay_rows _ hS1m]369          subst hS1370          simp only [cstep, if_true]371          exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩372        · simp at h2373    · rw [crun_decision s hs P] at h1374      have hidle : Idle (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=375        ⟨rfl, rfl, rfl, rfl, rfl⟩376      have hfit : Fits B N (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=377        ⟨Nat.two_pow_pos B, nimSum_lt hwP, nimSum_lt hwP, Nat.zero_le _, by simp, by simp⟩378      exact ih _ hidle hfit (fun Q hQ => hP Q (by simp [hQ])) st h1379380381/-! ## Axiom audit -/382383#print axioms crun_append384#print axioms crunStates_append385#print axioms crun_mem_states386#print axioms crun_scan_rows387#print axioms crun_replay_rows388#print axioms crun_decision389#print axioms crun_stream390#print axioms cinit_idle391#print axioms crun_reset392#print axioms crun_games393#print axioms empty_board394#print axioms decision_correct395#print axioms ctrl_wins396#print axioms replayStep_fits397#print axioms scan_rows_fit398#print axioms replay_rows_fit399#print axioms stream_fits400end Controller401end NimAudit