  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.