diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
new file mode 100644
index 00000000..8032d0b6
--- /dev/null
+++ b/.github/workflows/lean.yml
@@ -0,0 +1,108 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
+name: lean
+
+on:
+  push:
+    branches: [ "main" ]
+    paths:
+      - "formal/**"
+      - ".github/workflows/lean.yml"
+  pull_request:
+    branches: [ "main" ]
+    paths:
+      - "formal/**"
+      - ".github/workflows/lean.yml"
+
+env:
+  # elan (the Lean toolchain manager) reads `formal/lean-toolchain` to decide
+  # which pinned Lean release to install; this only sets its install location.
+  ELAN_HOME: ${{ github.workspace }}/.elan
+
+# This workflow only checks out code, installs a pinned Lean/elan toolchain,
+# fetches precompiled Mathlib caches, and builds/checks the `formal/`
+# formalization. It never writes to the repository, so restrict the
+# GITHUB_TOKEN to read-only access to repository contents.
+permissions:
+  contents: read
+
+jobs:
+  build:
+    name: lean (formal/)
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install elan (pinned release, pinned to formal/lean-toolchain)
+        shell: bash
+        run: |
+          set -euxo pipefail
+          toolchain="$(cat formal/lean-toolchain)"
+          test -n "$toolchain"
+
+          # Download a specific, pinned elan release binary instead of piping
+          # the mutable `elan/master` install script into bash, and verify its
+          # integrity before executing it (mirroring how
+          # .github/workflows/verus.yml pins and hash-checks the Verus release).
+          elan_version=4.2.4
+          asset_url="https://github.com/leanprover/elan/releases/download/v${elan_version}/elan-x86_64-unknown-linux-gnu.tar.gz"
+          asset_sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+          curl -fsSL "$asset_url" -o elan.tar.gz
+          echo "${asset_sha256}  elan.tar.gz" | sha256sum --check --strict
+
+          tar -xzf elan.tar.gz
+          chmod +x elan-init
+          ./elan-init -y --default-toolchain "$toolchain"
+          echo "$ELAN_HOME/bin" >> "$GITHUB_PATH"
+
+      - name: Cache Lake build artifacts and Mathlib cache
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: |
+            formal/.lake
+          # Keyed on the manifest (exact pinned dependency revisions) and the
+          # toolchain version, so a Mathlib/Batteries bump invalidates the
+          # cache instead of silently reusing stale `.olean` files.
+          key: lean-lake-${{ runner.os }}-${{ hashFiles('formal/lean-toolchain', 'formal/lake-manifest.json') }}
+          restore-keys: |
+            lean-lake-${{ runner.os }}-
+
+      - name: Fetch dependencies and precompiled Mathlib cache
+        working-directory: formal
+        shell: bash
+        run: |
+          set -euxo pipefail
+          lake --version
+          # `lake exe cache get` resolves/fetches the pinned dependencies from
+          # lake-manifest.json (Mathlib, Batteries, ...) and then downloads
+          # their prebuilt `.olean` files instead of compiling them from
+          # source, which would otherwise take a very long time. Failures are
+          # tolerated here (e.g. no cache entry for a brand-new revision);
+          # `lake build` below falls back to compiling anything missing.
+          lake exe cache get || echo "Mathlib cache fetch skipped/unavailable; continuing to lake build."
+
+      - name: Build the Regorus formalization
+        working-directory: formal
+        shell: bash
+        run: |
+          set -euxo pipefail
+          # `@[default_target]` is only on the `Regorus` library, so a bare
+          # `lake build` never builds/typechecks the `regorusFormal`
+          # executable (whose root is `Main.lean`). Build it explicitly; it
+          # imports `Regorus`, so this still builds/checks the full library.
+          lake build regorusFormal
+
+      - name: Reject unproven placeholders (sorry/admit)
+        working-directory: formal
+        shell: bash
+        run: |
+          set -euxo pipefail
+          # `lake build` succeeds even in the presence of `sorry`, which only
+          # produces a warning. Fail CI explicitly so the formalization can
+          # never merge with an unproven theorem hiding behind a warning.
+          if grep -rnE '\bsorry\b|\badmit\b' Regorus Main.lean Regorus.lean; then
+            echo "::error::Found sorry/admit in the Lean formalization; all theorems must be fully proved."
+            exit 1
+          fi
+          echo "No sorry/admit found."
diff --git a/formal/.gitignore b/formal/.gitignore
new file mode 100644
index 00000000..19122806
--- /dev/null
+++ b/formal/.gitignore
@@ -0,0 +1,9 @@
+# Local Lean/Lake toolchain installation (elan, lean, lake binaries) — not
+# part of the formalization source; contributors should install their own
+# toolchain via elan using the pinned `lean-toolchain` file.
+.lean-tools/
+
+# Lake build artifacts and downloaded dependency packages (Mathlib, Batteries,
+# etc.) — reproducible from lakefile.lean + lake-manifest.json via `lake build`.
+.lake/
+build/
diff --git a/formal/Main.lean b/formal/Main.lean
new file mode 100644
index 00000000..22ed2412
--- /dev/null
+++ b/formal/Main.lean
@@ -0,0 +1,4 @@
+import Regorus
+
+def main : IO Unit :=
+  IO.println "Regorus Value formalization"
diff --git a/formal/Regorus.lean b/formal/Regorus.lean
new file mode 100644
index 00000000..b1952a6f
--- /dev/null
+++ b/formal/Regorus.lean
@@ -0,0 +1,8 @@
+import Regorus.Value.RawNumber
+import Regorus.Value.RegoNumber
+import Regorus.Value.RawValue
+import Regorus.Value.Value
+import Regorus.Value.Canonical
+import Regorus.Value.Truth
+import Regorus.Value.SourceValue
+import Regorus.RVM
diff --git a/formal/Regorus/RVM.lean b/formal/Regorus/RVM.lean
new file mode 100644
index 00000000..03fc5798
--- /dev/null
+++ b/formal/Regorus/RVM.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.RVM.Bytecode
+import Regorus.RVM.Program
+import Regorus.RVM.State
+import Regorus.RVM.Step
diff --git a/formal/Regorus/RVM/Bytecode.lean b/formal/Regorus/RVM/Bytecode.lean
new file mode 100644
index 00000000..661376fb
--- /dev/null
+++ b/formal/Regorus/RVM/Bytecode.lean
@@ -0,0 +1,196 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+/-!
+# RVM bytecode
+
+The instruction constructors mirror `src/rvm/instructions/mod.rs` as of the
+RVM phase-one model.  Register and table indices use mathematical naturals
+rather than the Rust representation widths (`u8` and `u16`); program
+well-formedness will impose those finite bounds in a later phase.
+
+Only the object, array, and set creation parameter tables are represented
+below.  The remaining parameter-bearing instructions are retained with their
+real table index operand, but their parameter records and semantics are
+deliberately deferred.
+-/
+
+namespace Regorus.RVM
+
+abbrev Reg := Nat
+abbrev PC := Nat
+abbrev LiteralIdx := Nat
+abbrev ParamIdx := Nat
+abbrev RuleIdx := Nat
+
+inductive LoopMode where
+  | Any
+  | Every
+  | ForEach
+  deriving Repr, DecidableEq
+
+inductive ComprehensionMode where
+  | Set
+  | Array
+  | Object
+  deriving Repr, DecidableEq
+
+inductive GuardMode where
+  | Not
+  | Condition
+  | NotUndefined
+  deriving Repr, DecidableEq
+
+inductive PolicyOp where
+  | Equals
+  | NotEquals
+  | Greater
+  | GreaterOrEquals
+  | Less
+  | LessOrEquals
+  | In
+  | NotIn
+  | Contains
+  | NotContains
+  | ContainsKey
+  | NotContainsKey
+  | Like
+  | NotLike
+  | Match
+  | NotMatch
+  | MatchInsensitively
+  | NotMatchInsensitively
+  | Exists
+  | ValueConditionGuard
+  | Not
+  deriving Repr, DecidableEq
+
+inductive LogicalBlockMode where
+  | AllOf
+  | AnyOf
+  deriving Repr, DecidableEq
+
+inductive LiteralOrRegister where
+  | Literal (index : LiteralIdx)
+  | Register (register : Reg)
+  deriving Repr, DecidableEq
+
+/--
+The full current Rust opcode enum.  Constructors outside the phase-one core
+retain their actual immediate operands so programs can be represented
+faithfully even though `step` reports them as unimplemented.
+-/
+inductive Instruction where
+  | Load (dest : Reg) (literalIdx : LiteralIdx)
+  | LoadTrue (dest : Reg)
+  | LoadFalse (dest : Reg)
+  | LoadNull (dest : Reg)
+  | LoadBool (dest : Reg) (value : Bool)
+  | LoadData (dest : Reg)
+  | LoadInput (dest : Reg)
+  | LoadContext (dest : Reg)
+  | LoadMetadata (dest : Reg)
+  | Move (dest src : Reg)
+  | Add (dest left right : Reg)
+  | Sub (dest left right : Reg)
+  | Mul (dest left right : Reg)
+  | Div (dest left right : Reg)
+  | Mod (dest left right : Reg)
+  | Eq (dest left right : Reg)
+  | Ne (dest left right : Reg)
+  | Lt (dest left right : Reg)
+  | Le (dest left right : Reg)
+  | Gt (dest left right : Reg)
+  | Ge (dest left right : Reg)
+  | And (dest left right : Reg)
+  | Or (dest left right : Reg)
+  | Not (dest operand : Reg)
+  | BuiltinCall (paramsIndex : ParamIdx)
+  | HostAwait (dest arg id : Reg)
+  | FunctionCall (paramsIndex : ParamIdx)
+  | Return (value : Reg)
+  | ObjectSet (obj key value : Reg)
+  | ObjectCreate (paramsIndex : ParamIdx)
+  | Index (dest container key : Reg)
+  | IndexLiteral (dest container : Reg) (literalIdx : LiteralIdx)
+  | ChainedIndex (paramsIndex : ParamIdx)
+  | ArrayNew (dest : Reg)
+  | ArrayPush (arr value : Reg)
+  | ArrayPushDefined (arr value : Reg)
+  | ArrayCreate (paramsIndex : ParamIdx)
+  | SetNew (dest : Reg)
+  | SetAdd (set value : Reg)
+  | SetCreate (paramsIndex : ParamIdx)
+  | Contains (dest collection value : Reg)
+  | Count (dest collection : Reg)
+  | AssertEq (left right : Reg)
+  | Guard (register : Reg) (mode : GuardMode)
+  | ReturnUndefinedIfNotTrue (condition : Reg)
+  | CoalesceUndefinedToNull (register : Reg)
+  | LoopStart (paramsIndex : ParamIdx)
+  | LoopNext (bodyStart loopEnd : PC)
+  | CallRule (dest : Reg) (ruleIndex : RuleIdx)
+  | RuleInit (resultReg : Reg) (ruleIndex : RuleIdx)
+  | VirtualDataDocumentLookup (paramsIndex : ParamIdx)
+  | DestructuringSuccess
+  | RuleReturn
+  | Halt
+  | ComprehensionBegin (paramsIndex : ParamIdx)
+  | ComprehensionYield (valueReg : Reg) (keyReg : Option Reg)
+  | ComprehensionEnd
+  | PolicyCondition (dest left right : Reg) (op : PolicyOp)
+  | LogicalBlockStart (mode : LogicalBlockMode) (result : Reg) (endPC : PC)
+  | AllOfNext (check result : Reg) (endPC : PC)
+  | AnyOfNext (check result : Reg) (endPC : PC)
+  | LogicalBlockEnd (mode : LogicalBlockMode) (result : Reg)
+  deriving Repr
+
+namespace Instruction
+
+/--
+Compatibility spelling for the former `AssertCondition` opcode.  Rust now
+encodes it as `Guard { mode: Condition }`.
+-/
+def AssertCondition (condition : Reg) : Instruction :=
+  .Guard condition .Condition
+
+/--
+Compatibility spelling for the former `AssertNotUndefined` opcode.  Rust now
+encodes it as `Guard { mode: NotUndefined }`.
+-/
+def AssertNotUndefined (register : Reg) : Instruction :=
+  .Guard register .NotUndefined
+
+end Instruction
+
+structure ObjectCreateParams where
+  dest : Reg
+  templateLiteralIdx : LiteralIdx
+  literalKeyFields : List (LiteralIdx × Reg)
+  fields : List (Reg × Reg)
+  deriving Repr, DecidableEq
+
+structure ArrayCreateParams where
+  dest : Reg
+  elements : List Reg
+  deriving Repr, DecidableEq
+
+structure SetCreateParams where
+  dest : Reg
+  elements : List Reg
+  deriving Repr, DecidableEq
+
+/--
+The phase-one portion of Rust's `InstructionData`.  Tables for loops, calls,
+virtual lookup, chained indexing, and comprehensions are deferred with those
+instructions.
+-/
+structure InstructionData where
+  objectCreateParams : List ObjectCreateParams := []
+  arrayCreateParams : List ArrayCreateParams := []
+  setCreateParams : List SetCreateParams := []
+  deriving Repr, DecidableEq
+
+end Regorus.RVM
diff --git a/formal/Regorus/RVM/Program.lean b/formal/Regorus/RVM/Program.lean
new file mode 100644
index 00000000..9dbbb2f2
--- /dev/null
+++ b/formal/Regorus/RVM/Program.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.RVM.Bytecode
+import Regorus.Value.Value
+
+/-!
+# Executable RVM program
+
+This is the executable phase-one projection of Rust's `Program`.  It retains
+the instruction stream, literal pool, relevant instruction parameter tables,
+and entry points.  Rule metadata, builtin dispatch, source spans, compiler
+metadata, virtual-data caches, register-window sizing, and serialization flags
+are deferred until their instructions enter the formalized subset.
+-/
+
+namespace Regorus.RVM
+
+structure Program where
+  instructions : List Instruction := []
+  literals : List Regorus.Value := []
+  instructionData : InstructionData := {}
+  entryPoints : List (String × PC) := []
+  mainEntryPoint : PC := 0
+  deriving Repr
+
+end Regorus.RVM
diff --git a/formal/Regorus/RVM/State.lean b/formal/Regorus/RVM/State.lean
new file mode 100644
index 00000000..45708466
--- /dev/null
+++ b/formal/Regorus/RVM/State.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.RVM.Program
+
+/-!
+# Core RVM state
+
+The Rust VM has additional frame, loop, comprehension, cache, suspension, and
+resource-accounting state.  Those components are intentionally absent here:
+this state is the complete state needed by the non-control-flow phase-one
+instruction subset.
+
+Rust exposes several specialized register/type errors.  The phase-one model
+keeps bounds failures precise and consolidates collection and arithmetic type
+failures under `TypeMismatch`.
+-/
+
+namespace Regorus.RVM
+
+inductive VMError where
+  | RegisterOutOfBounds (register : Reg)
+  | LiteralIndexOutOfBounds (index : LiteralIdx)
+  | ParameterIndexOutOfBounds (table : String) (index : ParamIdx)
+  | ProgramCounterOutOfBounds (pc : PC)
+  | TypeMismatch (expected : String)
+  | DivisionByZero
+  | NonIntegralModulo
+  | AssertionFailed
+  | Unimplemented (instruction : String)
+  deriving Repr, DecidableEq
+
+inductive VMStatus where
+  | Running
+  | Halted (value : Regorus.Value)
+  | Returned (value : Regorus.Value)
+  | Error (error : VMError)
+  | Stuck (reason : String)
+  deriving Repr, DecidableEq
+
+structure VMState where
+  registers : List Regorus.Value
+  pc : PC
+  program : Program
+  data : Regorus.Value
+  input : Regorus.Value
+  status : VMStatus := .Running
+  deriving Repr
+
+def readRegister (state : VMState) (register : Reg) :
+    Except VMError Regorus.Value :=
+  match state.registers.get? register with
+  | some value => .ok value
+  | none => .error (.RegisterOutOfBounds register)
+
+def writeRegister (state : VMState) (register : Reg) (value : Regorus.Value) :
+    Except VMError VMState :=
+  if register < state.registers.length then
+    .ok { state with registers := state.registers.set register value }
+  else
+    .error (.RegisterOutOfBounds register)
+
+def readLiteral (state : VMState) (index : LiteralIdx) :
+    Except VMError Regorus.Value :=
+  match state.program.literals.get? index with
+  | some value => .ok value
+  | none => .error (.LiteralIndexOutOfBounds index)
+
+def fetchInstruction (state : VMState) : Except VMError Instruction :=
+  match state.program.instructions.get? state.pc with
+  | some instruction => .ok instruction
+  | none => .error (.ProgramCounterOutOfBounds state.pc)
+
+end Regorus.RVM
diff --git a/formal/Regorus/RVM/Step.lean b/formal/Regorus/RVM/Step.lean
new file mode 100644
index 00000000..485d3d5c
--- /dev/null
+++ b/formal/Regorus/RVM/Step.lean
@@ -0,0 +1,640 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.RVM.State
+import Regorus.Value.Canonical
+import Regorus.Value.Truth
+
+/-!
+# Core RVM small-step semantics
+
+`step` is the total executable transition function.  A running state either
+executes its current instruction, enters a terminal state, or records an
+explicit error; terminal states are fixed points.  `Step` is the corresponding
+proof-facing relation.
+
+Arithmetic is strict in `Undefined`.  This phase uses exact rational
+arithmetic, reports division by zero explicitly, and requires integral modulo
+operands.  The full Rust VM's configurable non-strict arithmetic-error mode is
+deferred.
+-/
+
+namespace Regorus.RVM
+
+open Regorus
+
+private def advance (state : VMState) : VMState :=
+  { state with pc := state.pc + 1 }
+
+private def writeAndAdvance (state : VMState) (dest : Reg) (value : Value) :
+    Except VMError VMState :=
+  match writeRegister state dest value with
+  | .ok state' => .ok (advance state')
+  | .error error => .error error
+
+private def readRegisters (state : VMState) : List Reg → Except VMError (List Value)
+  | [] => .ok []
+  | register :: registers => do
+      let value ← readRegister state register
+      let values ← readRegisters state registers
+      pure (value :: values)
+
+private def strictLift₂
+    (operation : Value → Value → Except VMError Value)
+    (left right : Value) : Except VMError Value :=
+  match left, right with
+  | .Undefined, _ | _, .Undefined =>
+      .ok (Regorus.lift₂ (fun _ _ => .Undefined) left right)
+  | _, _ => operation left right
+
+private def evalAdd : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Number left, .Number right => .ok (.Number (left + right))
+    | _, _ => .error (.TypeMismatch "Add expects two numbers")
+
+private def evalSub : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Number left, .Number right => .ok (.Number (left - right))
+    | .Set left, .Set right =>
+        .ok (Value.mkSet (left.filter fun value => value ∉ right))
+    | _, _ => .error (.TypeMismatch "Sub expects two numbers or two sets")
+
+private def evalMul : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Number left, .Number right => .ok (.Number (left * right))
+    | _, _ => .error (.TypeMismatch "Mul expects two numbers")
+
+private def evalDiv : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Number left, .Number right =>
+        match RegoNumber.div? left right with
+        | some quotient => .ok (.Number quotient)
+        | none => .error .DivisionByZero
+    | _, _ => .error (.TypeMismatch "Div expects two numbers")
+
+private def evalMod : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Number left, .Number right =>
+        match left.toInt?, right.toInt? with
+        | some _, some 0 => .error .DivisionByZero
+        | some leftInt, some rightInt =>
+            .ok (.Number (RegoNumber.ofInt (Int.tmod leftInt rightInt)))
+        | _, _ => .error .NonIntegralModulo
+    | _, _ => .error (.TypeMismatch "Mod expects two numbers")
+
+private def evalEq : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right => .ok (.Bool (decide (left = right)))
+
+private def evalNe : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right => .ok (.Bool (decide (left ≠ right)))
+
+/-- Ordered comparisons in the modeled strict mode reject operands of
+different value kinds instead of falling back to heterogeneous ordering. -/
+private def requireSameKind
+    (left right : Value) (result : Bool) : Except VMError Value :=
+  if left.kindRank = right.kindRank then
+    .ok (.Bool result)
+  else
+    .error (.TypeMismatch "cannot compare values of different types")
+
+private def evalLt : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right =>
+    requireSameKind left right (decide (Value.compareValue left right = .lt))
+
+private def evalLe : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right =>
+    requireSameKind left right (decide (Value.compareValue left right ≠ .gt))
+
+private def evalGt : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right =>
+    requireSameKind left right (decide (Value.compareValue left right = .gt))
+
+private def evalGe : Value → Value → Except VMError Value :=
+  strictLift₂ fun left right =>
+    requireSameKind left right (decide (Value.compareValue left right ≠ .lt))
+
+/-- Strict-mode `And`/`Or` accept Boolean operands only; the Rust VM's
+`to_bool` helper additionally coerces `Null` in non-strict mode only, which
+this phase does not model (see the module docstring). -/
+private def evalAnd : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Bool left, .Bool right => .ok (.Bool (left && right))
+    | _, _ => .error (.TypeMismatch "And expects two booleans")
+
+private def evalOr : Value → Value → Except VMError Value :=
+  strictLift₂ fun
+    | .Bool left, .Bool right => .ok (.Bool (left || right))
+    | _, _ => .error (.TypeMismatch "Or expects two booleans")
+
+private def executeBinary
+    (operation : Value → Value → Except VMError Value)
+    (state : VMState) (dest left right : Reg) : Except VMError VMState := do
+  let leftValue ← readRegister state left
+  let rightValue ← readRegister state right
+  let result ← operation leftValue rightValue
+  writeAndAdvance state dest result
+
+private def indexValue (container key : Value) : Value :=
+  match container with
+  | .Object fields =>
+      match fields.find? fun field => field.1 == key with
+      | some field => field.2
+      | none => .Undefined
+  | .Set elements =>
+      if key ∈ elements then key else .Undefined
+  | .Array elements =>
+      match key with
+      | .Number number =>
+          match number.toInt? with
+          | some index =>
+              if 0 ≤ index then
+                (elements.get? index.toNat).getD .Undefined
+              else
+                .Undefined
+          | none => .Undefined
+      | _ => .Undefined
+  | _ => .Undefined
+
+private def containsValue (collection value : Value) : Value :=
+  .Bool <| match collection with
+    | .Set elements | .Array elements => value ∈ elements
+    | .Object fields => fields.any fun field => field.2 == value
+    | _ => false
+
+private def countValue : Value → Value
+  | .Array elements | .Set elements =>
+      .Number (RegoNumber.ofInt (Int.ofNat elements.length))
+  | .Object fields =>
+      .Number (RegoNumber.ofInt (Int.ofNat fields.length))
+  | _ => .Undefined
+
+private def readLiteralFields
+    (state : VMState) :
+    List (LiteralIdx × Reg) → Except VMError (List (Value × Value))
+  | [] => .ok []
+  | (literalIdx, valueReg) :: fields => do
+      let key ← readLiteral state literalIdx
+      let value ← readRegister state valueReg
+      let rest ← readLiteralFields state fields
+      pure ((key, value) :: rest)
+
+private def readDynamicFields
+    (state : VMState) : List (Reg × Reg) → Except VMError (List (Value × Value))
+  | [] => .ok []
+  | (keyReg, valueReg) :: fields => do
+      let key ← readRegister state keyReg
+      let value ← readRegister state valueReg
+      let rest ← readDynamicFields state fields
+      pure ((key, value) :: rest)
+
+private def hasUndefinedField (fields : List (Value × Value)) : Bool :=
+  fields.any fun field =>
+    field.1 == Value.Undefined || field.2 == Value.Undefined
+
+private def executeObjectCreate
+    (state : VMState) (paramsIndex : ParamIdx) : Except VMError VMState := do
+  let params ←
+    match state.program.instructionData.objectCreateParams.get? paramsIndex with
+    | some params => .ok params
+    | none => .error (.ParameterIndexOutOfBounds "objectCreateParams" paramsIndex)
+  let literalFields ← readLiteralFields state params.literalKeyFields
+  let fields ← readDynamicFields state params.fields
+  if hasUndefinedField literalFields || hasUndefinedField fields then
+    writeAndAdvance state params.dest .Undefined
+  else
+    let template ← readLiteral state params.templateLiteralIdx
+    match template with
+    | .Object entries =>
+        writeAndAdvance state params.dest
+          (Value.mkObject (entries ++ literalFields ++ fields))
+    | _ => .error (.TypeMismatch "ObjectCreate template must be an object")
+
+private def executeArrayCreate
+    (state : VMState) (paramsIndex : ParamIdx) : Except VMError VMState := do
+  let params ←
+    match state.program.instructionData.arrayCreateParams.get? paramsIndex with
+    | some params => .ok params
+    | none => .error (.ParameterIndexOutOfBounds "arrayCreateParams" paramsIndex)
+  let values ← readRegisters state params.elements
+  if Value.Undefined ∈ values then
+    writeAndAdvance state params.dest .Undefined
+  else
+    writeAndAdvance state params.dest (.Array values)
+
+private def executeSetCreate
+    (state : VMState) (paramsIndex : ParamIdx) : Except VMError VMState := do
+  let params ←
+    match state.program.instructionData.setCreateParams.get? paramsIndex with
+    | some params => .ok params
+    | none => .error (.ParameterIndexOutOfBounds "setCreateParams" paramsIndex)
+  let values ← readRegisters state params.elements
+  if Value.Undefined ∈ values then
+    writeAndAdvance state params.dest .Undefined
+  else
+    writeAndAdvance state params.dest (Value.mkSet values)
+
+/-- Execute one already-fetched instruction. -/
+def executeInstruction (instruction : Instruction) (state : VMState) :
+    Except VMError VMState := do
+  match instruction with
+  | .Load dest literalIdx =>
+      let value ← readLiteral state literalIdx
+      writeAndAdvance state dest value
+  | .LoadTrue dest => writeAndAdvance state dest (.Bool true)
+  | .LoadFalse dest => writeAndAdvance state dest (.Bool false)
+  | .LoadNull dest => writeAndAdvance state dest .Null
+  | .LoadBool dest value => writeAndAdvance state dest (.Bool value)
+  | .LoadData dest => writeAndAdvance state dest state.data
+  | .LoadInput dest => writeAndAdvance state dest state.input
+  | .Move dest src =>
+      let value ← readRegister state src
+      writeAndAdvance state dest value
+  | .Add dest left right => executeBinary evalAdd state dest left right
+  | .Sub dest left right => executeBinary evalSub state dest left right
+  | .Mul dest left right => executeBinary evalMul state dest left right
+  | .Div dest left right => executeBinary evalDiv state dest left right
+  | .Mod dest left right => executeBinary evalMod state dest left right
+  | .Eq dest left right => executeBinary evalEq state dest left right
+  | .Ne dest left right => executeBinary evalNe state dest left right
+  | .Lt dest left right => executeBinary evalLt state dest left right
+  | .Le dest left right => executeBinary evalLe state dest left right
+  | .Gt dest left right => executeBinary evalGt state dest left right
+  | .Ge dest left right => executeBinary evalGe state dest left right
+  | .And dest left right => executeBinary evalAnd state dest left right
+  | .Or dest left right => executeBinary evalOr state dest left right
+  | .Not dest operand =>
+      let value ← readRegister state operand
+      writeAndAdvance state dest (Regorus.notRvm value)
+  | .Guard register .Condition =>
+      let value ← readRegister state register
+      if Regorus.guardCondition value then
+        pure (advance state)
+      else
+        .error .AssertionFailed
+  | .Guard register .NotUndefined =>
+      let value ← readRegister state register
+      if Regorus.guardNotUndefined value then
+        pure (advance state)
+      else
+        .error .AssertionFailed
+  | .Guard register .Not =>
+      let value ← readRegister state register
+      if Regorus.isTruthy (Regorus.notRvm value) then
+        pure (advance state)
+      else
+        .error .AssertionFailed
+  | .ObjectSet obj key value =>
+      let keyValue ← readRegister state key
+      let fieldValue ← readRegister state value
+      let objectValue ← readRegister state obj
+      match objectValue with
+      | .Object fields =>
+          writeAndAdvance state obj
+            (Value.mkObject (fields ++ [(keyValue, fieldValue)]))
+      | _ => .error (.TypeMismatch "ObjectSet expects an object")
+  | .ObjectCreate paramsIndex => executeObjectCreate state paramsIndex
+  | .ArrayNew dest => writeAndAdvance state dest (.Array [])
+  | .ArrayPush arr value =>
+      let element ← readRegister state value
+      let arrayValue ← readRegister state arr
+      match arrayValue with
+      | .Array elements =>
+          writeAndAdvance state arr (.Array (elements ++ [element]))
+      | _ => .error (.TypeMismatch "ArrayPush expects an array")
+  | .ArrayCreate paramsIndex => executeArrayCreate state paramsIndex
+  | .SetNew dest => writeAndAdvance state dest (Value.mkSet [])
+  | .SetAdd set value =>
+      let element ← readRegister state value
+      let setValue ← readRegister state set
+      match setValue with
+      | .Set elements =>
+          writeAndAdvance state set (Value.mkSet (element :: elements))
+      | _ => .error (.TypeMismatch "SetAdd expects a set")
+  | .SetCreate paramsIndex => executeSetCreate state paramsIndex
+  | .Index dest container key =>
+      let containerValue ← readRegister state container
+      let keyValue ← readRegister state key
+      writeAndAdvance state dest (indexValue containerValue keyValue)
+  | .IndexLiteral dest container literalIdx =>
+      let containerValue ← readRegister state container
+      let keyValue ← readLiteral state literalIdx
+      writeAndAdvance state dest (indexValue containerValue keyValue)
+  | .Contains dest collection value =>
+      let collectionValue ← readRegister state collection
+      let soughtValue ← readRegister state value
+      writeAndAdvance state dest (containsValue collectionValue soughtValue)
+  | .Count dest collection =>
+      let collectionValue ← readRegister state collection
+      writeAndAdvance state dest (countValue collectionValue)
+  | .Return value =>
+      let result ← readRegister state value
+      pure { state with status := .Returned result }
+  | .Halt =>
+      let result ← readRegister state 0
+      pure { state with status := .Halted result }
+  | other => .error (.Unimplemented (reprStr other))
+
+/--
+Execute one small step.  Errors are data in the resulting state, and terminal
+states are fixed points, making the function total.
+-/
+def step (state : VMState) : VMState :=
+  match state.status with
+  | .Running =>
+      match fetchInstruction state with
+      | .error error => { state with status := .Error error }
+      | .ok instruction =>
+          match executeInstruction instruction state with
+          | .ok state' => state'
+          | .error error => { state with status := .Error error }
+  | _ => state
+
+/-- Relational presentation of the executable one-step transition. -/
+inductive Step : VMState → VMState → Prop where
+  | execute {before after : VMState} (result : step before = after) :
+      Step before after
+
+theorem step_iff_Step (before after : VMState) :
+    Step before after ↔ step before = after := by
+  constructor
+  · intro transition
+    cases transition with
+    | execute result => exact result
+  · exact Step.execute
+
+theorem Step.deterministic {before after₁ after₂ : VMState}
+    (first : Step before after₁) (second : Step before after₂) :
+    after₁ = after₂ := by
+  rw [step_iff_Step] at first second
+  exact first.symm.trans second
+
+private theorem getElem?_set_ne
+    (registers : List Value) (dest other : Reg) (value : Value)
+    (different : other ≠ dest) :
+    (registers.set dest value)[other]? = registers[other]? := by
+  rw [List.getElem?_set]
+  simp [Ne.symm different]
+
+theorem writeAndAdvance_frame
+    {state state' : VMState} {dest other : Reg} {value : Value}
+    (written : writeAndAdvance state dest value = .ok state')
+    (different : other ≠ dest) :
+    state'.registers[other]? = state.registers[other]? := by
+  by_cases inBounds : dest < state.registers.length
+  · simp [writeAndAdvance, writeRegister, inBounds] at written
+    rw [← written]
+    exact getElem?_set_ne state.registers dest other value different
+  · simp [writeAndAdvance, writeRegister, inBounds] at written
+
+theorem executeInstruction_load_frame
+    {state state' : VMState} {dest other : Reg} {literalIdx : LiteralIdx}
+    (executed : executeInstruction (.Load dest literalIdx) state = .ok state')
+    (different : other ≠ dest) :
+    state'.registers[other]? = state.registers[other]? := by
+  cases literalRead : readLiteral state literalIdx with
+  | error error =>
+      simp [executeInstruction, literalRead, Bind.bind, Except.bind] at executed
+  | ok value =>
+      rw [show executeInstruction (.Load dest literalIdx) state =
+        writeAndAdvance state dest value by
+          simp [executeInstruction, literalRead, Bind.bind, Except.bind]] at executed
+      exact writeAndAdvance_frame executed different
+
+theorem executeInstruction_move_frame
+    {state state' : VMState} {dest src other : Reg}
+    (executed : executeInstruction (.Move dest src) state = .ok state')
+    (different : other ≠ dest) :
+    state'.registers[other]? = state.registers[other]? := by
+  cases sourceRead : readRegister state src with
+  | error error =>
+      simp [executeInstruction, sourceRead, Bind.bind, Except.bind] at executed
+  | ok value =>
+      rw [show executeInstruction (.Move dest src) state =
+        writeAndAdvance state dest value by
+          simp [executeInstruction, sourceRead, Bind.bind, Except.bind]] at executed
+      exact writeAndAdvance_frame executed different
+
+private theorem executeBinary_frame
+    (operation : Value → Value → Except VMError Value)
+    {state state' : VMState} {dest left right other : Reg}
+    (executed : executeBinary operation state dest left right = .ok state')
+    (different : other ≠ dest) :
+    state'.registers[other]? = state.registers[other]? := by
+  cases leftRead : readRegister state left with
+  | error error =>
+      simp [executeBinary, leftRead, Bind.bind, Except.bind] at executed
+  | ok leftValue =>
+      cases rightRead : readRegister state right with
+      | error error =>
+          simp [executeBinary, leftRead, rightRead, Bind.bind, Except.bind] at executed
+      | ok rightValue =>
+          cases operationResult : operation leftValue rightValue with
+          | error error =>
+              simp [executeBinary, leftRead, rightRead, operationResult,
+                Bind.bind, Except.bind] at executed
+          | ok result =>
+              rw [show executeBinary operation state dest left right =
+                writeAndAdvance state dest result by
+                  simp [executeBinary, leftRead, rightRead, operationResult,
+                    Bind.bind, Except.bind]] at executed
+              exact writeAndAdvance_frame executed different
+
+theorem executeInstruction_add_frame
+    {state state' : VMState} {dest left right other : Reg}
+    (executed : executeInstruction (.Add dest left right) state = .ok state')
+    (different : other ≠ dest) :
+    state'.registers[other]? = state.registers[other]? := by
+  exact executeBinary_frame evalAdd (by simpa [executeInstruction] using executed)
+    different
+
+theorem executeInstruction_add_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Add dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined := by
+  rcases rightBound with ⟨rightValue, rightValueEq⟩
+  have leftRead : readRegister state left = .ok .Undefined := by
+    simp [readRegister, leftBottom]
+  have rightRead : readRegister state right = .ok rightValue := by
+    simp [readRegister, rightValueEq]
+  have operationResult : evalAdd .Undefined rightValue = .ok .Undefined := by
+    simp [evalAdd, strictLift₂]
+  have result :
+      writeAndAdvance state dest .Undefined = .ok state' := by
+    simpa [executeInstruction, executeBinary, leftRead, rightRead,
+      operationResult, Bind.bind, Except.bind] using executed
+  have inBounds : dest < state.registers.length := by
+    by_contra outOfBounds
+    have errorResult :
+        writeAndAdvance state dest .Undefined =
+          .error (.RegisterOutOfBounds dest) := by
+      simp [writeAndAdvance, writeRegister, outOfBounds]
+    rw [errorResult] at result
+    contradiction
+  have stateEq :
+      advance { state with registers := state.registers.set dest .Undefined } =
+        state' := by
+    simpa [writeAndAdvance, writeRegister, inBounds] using result
+  rw [← stateEq]
+  change (state.registers.set dest .Undefined)[dest]? = some .Undefined
+  rw [List.getElem?_set]
+  simp [inBounds]
+
+theorem executeInstruction_binary_left_undefined
+    (operation : Value → Value → Except VMError Value)
+    (bottom : ∀ value, operation .Undefined value = .ok .Undefined)
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeBinary operation state dest left right = .ok state') :
+    state'.registers[dest]? = some .Undefined := by
+  rcases rightBound with ⟨rightValue, rightValueEq⟩
+  have leftRead : readRegister state left = .ok .Undefined := by
+    simp [readRegister, leftBottom]
+  have rightRead : readRegister state right = .ok rightValue := by
+    simp [readRegister, rightValueEq]
+  have result :
+      writeAndAdvance state dest .Undefined = .ok state' := by
+    simpa [executeBinary, leftRead, rightRead, bottom rightValue,
+      Bind.bind, Except.bind] using executed
+  have inBounds : dest < state.registers.length := by
+    by_contra outOfBounds
+    have errorResult :
+        writeAndAdvance state dest .Undefined =
+          .error (.RegisterOutOfBounds dest) := by
+      simp [writeAndAdvance, writeRegister, outOfBounds]
+    rw [errorResult] at result
+    contradiction
+  have stateEq :
+      advance { state with registers := state.registers.set dest .Undefined } =
+        state' := by
+    simpa [writeAndAdvance, writeRegister, inBounds] using result
+  rw [← stateEq]
+  change (state.registers.set dest .Undefined)[dest]? = some .Undefined
+  rw [List.getElem?_set]
+  simp [inBounds]
+
+theorem executeInstruction_sub_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Sub dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalSub
+    (by intro value; simp [evalSub, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_mul_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Mul dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalMul
+    (by intro value; simp [evalMul, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_div_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Div dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalDiv
+    (by intro value; simp [evalDiv, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_mod_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Mod dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalMod
+    (by intro value; simp [evalMod, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_eq_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Eq dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalEq
+    (by intro value; simp [evalEq, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_ne_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Ne dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalNe
+    (by intro value; simp [evalNe, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_lt_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Lt dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalLt
+    (by intro value; simp [evalLt, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_le_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Le dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalLe
+    (by intro value; simp [evalLe, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_gt_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Gt dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalGt
+    (by intro value; simp [evalGt, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_ge_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Ge dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalGe
+    (by intro value; simp [evalGe, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_and_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.And dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalAnd
+    (by intro value; simp [evalAnd, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+theorem executeInstruction_or_left_undefined
+    {state state' : VMState} {dest left right : Reg}
+    (leftBottom : state.registers[left]? = some .Undefined)
+    (rightBound : ∃ value, state.registers[right]? = some value)
+    (executed : executeInstruction (.Or dest left right) state = .ok state') :
+    state'.registers[dest]? = some .Undefined :=
+  executeInstruction_binary_left_undefined evalOr
+    (by intro value; simp [evalOr, strictLift₂])
+    leftBottom rightBound (by simpa [executeInstruction] using executed)
+
+end Regorus.RVM
diff --git a/formal/Regorus/Value/Canonical.lean b/formal/Regorus/Value/Canonical.lean
new file mode 100644
index 00000000..2987d608
--- /dev/null
+++ b/formal/Regorus/Value/Canonical.lean
@@ -0,0 +1,443 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Mathlib.Data.Multiset.Sort
+import Regorus.Value.Value
+
+/-!
+# Canonical unordered collections
+
+`Value.Set` and `Value.Object` store lists only as canonical representations
+of unordered mathematical collections.  Set inputs are deduplicated and
+sorted.  Object inputs use the same policy as repeated Rust `BTreeMap::insert`
+calls: the last value supplied for a key wins, after which entries are sorted
+by key (with the value comparison serving only as an unreachable tie-breaker
+between distinct retained keys).
+-/
+
+namespace Regorus.Value
+
+private theorem compareValue_eq_of_not_gt_not_gt {x y : Value}
+    (hxy : compareValue x y ≠ .gt) (hyx : compareValue y x ≠ .gt) :
+    compareValue x y = .eq := by
+  cases h : compareValue x y with
+  | lt =>
+      have hs := compareValue_swap x y
+      rw [h] at hs
+      exact False.elim (hyx (by simpa using hs.symm))
+  | eq => rfl
+  | gt => exact False.elim (hxy h)
+
+private theorem kindRank_le_of_compareValue_ne_gt {x y : Value}
+    (h : compareValue x y ≠ .gt) : x.kindRank ≤ y.kindRank := by
+  cases x <;> cases y <;>
+    simp [compareValue, kindRank, LinearOrder.compare_eq_compareOfLessAndEq,
+      compareOfLessAndEq] at h ⊢
+
+private theorem then_ne_gt_iff (a b : Ordering) :
+    a.then b ≠ .gt ↔ a ≠ .gt ∧ (a = .eq → b ≠ .gt) := by
+  cases a <;> cases b <;> decide
+
+private theorem compareValue_null :
+    compareValue .Null .Null = .eq := rfl
+
+private theorem compareValue_bool (x y : _root_.Bool) :
+    compareValue (.Bool x) (.Bool y) = compare x y := rfl
+
+private theorem compareValue_number (x y : RegoNumber) :
+    compareValue (.Number x) (.Number y) = compare x y := rfl
+
+private theorem compareValue_string (x y : _root_.String) :
+    compareValue (.String x) (.String y) = compare x y := rfl
+
+private theorem compareValue_array (xs ys : List Value) :
+    compareValue (.Array xs) (.Array ys) = compareList xs ys := rfl
+
+private theorem compareValue_set (xs ys : List Value) :
+    compareValue (.Set xs) (.Set ys) = compareList xs ys := rfl
+
+private theorem compareValue_object (xs ys : List (Value × Value)) :
+    compareValue (.Object xs) (.Object ys) = compareObject xs ys := rfl
+
+private theorem compareValue_undefined :
+    compareValue .Undefined .Undefined = .eq := rfl
+
+private theorem compareList_nil_left (ys : List Value) :
+    compareList [] ys = if ys = [] then .eq else .lt := by
+  cases ys <;> rfl
+
+private theorem compareList_cons_nil (x : Value) (xs : List Value) :
+    compareList (x :: xs) [] = .gt := rfl
+
+private theorem compareList_cons_cons (x y : Value) (xs ys : List Value) :
+    compareList (x :: xs) (y :: ys) =
+      (compareValue x y).then (compareList xs ys) := rfl
+
+private theorem compareObject_nil_left (ys : List (Value × Value)) :
+    compareObject [] ys = if ys = [] then .eq else .lt := by
+  cases ys <;> rfl
+
+private theorem compareObject_cons_nil
+    (x : Value × Value) (xs : List (Value × Value)) :
+    compareObject (x :: xs) [] = .gt := by
+  rcases x with ⟨k, v⟩
+  rfl
+
+private theorem compareObject_cons_cons
+    (x y : Value × Value) (xs ys : List (Value × Value)) :
+    compareObject (x :: xs) (y :: ys) =
+      (compareValue x.1 y.1).then
+        ((compareValue x.2 y.2).then (compareObject xs ys)) := by
+  rcases x with ⟨kx, vx⟩
+  rcases y with ⟨ky, vy⟩
+  rfl
+
+mutual
+  private theorem compareValue_le_trans (x y z : Value)
+      (hxy : compareValue x y ≠ .gt)
+      (hyz : compareValue y z ≠ .gt) :
+      compareValue x z ≠ .gt := by
+    have hrxy := kindRank_le_of_compareValue_ne_gt hxy
+    have hryz := kindRank_le_of_compareValue_ne_gt hyz
+    by_cases hr : x.kindRank < z.kindRank
+    · rw [compare_of_kindRank_lt hr]
+      decide
+    have hrxyEq : x.kindRank = y.kindRank := by omega
+    have hryzEq : y.kindRank = z.kindRank := by omega
+    cases x <;> cases y <;> cases z <;>
+      simp [kindRank] at hrxyEq hryzEq <;>
+      simp only [compareValue_null, compareValue_bool, compareValue_number,
+        compareValue_string, compareValue_array, compareValue_set,
+        compareValue_object, compareValue_undefined] at hxy hyz ⊢ <;>
+      first
+      | decide
+      | exact Batteries.TransCmp.le_trans (cmp := compare) hxy hyz
+      | exact compareList_le_trans _ _ _ hxy hyz
+      | exact compareObject_le_trans _ _ _ hxy hyz
+  termination_by sizeOf x + sizeOf y + sizeOf z
+  decreasing_by
+    all_goals subst_vars
+    all_goals simp_wf
+    all_goals omega
+
+  private theorem compareObject_le_trans :
+      ∀ (xs ys zs : List (Value × Value)),
+        compareObject xs ys ≠ .gt →
+        compareObject ys zs ≠ .gt →
+        compareObject xs zs ≠ .gt
+    | [], _, zs, _, _ => by cases zs <;> simp [compareObject_nil_left]
+    | x :: xs, [], _, hxy, _ => by
+        exact False.elim (hxy (compareObject_cons_nil x xs))
+    | _, y :: ys, [], _, hyz => by
+        exact False.elim (hyz (compareObject_cons_nil y ys))
+    | x :: xs, y :: ys, z :: zs, hxy, hyz => by
+        simp only [compareObject_cons_cons] at hxy hyz ⊢
+        rw [then_ne_gt_iff] at hxy hyz ⊢
+        simp only [then_ne_gt_iff] at hxy hyz ⊢
+        refine
+          ⟨compareValue_le_trans x.1 y.1 z.1 hxy.1 hyz.1, ?_⟩
+        intro hkxz
+        have hkxzEq : x.1 = z.1 :=
+          (compareValue_eq_eq_iff x.1 z.1).1 hkxz
+        have hyx : compareValue y.1 x.1 ≠ .gt := by
+          simpa [hkxzEq] using hyz.1
+        have hkxy : compareValue x.1 y.1 = .eq :=
+          compareValue_eq_of_not_gt_not_gt hxy.1 hyx
+        have hkxyEq : x.1 = y.1 :=
+          (compareValue_eq_eq_iff x.1 y.1).1 hkxy
+        have hkyzEq : y.1 = z.1 := hkxyEq.symm.trans hkxzEq
+        have hxy' := hxy.2 ((compareValue_eq_eq_iff x.1 y.1).2 hkxyEq)
+        have hyz' := hyz.2 ((compareValue_eq_eq_iff y.1 z.1).2 hkyzEq)
+        refine
+          ⟨compareValue_le_trans x.2 y.2 z.2 hxy'.1 hyz'.1, ?_⟩
+        intro hvxz
+        have hvxzEq : x.2 = z.2 :=
+          (compareValue_eq_eq_iff x.2 z.2).1 hvxz
+        have hyvx : compareValue y.2 x.2 ≠ .gt := by
+          simpa [hvxzEq] using hyz'.1
+        have hvxy : compareValue x.2 y.2 = .eq :=
+          compareValue_eq_of_not_gt_not_gt hxy'.1 hyvx
+        have hvxyEq : x.2 = y.2 :=
+          (compareValue_eq_eq_iff x.2 y.2).1 hvxy
+        have hvyzEq : y.2 = z.2 := hvxyEq.symm.trans hvxzEq
+        exact compareObject_le_trans xs ys zs
+          (hxy'.2 ((compareValue_eq_eq_iff x.2 y.2).2 hvxyEq))
+          (hyz'.2 ((compareValue_eq_eq_iff y.2 z.2).2 hvyzEq))
+  termination_by xs ys zs => sizeOf xs + sizeOf ys + sizeOf zs
+  decreasing_by
+    all_goals rcases x with ⟨kx, vx⟩
+    all_goals rcases y with ⟨ky, vy⟩
+    all_goals rcases z with ⟨kz, vz⟩
+    all_goals simp_wf
+    all_goals omega
+
+  private theorem compareList_le_trans (xs ys zs : List Value)
+      (hxy : compareList xs ys ≠ .gt)
+      (hyz : compareList ys zs ≠ .gt) :
+      compareList xs zs ≠ .gt := by
+    cases xs with
+    | nil => cases zs <;> simp [compareList_nil_left]
+    | cons x xs =>
+        cases ys with
+        | nil => exact False.elim (hxy (compareList_cons_nil x xs))
+        | cons y ys =>
+            cases zs with
+            | nil => exact False.elim (hyz (compareList_cons_nil y ys))
+            | cons z zs =>
+                simp only [compareList_cons_cons] at hxy hyz ⊢
+                rw [then_ne_gt_iff] at hxy hyz ⊢
+                refine ⟨compareValue_le_trans x y z hxy.1 hyz.1, ?_⟩
+                intro hxz
+                have hxzEq : x = z :=
+                  (compareValue_eq_eq_iff x z).1 hxz
+                subst z
+                have hxyEq : compareValue x y = .eq :=
+                  compareValue_eq_of_not_gt_not_gt hxy.1 hyz.1
+                have hxyValue : x = y :=
+                  (compareValue_eq_eq_iff x y).1 hxyEq
+                subst y
+                exact compareList_le_trans xs ys zs
+                  (hxy.2 ((compareValue_eq_eq_iff x x).2 rfl))
+                  (hyz.2 ((compareValue_eq_eq_iff x x).2 rfl))
+  termination_by sizeOf xs + sizeOf ys + sizeOf zs
+  decreasing_by
+    all_goals subst_vars
+    all_goals simp_wf
+    all_goals omega
+end
+
+private instance : Batteries.TransCmp compareValue where
+  symm := compareValue_swap
+  le_trans := compareValue_le_trans _ _ _
+
+/-- The non-strict order induced by the Rust-compatible value comparator. -/
+def canonicalLE (x y : Value) : Prop :=
+  compareValue x y ≠ .gt
+
+private instance : DecidableRel canonicalLE := fun x y =>
+  inferInstanceAs (Decidable (compareValue x y ≠ .gt))
+
+private instance : IsTrans Value canonicalLE where
+  trans _ _ _ := compareValue_le_trans _ _ _
+
+private instance : IsAntisymm Value canonicalLE where
+  antisymm x y hxy hyx :=
+    (compareValue_eq_eq_iff x y).1
+      (compareValue_eq_of_not_gt_not_gt hxy hyx)
+
+private instance : IsTotal Value canonicalLE where
+  total x y := by
+    cases h : compareValue x y with
+    | lt => exact Or.inl (by simp [canonicalLE, h])
+    | eq => exact Or.inl (by simp [canonicalLE, h])
+    | gt =>
+        apply Or.inr
+        simp only [canonicalLE]
+        intro hyx
+        have hs := compareValue_swap x y
+        rw [h] at hs
+        have hyxlt : compareValue y x = .lt := by simpa using hs.symm
+        exact Ordering.noConfusion (hyxlt.symm.trans hyx)
+
+/--
+Canonical representation of an unordered set: discard multiplicity, then
+sort by `compareValue`.
+-/
+def canonicalizeSet (xs : List Value) : List Value :=
+  Multiset.sort canonicalLE (Multiset.dedup (xs : Multiset Value))
+
+theorem canonicalizeSet_perm {xs ys : List Value} (h : xs.Perm ys) :
+    canonicalizeSet xs = canonicalizeSet ys := by
+  apply congrArg (Multiset.sort canonicalLE)
+  apply congrArg Multiset.dedup
+  exact Multiset.coe_eq_coe.mpr h
+
+@[simp] theorem mem_canonicalizeSet {v : Value} {xs : List Value} :
+    v ∈ canonicalizeSet xs ↔ v ∈ xs := by
+  simp [canonicalizeSet]
+
+theorem canonicalizeSet_sorted (xs : List Value) :
+    (canonicalizeSet xs).Sorted canonicalLE :=
+  Multiset.sort_sorted canonicalLE _
+
+theorem canonicalizeSet_nodup (xs : List Value) :
+    (canonicalizeSet xs).Nodup := by
+  have hp : (canonicalizeSet xs).Perm xs.dedup := by
+    simpa [canonicalizeSet, Multiset.coe_dedup] using
+      List.mergeSort_perm xs.dedup
+        (fun x y => decide (canonicalLE x y))
+  exact hp.nodup_iff.mpr (List.nodup_dedup xs)
+
+@[simp] theorem canonicalizeSet_idempotent (xs : List Value) :
+    canonicalizeSet (canonicalizeSet xs) = canonicalizeSet xs := by
+  apply List.eq_of_perm_of_sorted (r := canonicalLE)
+  · change
+      (Multiset.sort canonicalLE
+        (Multiset.dedup (canonicalizeSet xs : Multiset Value))).Perm
+        (canonicalizeSet xs)
+    apply Multiset.coe_eq_coe.mp
+    rw [Multiset.sort_eq]
+    have hn : (canonicalizeSet xs : Multiset Value).Nodup :=
+      canonicalizeSet_nodup xs
+    rw [Multiset.dedup_eq_self.mpr hn]
+  · exact canonicalizeSet_sorted _
+  · exact canonicalizeSet_sorted _
+
+/-- Construct a semantic set from elements in arbitrary input order. -/
+def mkSet (xs : List Value) : Value :=
+  .Set (canonicalizeSet xs)
+
+theorem mkSet_perm {xs ys : List Value} (h : xs.Perm ys) :
+    mkSet xs = mkSet ys := by
+  rw [mkSet, mkSet, canonicalizeSet_perm h]
+
+/-- Key-first, value-second comparison of object entries. -/
+def compareEntry (x y : Value × Value) : Ordering :=
+  (compareValue x.1 y.1).then (compareValue x.2 y.2)
+
+private theorem compareEntry_swap (x y : Value × Value) :
+    (compareEntry x y).swap = compareEntry y x := by
+  simp [compareEntry, Ordering.swap_then, compareValue_swap]
+
+private theorem compareEntry_eq_eq_iff (x y : Value × Value) :
+    compareEntry x y = .eq ↔ x = y := by
+  rcases x with ⟨kx, vx⟩
+  rcases y with ⟨ky, vy⟩
+  simp [compareEntry, Ordering.then_eq_eq, compareValue_eq_eq_iff,
+    Prod.ext_iff]
+
+private theorem compareEntry_le_trans (x y z : Value × Value)
+    (hxy : compareEntry x y ≠ .gt)
+    (hyz : compareEntry y z ≠ .gt) :
+    compareEntry x z ≠ .gt := by
+  simp only [compareEntry] at hxy hyz ⊢
+  rw [then_ne_gt_iff] at hxy hyz ⊢
+  refine ⟨compareValue_le_trans x.1 y.1 z.1 hxy.1 hyz.1, ?_⟩
+  intro hxz
+  have hxzEq : x.1 = z.1 := (compareValue_eq_eq_iff _ _).1 hxz
+  have hyx : compareValue y.1 x.1 ≠ .gt := by
+    simpa [hxzEq] using hyz.1
+  have hxyEq := compareValue_eq_of_not_gt_not_gt hxy.1 hyx
+  have hkxy : x.1 = y.1 := (compareValue_eq_eq_iff _ _).1 hxyEq
+  have hkyz : y.1 = z.1 := hkxy.symm.trans hxzEq
+  exact compareValue_le_trans x.2 y.2 z.2
+    (hxy.2 ((compareValue_eq_eq_iff _ _).2 hkxy))
+    (hyz.2 ((compareValue_eq_eq_iff _ _).2 hkyz))
+
+private instance : Batteries.TransCmp compareEntry where
+  symm := compareEntry_swap
+  le_trans := compareEntry_le_trans _ _ _
+
+/-- The non-strict key-first order used for canonical object entries. -/
+def entryLE (x y : Value × Value) : Prop :=
+  compareEntry x y ≠ .gt
+
+private instance : DecidableRel entryLE := fun x y =>
+  inferInstanceAs (Decidable (compareEntry x y ≠ .gt))
+
+private instance : IsTrans (Value × Value) entryLE where
+  trans _ _ _ := compareEntry_le_trans _ _ _
+
+private instance : IsAntisymm (Value × Value) entryLE where
+  antisymm x y hxy hyx := by
+    apply (compareEntry_eq_eq_iff x y).1
+    cases h : compareEntry x y with
+    | lt =>
+        have hs := compareEntry_swap x y
+        rw [h] at hs
+        exact False.elim (hyx (by simpa using hs.symm))
+    | eq => rfl
+    | gt => exact False.elim (hxy h)
+
+private instance : IsTotal (Value × Value) entryLE where
+  total x y := by
+    cases h : compareEntry x y with
+    | lt => exact Or.inl (by simp [entryLE, h])
+    | eq => exact Or.inl (by simp [entryLE, h])
+    | gt =>
+        apply Or.inr
+        simp only [entryLE]
+        intro hyx
+        have hs := compareEntry_swap x y
+        rw [h] at hs
+        have hyxlt : compareEntry y x = .lt := by simpa using hs.symm
+        exact Ordering.noConfusion (hyxlt.symm.trans hyx)
+
+/--
+Remove duplicate object keys from right to left.  Thus the final occurrence of
+each key is retained, exactly matching repeated `BTreeMap::insert` operations.
+-/
+def deduplicateObjectLast : List (Value × Value) → List (Value × Value)
+  | [] => []
+  | x :: xs =>
+      let tail := deduplicateObjectLast xs
+      if x.1 ∈ tail.map Prod.fst then tail else x :: tail
+
+theorem deduplicateObjectLast_eq_self {xs : List (Value × Value)}
+    (h : (xs.map Prod.fst).Nodup) :
+    deduplicateObjectLast xs = xs := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih =>
+      have h' := List.nodup_cons.mp h
+      simp [deduplicateObjectLast, ih h'.2, h'.1]
+
+theorem mem_deduplicateObjectLast {p : Value × Value}
+    {xs : List (Value × Value)} (h : p ∈ deduplicateObjectLast xs) : p ∈ xs := by
+  induction xs with
+  | nil => simp [deduplicateObjectLast] at h
+  | cons x xs ih =>
+      simp only [deduplicateObjectLast] at h
+      split at h
+      · exact List.mem_cons_of_mem _ (ih h)
+      · rcases List.mem_cons.mp h with rfl | h
+        · exact List.mem_cons_self _ _
+        · exact List.mem_cons_of_mem _ (ih h)
+
+/--
+Canonical representation of an object. Duplicate keys use last-write-wins;
+the retained entries are sorted by key, then by value as a vacuous tie-break.
+-/
+def canonicalizeObject (xs : List (Value × Value)) : List (Value × Value) :=
+  Multiset.sort entryLE (deduplicateObjectLast xs : Multiset (Value × Value))
+
+/-- Every retained entry of the canonical object came from the original
+input; canonicalization only removes shadowed duplicate-key entries and
+reorders, it never fabricates entries. -/
+theorem mem_canonicalizeObject {p : Value × Value}
+    {xs : List (Value × Value)} (h : p ∈ canonicalizeObject xs) : p ∈ xs :=
+  mem_deduplicateObjectLast (by simpa [canonicalizeObject] using h)
+
+theorem canonicalizeObject_perm {xs ys : List (Value × Value)}
+    (hkeys : (xs.map Prod.fst).Nodup) (h : xs.Perm ys) :
+    canonicalizeObject xs = canonicalizeObject ys := by
+  have hkeys' : (ys.map Prod.fst).Nodup :=
+    (h.map Prod.fst).nodup_iff.mp hkeys
+  simp only [canonicalizeObject, deduplicateObjectLast_eq_self hkeys,
+    deduplicateObjectLast_eq_self hkeys']
+  apply congrArg (Multiset.sort entryLE)
+  exact Multiset.coe_eq_coe.mpr h
+
+theorem canonicalizeObject_sorted (xs : List (Value × Value)) :
+    (canonicalizeObject xs).Sorted entryLE :=
+  Multiset.sort_sorted entryLE _
+
+theorem canonicalizeObject_sortedByKey (xs : List (Value × Value)) :
+    (canonicalizeObject xs).Sorted
+      (fun x y => compareValue x.1 y.1 ≠ .gt) := by
+  apply (canonicalizeObject_sorted xs).imp
+  intro x y h
+  exact (then_ne_gt_iff _ _).1 h |>.1
+
+/-- Construct a semantic object from entries in arbitrary input order. -/
+def mkObject (xs : List (Value × Value)) : Value :=
+  .Object (canonicalizeObject xs)
+
+theorem mkObject_perm {xs ys : List (Value × Value)}
+    (hkeys : (xs.map Prod.fst).Nodup) (h : xs.Perm ys) :
+    mkObject xs = mkObject ys := by
+  rw [mkObject, mkObject, canonicalizeObject_perm hkeys h]
+
+end Regorus.Value
diff --git a/formal/Regorus/Value/RawNumber.lean b/formal/Regorus/Value/RawNumber.lean
new file mode 100644
index 00000000..30c8ad79
--- /dev/null
+++ b/formal/Regorus/Value/RawNumber.lean
@@ -0,0 +1,556 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Mathlib.Algebra.Order.Field.Rat
+import Mathlib.Data.BitVec
+import Mathlib.Tactic.NormNum
+
+/-!
+# Raw Regorus numbers
+
+This module models the representation-sensitive `Number` implementation in
+`src/number.rs`.  `F64Bits` stores the complete IEEE-754 binary64 bit pattern;
+in particular, signed zeroes and all NaN payloads remain distinguishable.
+
+`RawNumber.rustEq` and `RawNumber.rustCompare` deliberately model the Rust
+implementation rather than Lean equality.  Consequently `rustCompare` maps an
+unordered NaN comparison to `Ordering.eq`, while `rustEq` remains false.  No
+lawful order instance is therefore attached to `RawNumber`.
+-/
+
+namespace Regorus
+
+/-- A signed 64-bit integer, represented intrinsically by its mathematical value. -/
+structure Int64 where
+  val : Int
+  isValid : -(2 ^ 63 : Int) ≤ val ∧ val < (2 ^ 63 : Int)
+
+namespace Int64
+
+instance : DecidableEq Int64 := fun x y =>
+  decidable_of_iff (x.val = y.val) <| by
+    constructor
+    · intro h
+      cases x
+      cases y
+      simp_all
+    · exact congrArg Int64.val
+
+instance : Repr Int64 where
+  reprPrec i _ := repr i.val
+
+/-- The mathematical value represented by an `Int64`. -/
+@[coe] def toInt (i : Int64) : Int := i.val
+
+instance : Coe Int64 Int := ⟨toInt⟩
+
+/-- Checked construction, corresponding to `i64::try_from`. -/
+def ofInt? (i : Int) : Option Int64 :=
+  if h : -(2 ^ 63 : Int) ≤ i ∧ i < (2 ^ 63 : Int) then
+    some ⟨i, h⟩
+  else
+    none
+
+/-- Zero in the signed 64-bit representation. -/
+def zero : Int64 :=
+  ⟨0, by decide⟩
+
+@[simp] theorem toInt_zero : (zero : Int) = 0 := rfl
+
+instance : LinearOrder Int64 :=
+  LinearOrder.lift' Int64.val <| by
+    intro a b h
+    cases a
+    cases b
+    simp_all
+
+end Int64
+
+/-- A bit-exact IEEE-754 binary64 value. -/
+structure F64Bits where
+  bits : UInt64
+  deriving DecidableEq, Repr
+
+namespace F64Bits
+
+def significandWidth : Nat := 52
+def exponentWidth : Nat := 11
+def exponentBias : Nat := 1023
+def maxExponentField : Nat := 2047
+def signWeight : Nat := 2 ^ 63
+def exponentWeight : Nat := 2 ^ significandWidth
+def significandLimit : Nat := 2 ^ significandWidth
+def precisionLimit : Nat := 2 ^ 53
+
+/-- Construct a bit pattern from sign, exponent, and fraction fields.
+Inputs are masked to their respective field widths. -/
+def ofFields (negative : Bool) (exponent fraction : Nat) : F64Bits :=
+  ⟨UInt64.ofNat
+    ((if negative then signWeight else 0) +
+      (exponent % (2 ^ exponentWidth)) * exponentWeight +
+      fraction % significandLimit)⟩
+
+/-- The sign bit (`true` means negative). -/
+def sign (f : F64Bits) : Bool :=
+  decide (signWeight ≤ f.bits.toNat)
+
+/-- The eleven raw exponent bits. -/
+def exponent (f : F64Bits) : Nat :=
+  (f.bits.toNat / exponentWeight) % (2 ^ exponentWidth)
+
+/-- The 52 raw trailing-significand bits. -/
+def fraction (f : F64Bits) : Nat :=
+  f.bits.toNat % significandLimit
+
+def positiveZero : F64Bits := ofFields false 0 0
+def negativeZero : F64Bits := ofFields true 0 0
+def positiveInfinity : F64Bits := ofFields false maxExponentField 0
+def negativeInfinity : F64Bits := ofFields true maxExponentField 0
+def quietNaN : F64Bits := ofFields false maxExponentField (2 ^ 51)
+
+/-- Exact semantic classification of a binary64 bit pattern. -/
+inductive Decoded where
+  /-- Finite mathematical value; `negativeZero` records the sign when `value = 0`. -/
+  | finite (value : Rat) (negativeZero : Bool)
+  | infinity (negative : Bool)
+  | nan
+  deriving DecidableEq, Repr
+
+/-- An exact rational power of two. -/
+def twoPowRat : Int → Rat
+  | .ofNat n => (2 ^ n : Nat)
+  | .negSucc n => 1 / (2 ^ (n + 1) : Nat)
+
+/-- Decode a binary64 pattern without passing through a host floating-point value. -/
+def decode (f : F64Bits) : Decoded :=
+  let e := f.exponent
+  let m := f.fraction
+  let neg := f.sign
+  if e = maxExponentField then
+    if m = 0 then .infinity neg else .nan
+  else
+    let significand := if e = 0 then m else significandLimit + m
+    let scale : Int :=
+      if e = 0 then -1074 else Int.ofNat e - 1075
+    let magnitude : Rat := (significand : Rat) * twoPowRat scale
+    let value := if neg then -magnitude else magnitude
+    .finite value (neg && significand = 0)
+
+def isNaN (f : F64Bits) : Bool :=
+  match f.decode with
+  | .nan => true
+  | _ => false
+
+def isFinite (f : F64Bits) : Bool :=
+  match f.decode with
+  | .finite _ _ => true
+  | _ => false
+
+def isZero (f : F64Bits) : Bool :=
+  match f.decode with
+  | .finite q _ => decide (q = 0)
+  | _ => false
+
+/-- IEEE equality: NaNs compare unequal and signed zeroes compare equal. -/
+def ieeeEq (a b : F64Bits) : Bool :=
+  match a.decode, b.decode with
+  | .nan, _ | _, .nan => false
+  | .infinity sa, .infinity sb => decide (sa = sb)
+  | .finite x _, .finite y _ => decide (x = y)
+  | _, _ => false
+
+/-- IEEE partial comparison, with `none` for every comparison involving NaN. -/
+def partialCompare (a b : F64Bits) : Option Ordering :=
+  match a.decode, b.decode with
+  | .nan, _ | _, .nan => none
+  | .infinity true, .infinity true
+  | .infinity false, .infinity false => some .eq
+  | .infinity true, _ | _, .infinity false => some .lt
+  | .infinity false, _ | _, .infinity true => some .gt
+  | .finite x _, .finite y _ => some (compare x y)
+
+/-- Round `n / d` to an integer, using round-to-nearest, ties-to-even. -/
+private def roundDivEven (n d : Nat) : Nat :=
+  if d = 0 then
+    0
+  else
+    let q := n / d
+    let r := n % d
+    if 2 * r < d then
+      q
+    else if d < 2 * r then
+      q + 1
+    else if q % 2 = 0 then
+      q
+    else
+      q + 1
+
+/-- Decide whether `n / d < 2^e`, without approximate arithmetic. -/
+private def ratioLtPowTwo (n d : Nat) : Int → Bool
+  | .ofNat e => decide (n < d * 2 ^ e)
+  | .negSucc e => decide (n * 2 ^ (e + 1) < d)
+
+/-- `⌊log₂ (n / d)⌋` for positive `n` and `d`. -/
+private def floorLogTwoRatio (n d : Nat) : Int :=
+  let candidate := Int.ofNat n.log2 - Int.ofNat d.log2
+  if ratioLtPowTwo n d candidate then candidate - 1 else candidate
+
+/-- Round `(n / d) * 2^shift` to the nearest-even natural number. -/
+private def roundScaled (n d : Nat) : Int → Nat
+  | .ofNat shift => roundDivEven (n * 2 ^ shift) d
+  | .negSucc shift => roundDivEven n (d * 2 ^ (shift + 1))
+
+/-- Encode a positive rational magnitude with the requested sign. -/
+private def encodeMagnitude (negative : Bool) (n d : Nat) : F64Bits :=
+  if n = 0 then
+    ofFields negative 0 0
+  else
+    let e := floorLogTwoRatio n d
+    if e < -1022 then
+      let m := roundScaled n d 1074
+      if m = 0 then
+        ofFields negative 0 0
+      else if significandLimit ≤ m then
+        ofFields negative 1 0
+      else
+        ofFields negative 0 m
+    else
+      let rounded := roundScaled n d (52 - e)
+      let carry := rounded = precisionLimit
+      let e' := if carry then e + 1 else e
+      let significand := if carry then significandLimit else rounded
+      if 1023 < e' then
+        ofFields negative maxExponentField 0
+      else
+        ofFields negative (e' + 1023).toNat (significand - significandLimit)
+
+/-- Correctly round an exact rational to binary64 (nearest, ties-to-even). -/
+def fromRat (q : Rat) (negativeZero : Bool := false) : F64Bits :=
+  if q = 0 then
+    ofFields negativeZero 0 0
+  else
+    encodeMagnitude (q < 0) q.num.natAbs q.den
+
+def fromInt (i : Int) : F64Bits :=
+  fromRat (i : Rat)
+
+/-- Toggle the IEEE sign bit, including for NaNs and signed zeroes. -/
+def negate (f : F64Bits) : F64Bits :=
+  ofFields (!f.sign) f.exponent f.fraction
+
+private def finiteSign (q : Rat) (negativeZero : Bool) : Bool :=
+  if q = 0 then negativeZero else q < 0
+
+/-- IEEE-754 addition, specified through exact rationals and nearest-even rounding. -/
+def add (a b : F64Bits) : F64Bits :=
+  match a.decode, b.decode with
+  | .nan, _ | _, .nan => quietNaN
+  | .infinity sa, .infinity sb =>
+      if sa = sb then ofFields sa maxExponentField 0 else quietNaN
+  | .infinity sa, _ | _, .infinity sa => ofFields sa maxExponentField 0
+  | .finite x zx, .finite y zy =>
+      let q := x + y
+      fromRat q (q = 0 && zx && zy)
+
+def sub (a b : F64Bits) : F64Bits :=
+  add a b.negate
+
+/-- IEEE-754 multiplication, specified through exact rationals and nearest-even rounding. -/
+def mul (a b : F64Bits) : F64Bits :=
+  match a.decode, b.decode with
+  | .nan, _ | _, .nan => quietNaN
+  | .infinity sa, .infinity sb =>
+      ofFields (xor sa sb) maxExponentField 0
+  | .infinity sa, .finite q z | .finite q z, .infinity sa =>
+      if q = 0 then quietNaN
+      else ofFields (xor sa (finiteSign q z)) maxExponentField 0
+  | .finite x zx, .finite y zy =>
+      let negative := xor (finiteSign x zx) (finiteSign y zy)
+      fromRat (x * y) (x * y = 0 && negative)
+
+/-- IEEE-754 division.  `RawNumber.div` rejects zero divisors before using this operation. -/
+def div (a b : F64Bits) : F64Bits :=
+  match a.decode, b.decode with
+  | .nan, _ | _, .nan => quietNaN
+  | .infinity _, .infinity _ => quietNaN
+  | .infinity sa, .finite y zy =>
+      ofFields (xor sa (finiteSign y zy)) maxExponentField 0
+  | .finite x zx, .infinity sb =>
+      ofFields (xor (finiteSign x zx) sb) 0 0
+  | .finite x zx, .finite y zy =>
+      let negative := xor (finiteSign x zx) (finiteSign y zy)
+      if y = 0 then
+        if x = 0 then quietNaN else ofFields negative maxExponentField 0
+      else
+        fromRat (x / y) (x = 0 && negative)
+
+/-- Rust's `float_to_small_bigint`: exact, finite integral floats in `[-2^53, 2^53]`. -/
+def toSmallInt? (f : F64Bits) : Option Int :=
+  match f.decode with
+  | .finite q _ =>
+      if q.den = 1 ∧ q.num.natAbs ≤ precisionLimit then some q.num else none
+  | _ => none
+
+@[simp] theorem decode_positiveZero : positiveZero.decode = .finite 0 false := by
+  change decode ⟨UInt64.ofNat 0⟩ = .finite 0 false
+  simp only [decode, exponent, fraction, sign]
+  rw [show (UInt64.ofNat 0).toNat = 0 from
+    UInt64.toNat_ofNat_of_lt (by norm_num)]
+  norm_num [exponentWeight, significandWidth, exponentWidth,
+    maxExponentField, significandLimit, signWeight, twoPowRat]
+
+@[simp] theorem decode_negativeZero : negativeZero.decode = .finite 0 true := by
+  change decode ⟨UInt64.ofNat 9223372036854775808⟩ = .finite 0 true
+  simp only [decode, exponent, fraction, sign]
+  rw [show (UInt64.ofNat 9223372036854775808).toNat =
+      9223372036854775808 from UInt64.toNat_ofNat_of_lt (by norm_num)]
+  norm_num [exponentWeight, significandWidth, exponentWidth,
+    maxExponentField, significandLimit, signWeight, twoPowRat]
+
+@[simp] theorem decode_positiveInfinity :
+    positiveInfinity.decode = .infinity false := by
+  decide
+
+@[simp] theorem decode_negativeInfinity :
+    negativeInfinity.decode = .infinity true := by
+  decide
+
+@[simp] theorem decode_quietNaN : quietNaN.decode = .nan := by
+  decide
+
+end F64Bits
+
+/-- The four representation variants of Rust's `Number`. -/
+inductive RawNumber where
+  | UInt (u : UInt64)
+  | Int (i : Int64)
+  | BigInt (b : Int)
+  | Float (f : F64Bits)
+  deriving DecidableEq, Repr
+
+namespace RawNumber
+
+def safeInteger : Nat := 2 ^ 53
+def maxUInt64 : ℤ := Int.ofNat (UInt64.size - 1)
+
+/-- Canonicalize an integer exactly as `Number::from_bigint_owned`. -/
+def normalizeInt (i : ℤ) : RawNumber :=
+  if i = 0 then
+    .Int Int64.zero
+  else if 0 < i ∧ i ≤ maxUInt64 then
+    .UInt (UInt64.ofNat i.toNat)
+  else
+    match Int64.ofInt? i with
+    | some j => .Int j
+    | none => .BigInt i
+
+/-- Exact integer conversion used by equality, ordering, modulo, and bit operations. -/
+def toExactInt? : RawNumber → Option ℤ
+  | .UInt u => some (Int.ofNat u.toNat)
+  | .Int i => some i.val
+  | .BigInt i => some i
+  | .Float f => f.toSmallInt?
+
+/-- Exact rational value, undefined for infinities and NaNs. -/
+def toRat? : RawNumber → Option Rat
+  | .UInt u => some (Int.ofNat u.toNat : Rat)
+  | .Int i => some (i.val : Rat)
+  | .BigInt i => some (i : Rat)
+  | .Float f =>
+      match f.decode with
+      | .finite q _ => some q
+      | _ => none
+
+/-- Rust's lossy conversion used whenever a floating-point operand participates. -/
+def toF64Lossy : RawNumber → F64Bits
+  | .UInt u => F64Bits.fromInt (Int.ofNat u.toNat)
+  | .Int i => F64Bits.fromInt i.val
+  | .BigInt i => F64Bits.fromInt i
+  | .Float f => f
+
+def isFloat : RawNumber → Bool
+  | .Float _ => true
+  | _ => false
+
+def isZero : RawNumber → Bool
+  | .UInt u => decide (u.toNat = 0)
+  | .Int i => decide (i.val = 0)
+  | .BigInt i => decide (i = 0)
+  | .Float f => f.isZero
+
+/-- Normalize a float to an integer exactly when Rust's `normalize_float` does. -/
+def normalizeFloat (f : F64Bits) : RawNumber :=
+  match f.toSmallInt? with
+  | some i => normalizeInt i
+  | none => .Float f
+
+/-- Representation-insensitive equality implemented by `Number::eq`. -/
+def rustEq (a b : RawNumber) : Bool :=
+  match a.toExactInt?, b.toExactInt? with
+  | some x, some y => decide (x = y)
+  | _, _ => F64Bits.ieeeEq a.toF64Lossy b.toF64Lossy
+
+/-- Total comparator implemented by `Number::cmp`; unordered NaNs map to equality. -/
+def rustCompare (a b : RawNumber) : Ordering :=
+  match a.toExactInt?, b.toExactInt? with
+  | some x, some y => compare x y
+  | _, _ => (F64Bits.partialCompare a.toF64Lossy b.toF64Lossy).getD .eq
+
+inductive Error where
+  | divisionByZero
+  | moduloOnFloatingPoint
+  deriving DecidableEq, Repr
+
+def add (a b : RawNumber) : RawNumber :=
+  if a.isFloat || b.isFloat then
+    normalizeFloat (F64Bits.add a.toF64Lossy b.toF64Lossy)
+  else
+    match a.toExactInt?, b.toExactInt? with
+    | some x, some y => normalizeInt (x + y)
+    | _, _ => .Float F64Bits.quietNaN
+
+def sub (a b : RawNumber) : RawNumber :=
+  if a.isFloat || b.isFloat then
+    normalizeFloat (F64Bits.sub a.toF64Lossy b.toF64Lossy)
+  else
+    match a.toExactInt?, b.toExactInt? with
+    | some x, some y => normalizeInt (x - y)
+    | _, _ => .Float F64Bits.quietNaN
+
+def mul (a b : RawNumber) : RawNumber :=
+  if a.isFloat || b.isFloat then
+    normalizeFloat (F64Bits.mul a.toF64Lossy b.toF64Lossy)
+  else
+    match a.toExactInt?, b.toExactInt? with
+    | some x, some y => normalizeInt (x * y)
+    | _, _ => .Float F64Bits.quietNaN
+
+/-- Division follows `Number::divide`: exact integral quotients stay integral. -/
+def div (a b : RawNumber) : Except Error RawNumber :=
+  if b.isZero then
+    .error .divisionByZero
+  else if a.isFloat || b.isFloat then
+    .ok (.Float (F64Bits.div a.toF64Lossy b.toF64Lossy))
+  else
+    match a.toExactInt?, b.toExactInt? with
+    | some x, some y =>
+        if y ∣ x then
+          .ok (normalizeInt (x / y))
+        else
+          .ok (.Float (F64Bits.div a.toF64Lossy b.toF64Lossy))
+    | _, _ => .ok (.Float F64Bits.quietNaN)
+
+/-- Rust remainder (quotient truncated toward zero). -/
+def rustRem (a b : ℤ) : ℤ :=
+  a - a.tdiv b * b
+
+/-- Modulo accepts integers and only the small integral floats accepted by Rust. -/
+def modulo (a b : RawNumber) : Except Error RawNumber :=
+  match a.toExactInt?, b.toExactInt? with
+  | some x, some y =>
+      if y = 0 then
+        .error .divisionByZero
+      else
+        .ok (normalizeInt (rustRem x y))
+  | _, _ => .error .moduloOnFloatingPoint
+
+/-- Strict conversion corresponding to `Number::as_u64`. -/
+def asUInt64? (n : RawNumber) : Option UInt64 :=
+  n.toExactInt?.bind fun i =>
+    if 0 ≤ i ∧ i ≤ maxUInt64 then some (UInt64.ofNat i.toNat) else none
+
+/-- Strict conversion corresponding to `Number::as_i64`. -/
+def asInt64? (n : RawNumber) : Option Int64 :=
+  n.toExactInt?.bind Int64.ofInt?
+
+/-- Strict conversion corresponding to `Number::as_f64`. -/
+def asF64? : RawNumber → Option F64Bits
+  | .Float f => if f.isFinite then some f else none
+  | .UInt u =>
+      if u.toNat ≤ safeInteger then some (F64Bits.fromInt (Int.ofNat u.toNat)) else none
+  | .Int i =>
+      if i.val.natAbs ≤ safeInteger then some (F64Bits.fromInt i.val) else none
+  | .BigInt i =>
+      if i.natAbs < safeInteger then some (F64Bits.fromInt i) else none
+
+@[simp] theorem toExactInt_normalizeInt (i : ℤ) :
+    (normalizeInt i).toExactInt? = some i := by
+  simp only [normalizeInt]
+  split
+  · rename_i h
+    subst i
+    simp [toExactInt?, Int64.zero]
+  · split
+    · rename_i h
+      simp only [toExactInt?]
+      have hnonneg : 0 ≤ i := h.1.le
+      have hcast : Int.ofNat i.toNat = i := Int.toNat_of_nonneg hnonneg
+      have hi' : i.toNat ≤ UInt64.size - 1 := by
+        apply Int.ofNat_le.mp
+        simpa [hcast, maxUInt64] using h.2
+      have hi : i.toNat < UInt64.size := by
+        omega
+      rw [UInt64.toNat_ofNat_of_lt hi, hcast]
+    · cases h : Int64.ofInt? i with
+      | none => simp [toExactInt?, h]
+      | some j =>
+          simp only [toExactInt?, h, Option.some.injEq]
+          simp only [Int64.ofInt?] at h
+          split at h
+          · have hj := Option.some.inj h
+            exact (congrArg Int64.val hj).symm
+          · contradiction
+
+@[simp] theorem toRat_normalizeInt (i : ℤ) :
+    (normalizeInt i).toRat? = some (i : Rat) := by
+  simp only [normalizeInt]
+  split
+  · rename_i h
+    subst i
+    simp [toRat?, Int64.zero]
+  · split
+    · rename_i h
+      simp only [toRat?]
+      have hnonneg : 0 ≤ i := h.1.le
+      have hcast : Int.ofNat i.toNat = i := Int.toNat_of_nonneg hnonneg
+      have hi' : i.toNat ≤ UInt64.size - 1 := by
+        apply Int.ofNat_le.mp
+        simpa [hcast, maxUInt64] using h.2
+      have hi : i.toNat < UInt64.size := by
+        omega
+      rw [UInt64.toNat_ofNat_of_lt hi, hcast]
+    · cases h : Int64.ofInt? i with
+      | none => simp [toRat?, h]
+      | some j =>
+          simp only [toRat?, h, Option.some.injEq]
+          simp only [Int64.ofInt?] at h
+          split at h
+          · have hj := Option.some.inj h
+            exact (congrArg (fun z : Int64 => (z.val : Rat)) hj).symm
+          · contradiction
+
+@[simp] theorem add_integer_semantics
+    {a b : RawNumber} {x y : ℤ}
+    (ha : a.isFloat = false) (hb : b.isFloat = false)
+    (hax : a.toExactInt? = some x) (hby : b.toExactInt? = some y) :
+    (add a b).toExactInt? = some (x + y) := by
+  simp [add, ha, hb, hax, hby]
+
+@[simp] theorem rustEq_self_of_not_nan (n : RawNumber)
+    (h : F64Bits.isNaN n.toF64Lossy = false) :
+    rustEq n n = true := by
+  simp only [rustEq]
+  cases hi : n.toExactInt? with
+  | some i => simp
+  | none =>
+      simp only [hi]
+      cases hd : n.toF64Lossy.decode with
+      | nan => simp [F64Bits.isNaN, hd] at h
+      | infinity s => simp [F64Bits.ieeeEq, hd]
+      | finite q z => simp [F64Bits.ieeeEq, hd]
+
+end RawNumber
+
+end Regorus
diff --git a/formal/Regorus/Value/RawValue.lean b/formal/Regorus/Value/RawValue.lean
new file mode 100644
index 00000000..878b2498
--- /dev/null
+++ b/formal/Regorus/Value/RawValue.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.Value.RawNumber
+
+/-!
+# Representation-level values
+
+`RawValue` mirrors the eight constructors of Rust's `Value`.  Sets and objects
+are intentionally represented by lists here: uniqueness, sorting, and key
+normalization are representation invariants imposed by a later refinement.
+
+The mutually recursive node counts expose the decrease that is hidden by the
+nested `List RawValue` occurrences.  They are suitable termination measures
+for representation-sensitive recursive functions and proofs.
+-/
+
+namespace Regorus
+
+inductive RawValue where
+  | Null
+  | Bool (b : Bool)
+  | Number (n : RawNumber)
+  | String (s : String)
+  | Array (a : List RawValue)
+  | Set (s : List RawValue)
+  | Object (o : List (RawValue × RawValue))
+  | Undefined
+  deriving Repr
+
+namespace RawValue
+
+mutual
+  /-- Number of `RawValue` nodes, including the root. -/
+  @[simp] def nodeCount : RawValue → Nat
+    | .Null | .Bool _ | .Number _ | .String _ | .Undefined => 1
+    | .Array xs | .Set xs => listNodeCount xs + 1
+    | .Object xs => objectNodeCount xs + 1
+
+  /-- Aggregate node count of a raw array or set payload. -/
+  @[simp] def listNodeCount : List RawValue → Nat
+    | [] => 0
+    | x :: xs => nodeCount x + listNodeCount xs + 1
+
+  /-- Aggregate node count of raw object key/value pairs. -/
+  @[simp] def objectNodeCount : List (RawValue × RawValue) → Nat
+    | [] => 0
+    | (k, v) :: xs => nodeCount k + nodeCount v + objectNodeCount xs + 1
+end
+
+/-- The standard well-founded relation induced by `nodeCount`. -/
+def Smaller (x y : RawValue) : Prop :=
+  nodeCount x < nodeCount y
+
+theorem smaller_wellFounded : WellFounded Smaller :=
+  Nat.lt_wfRel.wf.onFun
+
+@[simp] theorem nodeCount_pos (v : RawValue) : 0 < nodeCount v := by
+  cases v <;> simp
+
+theorem head_lt_list (x : RawValue) (xs : List RawValue) :
+    nodeCount x < listNodeCount (x :: xs) := by
+  simp
+  omega
+
+theorem key_lt_object (k v : RawValue) (xs : List (RawValue × RawValue)) :
+    nodeCount k < objectNodeCount ((k, v) :: xs) := by
+  simp
+  omega
+
+theorem value_lt_object (k v : RawValue) (xs : List (RawValue × RawValue)) :
+    nodeCount v < objectNodeCount ((k, v) :: xs) := by
+  simp
+  omega
+
+theorem nodeCount_lt_list_of_mem {v : RawValue} {xs : List RawValue}
+    (h : v ∈ xs) : nodeCount v ≤ listNodeCount xs := by
+  induction xs with
+  | nil => simp at h
+  | cons x xs ih =>
+      simp only [List.mem_cons] at h
+      rcases h with rfl | h
+      · simp
+        omega
+      · have := ih h
+        simp
+        omega
+
+theorem nodeCount_lt_array_of_mem {v : RawValue} {xs : List RawValue}
+    (h : v ∈ xs) : nodeCount v < nodeCount (.Array xs) := by
+  simp only [nodeCount]
+  exact Nat.lt_succ_of_le (nodeCount_lt_list_of_mem h)
+
+theorem nodeCount_lt_set_of_mem {v : RawValue} {xs : List RawValue}
+    (h : v ∈ xs) : nodeCount v < nodeCount (.Set xs) := by
+  simp only [nodeCount]
+  exact Nat.lt_succ_of_le (nodeCount_lt_list_of_mem h)
+
+end RawValue
+
+end Regorus
diff --git a/formal/Regorus/Value/RegoNumber.lean b/formal/Regorus/Value/RegoNumber.lean
new file mode 100644
index 00000000..d73585d2
--- /dev/null
+++ b/formal/Regorus/Value/RegoNumber.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.Value.RawNumber
+
+/-!
+# Mathematical Regorus numbers
+
+`RegoNumber` is the representation-independent number domain used for proofs.
+Every finite IEEE-754 value embeds as its exact dyadic rational, while NaNs and
+infinities have no image.  Unlike `RawNumber`, this type has ordinary
+mathematical equality and a lawful linear order.
+-/
+
+namespace Regorus
+
+/-- An exact, finite mathematical number. -/
+structure RegoNumber where
+  val : Rat
+  deriving DecidableEq
+
+namespace RegoNumber
+
+instance : Repr RegoNumber where
+  reprPrec n p := reprPrec n.val p
+
+instance : LinearOrder RegoNumber :=
+  LinearOrder.lift' RegoNumber.val <| by
+    intro a b h
+    cases a
+    cases b
+    simp_all
+
+instance : Add RegoNumber := ⟨fun a b => ⟨a.val + b.val⟩⟩
+instance : Sub RegoNumber := ⟨fun a b => ⟨a.val - b.val⟩⟩
+instance : Mul RegoNumber := ⟨fun a b => ⟨a.val * b.val⟩⟩
+instance : Neg RegoNumber := ⟨fun a => ⟨-a.val⟩⟩
+instance (n : Nat) : OfNat RegoNumber n := ⟨⟨n⟩⟩
+
+/-- Embed a mathematical integer. -/
+def ofInt (i : Int) : RegoNumber :=
+  ⟨(i : Rat)⟩
+
+/-- Construct an exact rational, rejecting a zero denominator. -/
+def ofFraction? (numerator denominator : Int) : Option RegoNumber :=
+  if denominator = 0 then none else some ⟨Rat.divInt numerator denominator⟩
+
+/-- Strict division.  Rego reports division by zero rather than assigning it a value. -/
+def div? (a b : RegoNumber) : Option RegoNumber :=
+  if b.val = 0 then none else some ⟨a.val / b.val⟩
+
+/-- An exact integer projection. -/
+def toInt? (n : RegoNumber) : Option Int :=
+  if n.val.den = 1 then some n.val.num else none
+
+def isInteger (n : RegoNumber) : Bool :=
+  decide (n.val.den = 1)
+
+/-- Forget the representation of a finite raw number. -/
+def ofRaw? (n : RawNumber) : Option RegoNumber :=
+  n.toRat?.map RegoNumber.mk
+
+/-- A canonical raw integer when possible; otherwise the nearest binary64 value. -/
+def toRaw (n : RegoNumber) : RawNumber :=
+  match n.toInt? with
+  | some i => RawNumber.normalizeInt i
+  | none => .Float (F64Bits.fromRat n.val)
+
+@[simp] theorem val_ofInt (i : Int) : (ofInt i).val = (i : Rat) := rfl
+
+@[simp] theorem val_add (a b : RegoNumber) : (a + b).val = a.val + b.val := rfl
+
+@[simp] theorem val_sub (a b : RegoNumber) : (a - b).val = a.val - b.val := rfl
+
+@[simp] theorem val_mul (a b : RegoNumber) : (a * b).val = a.val * b.val := rfl
+
+@[simp] theorem val_neg (a : RegoNumber) : (-a).val = -a.val := rfl
+
+@[simp] theorem ofRaw_normalizeInt (i : Int) :
+    ofRaw? (RawNumber.normalizeInt i) = some (ofInt i) := by
+  simp [ofRaw?, ofInt]
+
+@[simp] theorem div?_eq_none_iff (a b : RegoNumber) :
+    div? a b = none ↔ b.val = 0 := by
+  simp [div?]
+
+@[simp] theorem ofRaw?_eq_none_iff (n : RawNumber) :
+    ofRaw? n = none ↔ n.toRat? = none := by
+  simp [ofRaw?]
+
+theorem le_iff_val_le (a b : RegoNumber) : a ≤ b ↔ a.val ≤ b.val :=
+  Iff.rfl
+
+theorem lt_iff_val_lt (a b : RegoNumber) : a < b ↔ a.val < b.val :=
+  Iff.rfl
+
+end RegoNumber
+
+end Regorus
diff --git a/formal/Regorus/Value/SourceValue.lean b/formal/Regorus/Value/SourceValue.lean
new file mode 100644
index 00000000..34f4f4cb
--- /dev/null
+++ b/formal/Regorus/Value/SourceValue.lean
@@ -0,0 +1,179 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.Value.Canonical
+import Regorus.Value.Truth
+
+/-!
+# Bottom-free source values
+
+`SourceValue` has no `Undefined` constructor.  More strongly, recursive
+containers can contain only other `SourceValue`s, so bottom cannot be hidden
+inside an array, set, object key, or object value.
+-/
+
+namespace Regorus
+
+inductive SourceValue where
+  | Null
+  | Bool (b : Bool)
+  | Number (n : RegoNumber)
+  | String (s : String)
+  | Array (a : List SourceValue)
+  | Set (s : List SourceValue)
+  | Object (o : List (SourceValue × SourceValue))
+  deriving Repr
+
+namespace SourceValue
+
+mutual
+  /-- Total embedding of the bottom-free source domain into semantic values.
+  `Set`/`Object` go through the canonical smart constructors so that source
+  values built with duplicate/unordered elements still respect the `Value`
+  representation invariant (e.g. `Set [Null, Null]` embeds as a one-element
+  set, matching Rust's `BTreeSet`/`BTreeMap`-backed collections). -/
+  def embed : SourceValue → Value
+    | .Null => .Null
+    | .Bool b => .Bool b
+    | .Number n => .Number n
+    | .String s => .String s
+    | .Array xs => .Array (embedList xs)
+    | .Set xs => Value.mkSet (embedList xs)
+    | .Object xs => Value.mkObject (embedObject xs)
+
+  def embedList : List SourceValue → List Value
+    | [] => []
+    | x :: xs => embed x :: embedList xs
+
+  def embedObject :
+      List (SourceValue × SourceValue) → List (Value × Value)
+    | [] => []
+    | (k, v) :: xs => (embed k, embed v) :: embedObject xs
+end
+
+instance : Coe SourceValue Value := ⟨embed⟩
+
+end SourceValue
+
+namespace Value
+
+mutual
+  /-- No occurrence of `Undefined`, including recursively in containers. -/
+  def BottomFree : Value → Prop
+    | .Undefined => False
+    | .Array xs | .Set xs => ListBottomFree xs
+    | .Object xs => ObjectBottomFree xs
+    | _ => True
+
+  def ListBottomFree : List Value → Prop
+    | [] => True
+    | x :: xs => BottomFree x ∧ ListBottomFree xs
+
+  def ObjectBottomFree : List (Value × Value) → Prop
+    | [] => True
+    | (k, v) :: xs =>
+        BottomFree k ∧ BottomFree v ∧ ObjectBottomFree xs
+end
+
+theorem BottomFree.ne_undefined {v : Value} (h : BottomFree v) :
+    v ≠ .Undefined := by
+  intro hv
+  subst v
+  exact h
+
+theorem ListBottomFree.of_forall_mem {xs : List Value}
+    (h : ∀ x ∈ xs, BottomFree x) : ListBottomFree xs := by
+  induction xs with
+  | nil => trivial
+  | cons x xs ih =>
+      exact ⟨h x (List.mem_cons_self ..),
+        ih fun y hy => h y (List.mem_cons_of_mem _ hy)⟩
+
+theorem ListBottomFree.forall_mem {xs : List Value}
+    (h : ListBottomFree xs) : ∀ x ∈ xs, BottomFree x := by
+  induction xs with
+  | nil => intro x hx; cases hx
+  | cons y xs ih =>
+      intro x hx
+      rcases List.mem_cons.mp hx with rfl | hx
+      · exact h.1
+      · exact ih h.2 x hx
+
+theorem ObjectBottomFree.of_forall_mem {xs : List (Value × Value)}
+    (h : ∀ p ∈ xs, BottomFree p.1 ∧ BottomFree p.2) : ObjectBottomFree xs := by
+  induction xs with
+  | nil => trivial
+  | cons p xs ih =>
+      obtain ⟨k, v⟩ := p
+      exact ⟨(h (k, v) (List.mem_cons_self ..)).1,
+        (h (k, v) (List.mem_cons_self ..)).2,
+        ih fun q hq => h q (List.mem_cons_of_mem _ hq)⟩
+
+theorem ObjectBottomFree.forall_mem {xs : List (Value × Value)}
+    (h : ObjectBottomFree xs) : ∀ p ∈ xs, BottomFree p.1 ∧ BottomFree p.2 := by
+  induction xs with
+  | nil => intro p hp; cases hp
+  | cons q xs ih =>
+      obtain ⟨k, v⟩ := q
+      intro p hp
+      rcases List.mem_cons.mp hp with rfl | hp
+      · exact ⟨h.1, h.2.1⟩
+      · exact ih h.2.2 p hp
+
+end Value
+
+namespace SourceValue
+
+mutual
+  theorem embed_bottomFree (s : SourceValue) :
+      Value.BottomFree s.embed := by
+    cases s with
+    | Null => trivial
+    | Bool _ => trivial
+    | Number _ => trivial
+    | String _ => trivial
+    | Array xs => exact embedList_bottomFree xs
+    | Set xs =>
+        show Value.ListBottomFree (Value.canonicalizeSet (embedList xs))
+        exact Value.ListBottomFree.of_forall_mem fun v hv =>
+          (embedList_bottomFree xs).forall_mem v (Value.mem_canonicalizeSet.mp hv)
+    | Object xs =>
+        show Value.ObjectBottomFree (Value.canonicalizeObject (embedObject xs))
+        exact Value.ObjectBottomFree.of_forall_mem fun p hp =>
+          (embedObject_bottomFree xs).forall_mem p (Value.mem_canonicalizeObject hp)
+  termination_by sizeOf s
+
+  theorem embedList_bottomFree (xs : List SourceValue) :
+      Value.ListBottomFree (embedList xs) := by
+    cases xs with
+    | nil => simp [embedList, Value.ListBottomFree]
+    | cons x xs =>
+        exact ⟨embed_bottomFree x, embedList_bottomFree xs⟩
+  termination_by sizeOf xs
+
+  theorem embedObject_bottomFree
+      (xs : List (SourceValue × SourceValue)) :
+      Value.ObjectBottomFree (embedObject xs) := by
+    cases xs with
+    | nil => simp [embedObject, Value.ObjectBottomFree]
+    | cons x xs =>
+        rcases x with ⟨k, v⟩
+        exact ⟨embed_bottomFree k, embed_bottomFree v,
+          embedObject_bottomFree xs⟩
+  termination_by sizeOf xs
+end
+
+/-- Every source value embeds to a defined (non-bottom) semantic value. -/
+@[simp] theorem embed_ne_undefined (s : SourceValue) :
+    s.embed ≠ Value.Undefined :=
+  (embed_bottomFree s).ne_undefined
+
+@[simp] theorem guardNotUndefined_embed (s : SourceValue) :
+    guardNotUndefined s.embed = true :=
+  (guardNotUndefined_spec s.embed).2 (embed_ne_undefined s)
+
+end SourceValue
+
+end Regorus
diff --git a/formal/Regorus/Value/Truth.lean b/formal/Regorus/Value/Truth.lean
new file mode 100644
index 00000000..0651714f
--- /dev/null
+++ b/formal/Regorus/Value/Truth.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Regorus.Value.Value
+
+/-!
+# Rego truth and bottom propagation
+
+Regorus does not identify `Undefined` with Boolean false.  They agree at a
+condition guard, but differ at guards that test definedness and remain distinct
+values throughout evaluation.  The definitions below mirror the RVM `Not` and
+`Guard` instruction cases.
+-/
+
+namespace Regorus
+
+/-- Rego/RVM truthiness: only `false` and bottom are not truthy. -/
+def isTruthy : Value → _root_.Bool
+  | .Bool false | .Undefined => false
+  | _ => true
+
+/-- RVM logical negation, including its asymmetric treatment of bottom. -/
+def notRvm : Value → Value
+  | .Undefined | .Bool false => .Bool true
+  | _ => .Bool false
+
+/-- Condition guard: reject exactly bottom and Boolean false. -/
+def guardCondition : Value → _root_.Bool
+  | .Undefined | .Bool false => false
+  | _ => true
+
+/-- Definedness guard: reject bottom, but accept every ordinary value. -/
+def guardNotUndefined : Value → _root_.Bool
+  | .Undefined => false
+  | _ => true
+
+/-- Strict binary bottom lifting used by ordinary two-argument operations. -/
+def lift₂ (f : Value → Value → Value) : Value → Value → Value
+  | .Undefined, _ | _, .Undefined => .Undefined
+  | x, y => f x y
+
+@[simp] theorem isTruthy_false : isTruthy (.Bool false) = false := rfl
+@[simp] theorem isTruthy_true : isTruthy (.Bool true) = true := rfl
+@[simp] theorem isTruthy_undefined : isTruthy .Undefined = false := rfl
+
+theorem isTruthy_eq_false_iff (v : Value) :
+    isTruthy v = false ↔ v = .Bool false ∨ v = .Undefined := by
+  cases v <;> simp [isTruthy]
+  case Bool b => cases b <;> simp [isTruthy]
+
+theorem isTruthy_eq_true_iff (v : Value) :
+    isTruthy v = true ↔ v ≠ .Bool false ∧ v ≠ .Undefined := by
+  cases v <;> simp [isTruthy]
+  case Bool b => cases b <;> simp [isTruthy]
+
+@[simp] theorem guardCondition_eq_isTruthy (v : Value) :
+    guardCondition v = isTruthy v := by
+  cases v <;> try rfl
+  case Bool b => cases b <;> rfl
+
+theorem guardCondition_spec (v : Value) :
+    guardCondition v = true ↔ v ≠ .Undefined ∧ v ≠ .Bool false := by
+  rw [guardCondition_eq_isTruthy, isTruthy_eq_true_iff]
+  tauto
+
+theorem guardNotUndefined_spec (v : Value) :
+    guardNotUndefined v = true ↔ v ≠ .Undefined := by
+  cases v <;> simp [guardNotUndefined]
+
+theorem guardNotUndefined_eq_false_iff (v : Value) :
+    guardNotUndefined v = false ↔ v = .Undefined := by
+  cases v <;> simp [guardNotUndefined]
+
+theorem guardCondition_implies_defined {v : Value}
+    (h : guardCondition v = true) : guardNotUndefined v = true := by
+  have hv := (guardCondition_spec v).1 h
+  exact (guardNotUndefined_spec v).2 hv.1
+
+@[simp] theorem notRvm_eq_boolean_not (v : Value) :
+    notRvm v = .Bool (!isTruthy v) := by
+  cases v <;> try rfl
+  case Bool b => cases b <;> rfl
+
+theorem notRvm_true_iff (v : Value) :
+    notRvm v = .Bool true ↔ v = .Undefined ∨ v = .Bool false := by
+  cases v <;> simp [notRvm]
+  case Bool b => cases b <;> simp [notRvm]
+
+theorem notRvm_false_iff (v : Value) :
+    notRvm v = .Bool false ↔ v ≠ .Undefined ∧ v ≠ .Bool false := by
+  rw [notRvm_eq_boolean_not]
+  cases v <;> simp [isTruthy]
+  case Bool b => cases b <;> simp [isTruthy]
+
+@[simp] theorem isTruthy_notRvm (v : Value) :
+    isTruthy (notRvm v) = !isTruthy v := by
+  rw [notRvm_eq_boolean_not]
+  cases isTruthy v <;> rfl
+
+/-- Negating twice Booleanizes a value rather than recovering a non-Boolean operand. -/
+@[simp] theorem notRvm_twice (v : Value) :
+    notRvm (notRvm v) = .Bool (isTruthy v) := by
+  cases v <;> try rfl
+  case Bool b => cases b <;> rfl
+
+@[simp] theorem lift₂_left_bottom (f : Value → Value → Value) (v : Value) :
+    lift₂ f .Undefined v = .Undefined := by
+  cases v <;> rfl
+
+@[simp] theorem lift₂_right_bottom (f : Value → Value → Value) (v : Value) :
+    lift₂ f v .Undefined = .Undefined := by
+  cases v <;> rfl
+
+theorem lift₂_of_defined (f : Value → Value → Value) {x y : Value}
+    (hx : x ≠ .Undefined) (hy : y ≠ .Undefined) :
+    lift₂ f x y = f x y := by
+  cases x <;> cases y <;> simp_all [lift₂]
+
+theorem lift₂_eq_undefined_iff (f : Value → Value → Value) (x y : Value) :
+    lift₂ f x y = .Undefined ↔
+      x = .Undefined ∨ y = .Undefined ∨ f x y = .Undefined := by
+  cases x <;> cases y <;> simp [lift₂]
+
+theorem lift₂_defined (f : Value → Value → Value) {x y : Value}
+    (hx : x ≠ .Undefined) (hy : y ≠ .Undefined)
+    (hf : f x y ≠ .Undefined) :
+    lift₂ f x y ≠ .Undefined := by
+  rw [lift₂_of_defined f hx hy]
+  exact hf
+
+theorem lift₂_comm (f : Value → Value → Value)
+    (hcomm : ∀ x y, f x y = f y x) (x y : Value) :
+    lift₂ f x y = lift₂ f y x := by
+  cases x <;> cases y <;> simp [lift₂, hcomm]
+
+end Regorus
diff --git a/formal/Regorus/Value/Value.lean b/formal/Regorus/Value/Value.lean
new file mode 100644
index 00000000..9b8cfa55
--- /dev/null
+++ b/formal/Regorus/Value/Value.lean
@@ -0,0 +1,297 @@
+/-
+Copyright (c) Microsoft Corporation.
+Licensed under the MIT License.
+-/
+
+import Batteries.Classes.Order
+import Mathlib.Data.String.Basic
+import Regorus.Value.RegoNumber
+
+/-!
+# Mathematical Regorus values
+
+This is the finite, exact value domain used for semantic proofs.  Set and
+object payload lists represent unordered mathematical sets and maps.  They are
+canonicalized at the construction boundary (see `Regorus.Value.Canonical`);
+the stored sort order is a choice function for a permutation-equivalence
+class, not part of semantic identity.  This is established by
+`canonicalizeSet_perm` and `canonicalizeObject_perm` (the latter on inputs
+with unique keys, because last-write-wins intentionally distinguishes
+conflicting duplicate-key orders).  Consequently `beq` and `compareValue`,
+although structural on the payload lists, are representation-independent for
+values built with `mkSet` and `mkObject`.
+
+Lean's automatic equality derivation cannot recurse through the nested
+`List Value` occurrences.  Equality and comparison are consequently defined
+as explicit mutually recursive programs.  Their termination is witnessed by
+`nodeCount`, and equality is proved extensionally correct below.
+-/
+
+namespace Regorus
+
+inductive Value where
+  | Null
+  | Bool (b : Bool)
+  | Number (n : RegoNumber)
+  | String (s : String)
+  | Array (a : List Value)
+  | Set (s : List Value)
+  | Object (o : List (Value × Value))
+  | Undefined
+  deriving Repr
+
+namespace Value
+
+mutual
+  /-- Number of value and list-cell nodes in a value. -/
+  @[simp] def nodeCount : Value → Nat
+    | .Null | .Bool _ | .Number _ | .String _ | .Undefined => 1
+    | .Array xs | .Set xs => listNodeCount xs + 1
+    | .Object xs => objectNodeCount xs + 1
+
+  @[simp] def listNodeCount : List Value → Nat
+    | [] => 0
+    | x :: xs => nodeCount x + listNodeCount xs + 1
+
+  @[simp] def objectNodeCount : List (Value × Value) → Nat
+    | [] => 0
+    | (k, v) :: xs => nodeCount k + nodeCount v + objectNodeCount xs + 1
+end
+
+@[simp] theorem nodeCount_pos (v : Value) : 0 < nodeCount v := by
+  cases v <;> simp
+
+def Smaller (x y : Value) : Prop :=
+  nodeCount x < nodeCount y
+
+theorem smaller_wellFounded : WellFounded Smaller :=
+  Nat.lt_wfRel.wf.onFun
+
+mutual
+  /-- Structural Boolean equality for values. -/
+  def beq : Value → Value → _root_.Bool
+    | .Null, .Null | .Undefined, .Undefined => true
+    | .Bool x, .Bool y => x == y
+    | .Number x, .Number y => x == y
+    | .String x, .String y => x == y
+    | .Array xs, .Array ys | .Set xs, .Set ys => listBeq xs ys
+    | .Object xs, .Object ys => objectBeq xs ys
+    | _, _ => false
+
+  def listBeq : List Value → List Value → _root_.Bool
+    | [], [] => true
+    | x :: xs, y :: ys => beq x y && listBeq xs ys
+    | _, _ => false
+
+  def objectBeq : List (Value × Value) → List (Value × Value) → _root_.Bool
+    | [], [] => true
+    | (kx, vx) :: xs, (ky, vy) :: ys =>
+        beq kx ky && beq vx vy && objectBeq xs ys
+    | _, _ => false
+end
+
+mutual
+  theorem beq_eq_true_iff (x y : Value) : beq x y = true ↔ x = y := by
+    cases x <;> cases y <;> simp [beq] <;>
+      first | exact listBeq_eq_true_iff _ _ | exact objectBeq_eq_true_iff _ _
+  termination_by nodeCount x + nodeCount y
+
+  theorem listBeq_eq_true_iff (xs ys : List Value) :
+      listBeq xs ys = true ↔ xs = ys := by
+    cases xs with
+    | nil => cases ys <;> simp [listBeq]
+    | cons x xs =>
+        cases ys with
+        | nil => simp [listBeq]
+        | cons y ys =>
+            simp [listBeq, beq_eq_true_iff x y, listBeq_eq_true_iff xs ys]
+  termination_by listNodeCount xs + listNodeCount ys
+
+  theorem objectBeq_eq_true_iff
+      (xs ys : List (Value × Value)) :
+      objectBeq xs ys = true ↔ xs = ys := by
+    cases xs with
+    | nil => cases ys <;> simp [objectBeq]
+    | cons x xs =>
+        cases ys with
+        | nil => simp [objectBeq]
+        | cons y ys =>
+            rcases x with ⟨kx, vx⟩
+            rcases y with ⟨ky, vy⟩
+            simp [objectBeq, beq_eq_true_iff kx ky, beq_eq_true_iff vx vy,
+              objectBeq_eq_true_iff xs ys]
+  termination_by objectNodeCount xs + objectNodeCount ys
+end
+
+instance : BEq Value := ⟨beq⟩
+
+instance : LawfulBEq Value where
+  rfl := (beq_eq_true_iff _ _).2 rfl
+  eq_of_beq h := (beq_eq_true_iff _ _).1 h
+
+/-- Decidable structural equality, obtained from the terminating Boolean equality. -/
+instance : DecidableEq Value := fun x y =>
+  decidable_of_iff (beq x y = true) (beq_eq_true_iff x y)
+
+/-- Constructor rank, matching Rust declaration order. -/
+def kindRank : Value → Nat
+  | .Null => 0
+  | .Bool _ => 1
+  | .Number _ => 2
+  | .String _ => 3
+  | .Array _ => 4
+  | .Set _ => 5
+  | .Object _ => 6
+  | .Undefined => 7
+
+mutual
+  /-- Rust-compatible heterogeneous comparison. -/
+  def compareValue (x y : Value) : Ordering :=
+    match x, y with
+    | .Null, .Null | .Undefined, .Undefined => .eq
+    | .Bool a, .Bool b => compare a b
+    | .Number a, .Number b => compare a b
+    | .String a, .String b => compare a b
+    | .Array xs, .Array ys | .Set xs, .Set ys => compareList xs ys
+    | .Object xs, .Object ys => compareObject xs ys
+    | a, b => compare a.kindRank b.kindRank
+
+  /-- Lexicographic comparison of array and canonical set payloads. -/
+  def compareList : List Value → List Value → Ordering
+    | [], [] => .eq
+    | [], _ :: _ => .lt
+    | _ :: _, [] => .gt
+    | x :: xs, y :: ys => (compareValue x y).then (compareList xs ys)
+
+  /-- Lexicographic key-then-value comparison of canonical object payloads. -/
+  def compareObject :
+      List (Value × Value) → List (Value × Value) → Ordering
+    | [], [] => .eq
+    | [], _ :: _ => .lt
+    | _ :: _, [] => .gt
+    | (kx, vx) :: xs, (ky, vy) :: ys =>
+        (compareValue kx ky).then
+          ((compareValue vx vy).then (compareObject xs ys))
+end
+
+instance : Ord Value := ⟨compareValue⟩
+
+@[simp] theorem compare_eq_compareValue (x y : Value) :
+    compare x y = compareValue x y := rfl
+
+mutual
+  /-- The comparator returns equality exactly for structural equality. -/
+  theorem compareValue_eq_eq_iff (x y : Value) :
+      compareValue x y = .eq ↔ x = y := by
+    cases x <;> cases y <;>
+      simp [compareValue, kindRank, compare_eq_iff_eq] <;>
+      first
+      | exact compareList_eq_eq_iff _ _
+      | exact compareObject_eq_eq_iff _ _
+  termination_by nodeCount x + nodeCount y
+
+  theorem compareList_eq_eq_iff (xs ys : List Value) :
+      compareList xs ys = .eq ↔ xs = ys := by
+    cases xs with
+    | nil => cases ys <;> simp [compareList]
+    | cons x xs =>
+        cases ys with
+        | nil => simp [compareList]
+        | cons y ys =>
+            rw [compareList, Ordering.then_eq_eq, compareValue_eq_eq_iff,
+              compareList_eq_eq_iff]
+            simp
+  termination_by listNodeCount xs + listNodeCount ys
+
+  theorem compareObject_eq_eq_iff
+      (xs ys : List (Value × Value)) :
+      compareObject xs ys = .eq ↔ xs = ys := by
+    cases xs with
+    | nil => cases ys <;> simp [compareObject]
+    | cons x xs =>
+        cases ys with
+        | nil => simp [compareObject]
+        | cons y ys =>
+            rcases x with ⟨kx, vx⟩
+            rcases y with ⟨ky, vy⟩
+            rw [compareObject, Ordering.then_eq_eq, compareValue_eq_eq_iff,
+              Ordering.then_eq_eq, compareValue_eq_eq_iff,
+              compareObject_eq_eq_iff]
+            constructor
+            · rintro ⟨hk, hv, ht⟩
+              subst ky
+              subst vy
+              subst ys
+              rfl
+            · intro h
+              have hp : (kx, vx) = (ky, vy) := (List.cons.inj h).1
+              have ht : xs = ys := (List.cons.inj h).2
+              exact ⟨congrArg Prod.fst hp, congrArg Prod.snd hp, ht⟩
+  termination_by objectNodeCount xs + objectNodeCount ys
+end
+
+theorem compare_eq_iff_eq (x y : Value) :
+    compare x y = .eq ↔ x = y :=
+  compareValue_eq_eq_iff x y
+
+mutual
+  /-- `compareValue` is oriented: reversing its arguments swaps the result. -/
+  theorem compareValue_swap (x y : Value) :
+      (compareValue x y).swap = compareValue y x := by
+    cases x <;> cases y <;>
+      simp [compareValue, kindRank, Ordering.swap_then] <;>
+      first
+      | rfl
+      | exact Batteries.OrientedCmp.symm _ _
+      | exact compareList_swap _ _
+      | exact compareObject_swap _ _
+  termination_by nodeCount x + nodeCount y
+
+  theorem compareList_swap (xs ys : List Value) :
+      (compareList xs ys).swap = compareList ys xs := by
+    cases xs with
+    | nil => cases ys <;> rfl
+    | cons x xs =>
+        cases ys with
+        | nil => rfl
+        | cons y ys =>
+            simp only [compareList, Ordering.swap_then]
+            rw [compareValue_swap, compareList_swap]
+  termination_by listNodeCount xs + listNodeCount ys
+
+  theorem compareObject_swap
+      (xs ys : List (Value × Value)) :
+      (compareObject xs ys).swap = compareObject ys xs := by
+    cases xs with
+    | nil => cases ys <;> rfl
+    | cons x xs =>
+        cases ys with
+        | nil => rfl
+        | cons y ys =>
+            rcases x with ⟨kx, vx⟩
+            rcases y with ⟨ky, vy⟩
+            simp only [compareObject, Ordering.swap_then]
+            rw [compareValue_swap, compareValue_swap, compareObject_swap]
+  termination_by objectNodeCount xs + objectNodeCount ys
+end
+
+theorem compare_of_kindRank_lt {x y : Value}
+    (h : x.kindRank < y.kindRank) : compareValue x y = .lt := by
+  cases x <;> cases y <;> simp [kindRank, compareValue] at h ⊢ <;> decide
+
+/-- `Undefined` is the final constructor in the heterogeneous order. -/
+@[simp] theorem compare_undefined (v : Value) :
+    compareValue v .Undefined = if v = .Undefined then .eq else .lt := by
+  cases v <;> simp [compareValue, kindRank] <;> decide
+
+@[simp] theorem undefined_compare (v : Value) :
+    compareValue .Undefined v = if v = .Undefined then .eq else .gt := by
+  cases v <;> simp [compareValue, kindRank] <;> decide
+
+theorem compare_lt_undefined {v : Value} (h : v ≠ .Undefined) :
+    compareValue v .Undefined = .lt := by
+  rw [compare_undefined, if_neg h]
+
+end Value
+
+end Regorus
diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
new file mode 100644
index 00000000..67f18e79
--- /dev/null
+++ b/formal/lake-manifest.json
@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.44",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.13.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Regorus",
+ "lakeDir": ".lake"}
diff --git a/formal/lakefile.lean b/formal/lakefile.lean
new file mode 100644
index 00000000..e6ad2bb7
--- /dev/null
+++ b/formal/lakefile.lean
@@ -0,0 +1,19 @@
+import Lake
+
+open Lake DSL
+
+package Regorus where
+  version := v!"0.1.0"
+  leanOptions := #[
+    ⟨`autoImplicit, false⟩,
+    ⟨`warningAsError, true⟩
+  ]
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.13.0"
+
+@[default_target]
+lean_lib Regorus
+
+lean_exe regorusFormal where
+  root := `Main
diff --git a/formal/lean-toolchain b/formal/lean-toolchain
new file mode 100644
index 00000000..4f86f953
--- /dev/null
+++ b/formal/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0