ScheduleNeutralityCert

formal source

 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