Add Lean 4 formalization of Value lattice and RVM core semantics

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

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/

formal/Main.lean

@@ -0,0 +1,4 @@
+import Regorus
+
+def main : IO Unit :=
+  IO.println "Regorus Value formalization"

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

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

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

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