talos/codelib/CodeLib.lean at b9ab6bd968e3e16de2e34da1c1c7ab499db224c6 · cajal-technologies/talos · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
import CodeLib.Attrs
import CodeLib.Basic
import CodeLib.Entry
import CodeLib.Equivalence
import CodeLib.UInt32
import CodeLib.UInt64
import CodeLib.RustStd.Frame
import CodeLib.RustStd.Region
import CodeLib.RustStd.MemArray
import CodeLib.RustStd.MemFillLoop
import CodeLib.RustStd.MemCopyLoop
import CodeLib.RustStd.UInt
import CodeLib.RustStd.U64.Basic
import CodeLib.RustStd.U64.AbsDiff
import CodeLib.RustStd.U64.Add
import CodeLib.RustStd.U64.Sub
import CodeLib.RustStd.U64.Mul
import CodeLib.RustStd.U64.Div
import CodeLib.RustStd.U64.Rem
import CodeLib.RustStd.U64.BitAnd
import CodeLib.RustStd.U64.BitOr
import CodeLib.RustStd.U64.BitXor
import CodeLib.RustStd.U64.Not
import CodeLib.RustStd.U64.Shl
import CodeLib.RustStd.U64.Shr
import CodeLib.RustStd.Array.Basic
import CodeLib.RustStd.Array.Len
import CodeLib.RustStd.Array.IsEmpty
import CodeLib.RustStd.Array.SmallStep
import CodeLib.RustStd.Option
import CodeLib.Near.State
import CodeLib.Near.Env
import CodeLib.Near.Proof
import CodeLib.IEEE32.Exec
import CodeLib.SepLogic.WasmHeap
import CodeLib.SepLogic.WasmRules
import CodeLib.SepLogic.SmallStepLanguage
import CodeLib.SepLogic.SmallStepState
import CodeLib.SepLogic.SmallStepLifting
import CodeLib.SepLogic.SmallStepAdequacy

/-!
# CodeLib — umbrella import for downstream code

Generated `Program.lean` files (emitted by `lake exe verifier check`) and
hand-written `Spec.lean` siblings should `import CodeLib`, never the
interpreter directly. Today this is mostly a thin re-export of Wasm;
domain-specific spec helpers will live here as they accrete.
-/