`OpcodeSoundnessCert`

definition

show as: view math explainer →

module: IndisputableMonolith.URCGenerators.LNALCerts
domain: URCGenerators
line: 83 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.URCGenerators.LNALCerts on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

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