IndisputableMonolith.Certificates.JMonotone

   1import Mathlib
   2import IndisputableMonolith.LNAL.Parser
   3import IndisputableMonolith.LNAL.JBudget
   4
   5namespace IndisputableMonolith
   6namespace Certificates
   7
   8open IndisputableMonolith.LNAL
   9
  10/-- Certificate package for per-window J-budget monotonicity diagnostics. -/
  11structure JMonotoneCert where
  12  ok          : Bool
  13  initBudget  : Nat := 4
  14  budgets     : Array Nat := #[]
  15  deltaJ      : Array Nat := #[]
  16  violations  : List Nat := []
  17  errors      : List String := []
  18deriving Repr
  19
  20@[simp] def JMonotoneCert.verified (c : JMonotoneCert) : Prop := c.ok = true
  21
  22private def mkError (idxs : List Nat) : List String :=
  23  match idxs with
  24  | []      => []
  25  | (i::_)  =>
  26      let windowStart := (i / 8) * 8
  27      [s!"J-monotone violated within window starting at {windowStart} (first increase at step {i}→{i+1})"]
  28
  29/-- Build a JMonotone certificate from compiled code. -/
  30def JMonotoneCert.fromProgram (code : Array LInstr) (initBudget : Nat := 4) : JMonotoneCert :=
  31  let budgets := simulateBudget code initBudget
  32  let delta := deltaJPerWindow code
  33  let violations := jMonotoneViolations code initBudget code.size
  34  let ok := violations = []
  35  let errors := if ok then [] else mkError violations
  36  { ok := ok, initBudget := initBudget, budgets := budgets, deltaJ := delta,
  37    violations := violations, errors := errors }
  38
  39/-- Build a JMonotone certificate directly from LNAL source text. -/
  40def JMonotoneCert.fromSource (src : String) (initBudget : Nat := 4) : JMonotoneCert :=
  41  let code := match parseProgram src with
  42    | .ok code => code
  43    | .error _ => #[]
  44  fromProgram code initBudget
  45
  46/-- Helper returning the first violation index, if any. -/
  47def JMonotoneCert.firstViolation? (c : JMonotoneCert) : Option Nat :=
  48  match c.violations with
  49  | [] => none
  50  | i :: _ => some i
  51