IndisputableMonolith.URCGenerators.LNALCerts

   1import Mathlib
   2import IndisputableMonolith.LNAL.Compiler
   3import IndisputableMonolith.LNAL.Parser
   4import IndisputableMonolith.LNAL.Invariants
   5import IndisputableMonolith.LNAL.VM
   6import IndisputableMonolith.Certificates.JMonotone
   7import IndisputableMonolith.Certificates.UnitsKGate
   8
   9namespace IndisputableMonolith
  10namespace URCGenerators
  11
  12open IndisputableMonolith.LNAL
  13
  14/-- LNAL invariants certificate: bundles VM preservation and token δ‑unit bound. -/
  15structure LNALInvariantsCert where
  16  ok     : Bool
  17  errors : List String := []
  18deriving Repr
  19
  20@[simp] def LNALInvariantsCert.verified (_c : LNALInvariantsCert) : Prop :=
  21  -- 1) VMInvariant preserved by one small-step
  22  (∀ (P : IndisputableMonolith.LNAL.LProgram)
  23     (s : IndisputableMonolith.LNAL.LState),
  24      IndisputableMonolith.LNAL.VMInvariant s →
  25      IndisputableMonolith.LNAL.VMInvariant (IndisputableMonolith.LNAL.lStep P s))
  26  ∧
  27  -- 2) Token parity implies |ΔtokenCt| ≤ 1 per step
  28  (∀ (P : IndisputableMonolith.LNAL.LProgram)
  29     (s : IndisputableMonolith.LNAL.LState),
  30      IndisputableMonolith.LNAL.TokenParityInvariant s →
  31      IndisputableMonolith.LNAL.DeltaUnit s.aux5.tokenCt
  32        (IndisputableMonolith.LNAL.lStep P s).aux5.tokenCt)
  33
  34@[simp] theorem LNALInvariantsCert.verified_any (c : LNALInvariantsCert) :
  35  LNALInvariantsCert.verified c := by
  36  constructor
  37  · intro P s h; simpa using
  38      (IndisputableMonolith.LNAL.lStep_preserves_VMInvariant (P:=P) (s:=s) h)
  39  · intro P s h; simpa using
  40      (IndisputableMonolith.LNAL.token_delta_unit (P:=P) (s:=s) h)
  41
  42def LNALInvariantsCert.fromSource (src : String) : LNALInvariantsCert :=
  43  let parsed := parseProgramFull src
  44  let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
  45  let emptyPackets : PhiIR.PacketAnalysis := {}
  46  let code := match parsed with
  47    | .ok out => out.code
  48    | .error _ => #[]
  49  let phi := match parsed with
  50    | .ok out => out.phi
  51    | .error _ => emptyPhi
  52  let packets := match parsed with
  53    | .ok out => out.packets
  54    | .error _ => emptyPackets
  55  let rep := staticChecks code phi packets
  56  { ok := rep.ok, errors := rep.errors }
  57
  58/-- Certificate stub for compiler checks (identical to invariants for now). -/
  59structure CompilerChecksCert where
  60  ok     : Bool
  61  errors : List String := []
  62deriving Repr
  63
  64@[simp] def CompilerChecksCert.verified (c : CompilerChecksCert) : Prop := c.ok = true
  65
  66def CompilerChecksCert.fromSource (src : String) : CompilerChecksCert :=
  67  let parsed := parseProgramFull src
  68  let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
  69  let emptyPackets : PhiIR.PacketAnalysis := {}
  70  let code := match parsed with
  71    | .ok out => out.code
  72    | .error _ => #[]
  73  let phi := match parsed with
  74    | .ok out => out.phi
  75    | .error _ => emptyPhi
  76  let packets := match parsed with
  77    | .ok out => out.packets
  78    | .error _ => emptyPackets
  79  let rep := staticChecks code phi packets
  80  { ok := rep.ok, errors := rep.errors }
  81
  82/-- Opcode soundness certificate (parsing validates opcode set). -/
  83structure OpcodeSoundnessCert where deriving Repr
  84
  85/-- Parser covers all VM opcodes by name. -/
  86@[simp] def OpcodeSoundnessCert.verified (_c : OpcodeSoundnessCert) : Prop :=
  87  ∀ (op : IndisputableMonolith.LNAL.Opcode),
  88    ∃ s : String, IndisputableMonolith.LNAL.parseOpcode s = some op
  89
  90@[simp] theorem OpcodeSoundnessCert.verified_any (c : OpcodeSoundnessCert) :
  91  OpcodeSoundnessCert.verified c := by
  92  intro op; cases op <;> first
  93    | exact ⟨"LOCK", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  94    | exact ⟨"BALANCE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  95    | exact ⟨"FOLD", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  96    | exact ⟨"UNFOLD", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  97    | exact ⟨"BRAID", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  98    | exact ⟨"HARDEN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
  99    | exact ⟨"SEED", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 100    | exact ⟨"SPAWN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 101    | exact ⟨"MERGE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 102    | exact ⟨"LISTEN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 103    | exact ⟨"GIVE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 104    | exact ⟨"REGIVE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 105    | exact ⟨"FLIP", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 106    | exact ⟨"VECTOR_EQ", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 107    | exact ⟨"CYCLE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 108    | exact ⟨"GC_SEED", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
 109
 110def OpcodeSoundnessCert.fromSource (_src : String) : OpcodeSoundnessCert :=
 111  {}
 112
 113/-- Schedule neutrality certificate aggregating schedule-related checks. -/
 114structure ScheduleNeutralityCert where
 115  ok     : Bool
 116  errors : List String := []
 117deriving Repr
 118
 119@[simp] def ScheduleNeutralityCert.verified (_c : ScheduleNeutralityCert) : Prop :=
 120  ∀ (P : IndisputableMonolith.LNAL.LProgram)
 121    (s : IndisputableMonolith.LNAL.LState),
 122    IndisputableMonolith.LNAL.EightTickInvariant P s →
 123    ∃ r, r ≤ 7 ∧ ∀ k,
 124      (Function.iterate (IndisputableMonolith.LNAL.lStep P) (r + 8 * k) s).winIdx8 = 0 ∧
 125      (Function.iterate (IndisputableMonolith.LNAL.lStep P) (r + 8 * k) s).winSum8 = 0
 126
 127@[simp] theorem ScheduleNeutralityCert.verified_any (c : ScheduleNeutralityCert) :
 128  ScheduleNeutralityCert.verified c := by
 129  intro P s H
 130  simpa using IndisputableMonolith.LNAL.schedule_neutrality_rotation (P:=P) (s:=s) H
 131
 132def ScheduleNeutralityCert.fromSource (src : String) : ScheduleNeutralityCert :=
 133  let parsed := parseProgramFull src
 134  let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
 135  let emptyPackets : PhiIR.PacketAnalysis := {}
 136  let code := match parsed with
 137    | .ok out => out.code
 138    | .error _ => #[]
 139  let phi := match parsed with
 140    | .ok out => out.phi
 141    | .error _ => emptyPhi
 142  let packets := match parsed with
 143    | .ok out => out.packets
 144    | .error _ => emptyPackets
 145  let rep := staticChecks code phi packets
 146  { ok := rep.ok, errors := rep.errors }
 147
 148/-- Cost ceiling certificate (|net GIVE−REGIVE| ≤ 4 per 8‑tick window). -/
 149structure CostCeilingCert where
 150  ok     : Bool
 151  errors : List String := []
 152deriving Repr
 153
 154@[simp] def CostCeilingCert.verified (_c : CostCeilingCert) : Prop :=
 155  -- At 8k boundaries, window cost is bounded (indeed zero)
 156  (∀ (P : IndisputableMonolith.LNAL.LProgram)
 157     (s : IndisputableMonolith.LNAL.LState),
 158      IndisputableMonolith.LNAL.EightTickInvariant P s →
 159      ∀ k, Int.abs (IndisputableMonolith.LNAL.windowCostAt P s (8 * k)) ≤ 4)
 160  ∧
 161  -- There exists r ≤ 7 such that rotated boundaries are also bounded
 162  (∀ (P : IndisputableMonolith.LNAL.LProgram)
 163     (s : IndisputableMonolith.LNAL.LState),
 164      IndisputableMonolith.LNAL.EightTickInvariant P s →
 165      ∃ r, r ≤ 7 ∧ ∀ k,
 166        Int.abs (IndisputableMonolith.LNAL.windowCostAt P s (r + 8 * k)) ≤ 4)
 167
 168@[simp] theorem CostCeilingCert.verified_any (c : CostCeilingCert) :
 169  CostCeilingCert.verified c := by
 170  constructor
 171  · intro P s H k; simpa using
 172      (IndisputableMonolith.LNAL.cost_ceiling_window_boundaries (P:=P) (s:=s) H k)
 173  · intro P s H; simpa using
 174      (IndisputableMonolith.LNAL.cost_ceiling_window_rotated (P:=P) (s:=s) H)
 175
 176def CostCeilingCert.fromSource (src : String) : CostCeilingCert :=
 177  let parsed := parseProgramFull src
 178  let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
 179  let emptyPackets : PhiIR.PacketAnalysis := {}
 180  let code := match parsed with
 181    | .ok out => out.code
 182    | .error _ => #[]
 183  let phi := match parsed with
 184    | .ok out => out.phi
 185    | .error _ => emptyPhi
 186  let packets := match parsed with
 187    | .ok out => out.packets
 188    | .error _ => emptyPackets
 189  let rep := staticChecks code phi packets
 190  { ok := rep.ok, errors := rep.errors }
 191
 192/-- SU(3) braid mask certificate: SU3Invariant preserved under lStep. -/
 193structure SU3MaskCert where deriving Repr
 194
 195@[simp] def SU3MaskCert.verified (_c : SU3MaskCert) : Prop :=
 196  ∀ (P : IndisputableMonolith.LNAL.LProgram)
 197    (s : IndisputableMonolith.LNAL.LState),
 198    IndisputableMonolith.LNAL.SU3Invariant s →
 199    IndisputableMonolith.LNAL.SU3Invariant (IndisputableMonolith.LNAL.lStep P s)
 200
 201@[simp] theorem SU3MaskCert.verified_any (c : SU3MaskCert) :
 202  SU3MaskCert.verified c := by
 203  intro P s h
 204  simpa using IndisputableMonolith.LNAL.lStep_preserves_su3 (P:=P) (s:=s) h
 205
 206def SU3MaskCert.fromSource (_src : String) : SU3MaskCert :=
 207  {}
 208
 209/-- J‑monotone per‑window budget certificate. -/
 210def JMonotoneCert := IndisputableMonolith.Certificates.JMonotoneCert
 211
 212@[simp] def JMonotoneCert.verified :=
 213  IndisputableMonolith.Certificates.JMonotoneCert.verified
 214
 215def JMonotoneCert.fromSource (src : String) : JMonotoneCert :=
 216  IndisputableMonolith.Certificates.JMonotoneCert.fromSource src
 217
 218/-- Placeholder Units/K‑gate audit in bundle. -/
 219def UnitsKGateCert := IndisputableMonolith.Certificates.UnitsKGateCert
 220
 221@[simp] def UnitsKGateCert.verified :=
 222  IndisputableMonolith.Certificates.UnitsKGateCert.verified
 223
 224def UnitsKGateCert.fromSource (src : String) : UnitsKGateCert :=
 225  IndisputableMonolith.Certificates.UnitsKGateCert.fromSource src
 226
 227end URCGenerators
 228end IndisputableMonolith
 229