Lua.lean

import Lua.Num.Decimal
import Lua.Num.DecimalBridge
import Lua.Num.DecimalFacts
import Lua.Bytecode.OpCode
import Lua.Bytecode.Syntax
import Lua.Bytecode.Semantics
import Lua.Bytecode.Exec
import Lua.Fragment
import Lua.FragmentSound
import Lua.Vm.Layout
import Lua.Vm.Image
import Lua.Vm.Repr
import Lua.Vm.Loaded
import Lua.Vm.Runtime
import Lua.Vm.Boot.Heap
import Lua.Vm.Boot.Gen.While
import Lua.Vm.Boot.Gen.F1Ops
import Lua.Vm.Boot.Witness.While
import Lua.Vm.Boot.Witness.F1Ops
import Lua.Vm.Host
import Lua.Vm.DecodeCheck
import Lua.Vm.Code
import Lua.Vm.Arms
import Lua.Vm.Sim
import Lua.Vm.Sim.Kit
import Lua.Vm.Sim.Fold
import Lua.StuckCases
import Lua.Vm.LayoutErr
import Lua.Vm.Sim.Stuck
import Lua.Vm.Sim.StuckErr
import Lua.Refinement
import Lua.Ast.Syntax
import Lua.Ast.Rulebook
import Lua.Ast.Semantics
import Lua.Ast.Exec
import Lua.Ast.Determinism
import Lua.Theorems
import Lua.Programs.While
import Lua.Programs.PrintPrint
import Lua.Programs.F1Ops
import Lua.Programs.F1bBits
import Lua.Programs.F4Strlite
import Lua.Programs.Validation
import Lua.Programs.Supported
import Lua.Programs.F1OpsAst
import Lua.Programs.F1SrcAst
import Lua.Programs.WhileAst
import Lua.Programs.F1bBitsAst
import Lua.Programs.F4StrliteAst
import Lua.Programs.F4StrliteSrc
import Lua.Programs.F1Src
import Lua.Programs.EscStrflt
import Lua.Programs.EscForstr
import Lua.Programs.EscUnmflt
import Lua.Programs.Escape
import Lua.Programs.EscStrfltAst
import Lua.Programs.EscForstrAst
import Lua.Programs.EscUnmfltAst
import Lua.Compile.TV
import Lua.Compile.Corpus
import Lua.Os.HtifFs
import Lua.Os.Htif
import Lua.Os.HtifTraces
import Lua.Num.F64
import Lua.Num.Pow
import Lua.Num.PowFacts
import Lua.Num.Arith

/-! Lua 5.4 on bare-metal RV64: bytecode semantics, VM representation, and
the Layer A / Layer B / end-to-end statements. See README.md, PHASES.md. -/