pith. machine review for the scientific record. sign in
structure definition def or abbrev

OpcodeSoundnessCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  83structure OpcodeSoundnessCert where deriving Repr
  84
  85/-- Parser covers all VM opcodes by name. -/
  86@[simp] def OpcodeSoundnessCert.verified (_c : OpcodeSoundnessCert) : Prop :=

proof body

Definition body.

  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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.