Add Lean 4 formalization of Value lattice and RVM core semantics

[Anand Krishnamoorthi (anakrish)]

Summary

Introduces a formal/ Lean 4 (Lake) package with a mechanized formalization of Regorus, following the precedent set by AWS Cedar's Lean formal spec / differential-random-testing approach. This is an independent, additive layer alongside the existing Verus proofs (src/verify/) — it targets whole-language semantics and compiler/VM correctness properties that are a better fit for Lean's tactic/proof-term style than Verus's SMT-based approach.

What's formalized so far

Value lattice (formal/Regorus/Value/)

• RawNumber.lean — bit-exact Int64/UInt64/BigInt/F64Bits model mirroring src/number.rs, including Rust's non-lawful equality/ordering (NaN, lossy BigInt/f64 comparisons) — consistent with src/verify/number_proofs.rs, which already documents that Number::eq/cmp do not satisfy obeys_eq_spec/obeys_cmp_spec.
• RegoNumber.lean — a separate, lawful exact-rational number model (LinearOrder, DecidableEq) used for the mathematical Value model and all proofs.
• RawValue.lean / Value.lean — representation-level and canonical Value types, with proved-terminating mutually recursive beq/compareValue, matching Rust's derived Ord (Null < Bool < Number < String < Array < Set < Object < Undefined, with Undefined sorted last despite being semantically bottom).
• Canonical.lean — proves Set/Object are semantically unordered collections: canonicalizeSet/canonicalizeObject (sort + last-write-wins dedup for objects) with proved permutation-invariance (canonicalizeSet_perm, mkSet_perm, canonicalizeObject_perm/mkObject_perm, the latter honestly scoped to Nodup keys, since duplicate-key permutation invariance is false in general under last-write-wins).
• Truth.lean — isTruthy/notRvm/guard conditions and strict-bottom-propagation lifting (lift₂), with proved algebraic properties.
• SourceValue.lean — a bottom-free value subtype with an embedding into Value, proved to always be defined.

RVM phase 1 (formal/Regorus/RVM/)

• Bytecode.lean / Program.lean — instruction set and program representation mirroring src/rvm/, with in-scope core instructions (load/move, arithmetic/comparison/logical, guards, simple collection construction, index/contains/count, return/halt) fully modeled; out-of-scope instructions (loops, comprehensions, rule calls, virtual-data, HostAwait, Azure Policy opcodes) present as explicit placeholders.
• State.lean — VMState/VMStatus/VMError with bounds-checked register access.
• Step.lean — executable step and relational Step small-step semantics with proved equivalence (step_iff_Step), determinism (Step.deterministic), register-framing lemmas, and strict-bottom-propagation corollaries for arithmetic/comparison/logical instructions.

All proofs are complete — zero sorry/admit anywhere in formal/.

CI

Adds .github/workflows/lean.yml, modeled on the conventions of .github/workflows/verus.yml (pinned action SHAs, minimal permissions: contents: read, manual toolchain install, set -euxo pipefail):

• Installs elan pinned to formal/lean-toolchain.
• Caches formal/.lake keyed on the toolchain + lake-manifest.json hash.
• Fetches precompiled Mathlib .olean files via lake exe cache get (tolerant of cache misses; lake build falls back to compiling anything missing).
• Runs lake build.
• Explicitly greps for sorry/admit and fails the job if found, since lake build only warns (does not error) on sorry.

Scoped to trigger only on changes under formal/** or the workflow file itself.

Why this is useful

• A machine-checked, independent reference semantics for Value and the RVM core step relation, usable as a differential-testing oracle against the Rust implementation (à la Cedar's DRT pipeline).
• A foundation for future compiler-correctness proofs (Rego/Azure Policy AST → RVM bytecode) and RVM verifier soundness proofs.
• Explicitly documents and formalizes subtle invariants that are easy to get wrong in the Rust code: non-lawful Number comparison, Undefined's dual role as both semantic bottom and the greatest element in deterministic sort order, and the unordered-collection semantics of Set/Object despite their sorted BTreeSet/BTreeMap backing representation.

Scope / non-goals of this PR

This does not touch src/ (no behavior change to the Rust engine). It is purely an additive formal/ Lean package plus its CI workflow. Loops, comprehensions, rule evaluation/caching, suspendable execution (HostAwait), the static bytecode verifier, and AST-level compiler correctness are left for follow-up work.

[Copilot]

🟡 Changes recommended

Several formal semantics diverge from Rust behavior, and the CI installer executes mutable unverified upstream code.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Adds an independent Lean 4 formalization of Regorus value semantics and core RVM execution.

Changes:

• Models numbers, values, canonical collections, truthiness, and source values.
• Defines core RVM bytecode, state, execution, and proofs.
• Adds pinned Lean dependencies and CI validation.

File summaries

File	Description
formal/Regorus/Value/Value.lean	Defines canonical semantic values and ordering.
formal/Regorus/Value/Truth.lean	Models truthiness and undefined propagation.
formal/Regorus/Value/SourceValue.lean	Defines bottom-free source values.
formal/Regorus/Value/RegoNumber.lean	Adds lawful rational numbers.
formal/Regorus/Value/RawValue.lean	Models representation-level values.
formal/Regorus/Value/RawNumber.lean	Models Rust-compatible numeric representations.
formal/Regorus/Value/Canonical.lean	Canonicalizes sets and objects.
formal/Regorus/RVM/Step.lean	Implements core RVM transitions and proofs.
formal/Regorus/RVM/State.lean	Defines VM state and errors.
formal/Regorus/RVM/Program.lean	Defines formal RVM programs.
formal/Regorus/RVM/Bytecode.lean	Mirrors the RVM instruction set.
formal/Regorus/RVM.lean	Aggregates RVM modules.
formal/Regorus.lean	Aggregates the formalization.
formal/Main.lean	Adds a minimal executable entry point.
formal/lean-toolchain	Pins Lean 4.13.0.
formal/lakefile.lean	Configures the Lake package.
formal/lake-manifest.json	Locks Lean dependencies.
formal/.gitignore	Excludes generated Lean artifacts.
.github/workflows/lean.yml	Builds and validates proofs in CI.

Review details

Suppressed comments (4)

formal/Regorus/RVM/Step.lean:99

• This also applies heterogeneous ordering even though the modeled strict RVM rejects comparisons between different value variants. Add the same kind check used for the other ordered comparisons; otherwise Null ≤ Bool false succeeds instead of producing a type error.

    .ok (.Bool (decide (Value.compareValue left right ≠ .gt)))

formal/Regorus/RVM/Step.lean:103

• This also applies heterogeneous ordering even though the modeled strict RVM rejects comparisons between different value variants. Add a value-kind check; for example, Bool true > Null currently returns true instead of a type error.

    .ok (.Bool (decide (Value.compareValue left right = .gt)))

formal/Regorus/RVM/Step.lean:107

• This also applies heterogeneous ordering even though the modeled strict RVM rejects comparisons between different value variants. Add a value-kind check; otherwise cross-type inputs such as Bool true ≥ Null produce a Boolean result rather than a type error.

    .ok (.Bool (decide (Value.compareValue left right ≠ .lt)))

formal/Regorus/RVM/Step.lean:119

• RVM Or is not general truthiness: String "x" Or Bool false evaluates to Bool true here, but Rust rejects the non-Boolean operand in both strict and non-strict modes. Restrict this operation to the modeled mode's supported operand types.

    .ok (Regorus.lift₂
      (fun x y => .Bool (Regorus.isTruthy x || Regorus.isTruthy y))
      left right)

• Files reviewed: 19/19 changed files
• Comments generated: 5
• Review effort level: Balanced

---

💡 Configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

🔵 Needs a closer look

The CI command skips the newly introduced executable target, leaving Main.lean unchecked.

Review details

Suppressed comments (1)

Previously missed (1) — in code that hasn't changed since the last review.

.github/workflows/lean.yml:90

• The explicit @[default_target] is the Regorus library, so a bare lake build does not build the regorusFormal executable and Main.lean is never typechecked in CI. Build the executable target explicitly; it imports Regorus, so this still checks the full library as well.

• Files reviewed: 19/19 changed files
• Comments generated: 0 new
• Review effort level: Balanced

[Anand Krishnamoorthi (anakrish)]

Re the latest review ("CI command skips the newly introduced executable target, leaving Main.lean unchecked"): confirmed valid — @[default_target] in formal/lakefile.lean is only on lean_lib Regorus, so a bare lake build never builds/typechecks the regorusFormal executable (root Main.lean). Fixed by having CI run lake build regorusFormal explicitly, which still builds/checks the full Regorus library since the executable imports it.