[Lef Ioannidis (elefthei)]

Currently blocked on:

• Regorus PR fix(number): make equality and ordering exact #846, "fix(number): make equality and ordering exact" by Anand Krishnamoorthi (@anakrish). This PR is stacked on it (base fix/number-exact-ordering); GitHub retargets it to main when fix(number): make equality and ordering exact #846 merges.
• A Verus bug, external_trait_extension: inherited ensures can be checked before concrete eq_spec is defined verus-lang/verus#3298, "external_trait_extension: inherited ensures can be checked before concrete eq_spec is defined". I filed a fix, Add call-graph edges from trait method impls to the spec fns in their inherited specs verus-lang/verus#3300, linked on the issue. Until it lands, Verus reports the 2 errors described under Verification.

Adds history.match(policy, history, request) -> bool behind the opt-in history feature, which is not part of default or full-opa. A policy pairs a request pattern with a regular expression over past events. The builtin returns whether history (oldest event first) belongs to the pair's language for request. It works in the interpreter and the RVM, including no_std builds. Syntax and semantics are in docs/builtins.md, section "History/request policies".

Specification

HistoryMatchState::evaluate (src/builtins/history/mod.rs) is verified against an independent spec in src/verify/history_specs.rs:

result matches Ok(answer) ==>
    answer == policy_lang(value_view(*policy), value_view(*request), history_view(*history))

Expanding pair_lang gives:

policy_lang(policy, req, history) =
    exists|head: Head, tail: Regex<SrcTest>|
        decodes_policy(policy, head, tail)
        && exists|theta: Subst|
               head_match(head, req, theta)
               && theta.dom() == head_vars(head)
               && lang(|test, event| src_test_holds(theta, test, event), tail, history)

• decodes_policy decodes the JSON policy object.
• head_match binds the request variables (theta).
• lang is ordinary regular-language membership over event sequences (history_specs.rs:112).
• src_test_holds evaluates eq/neq/and/or on a single event under theta.

An Err result has no Boolean meaning.

Implementation

• Lazy symbolic derivatives run over a hash-consed bump store (hashconsius, verus-bumpalo, both pinned to git revisions). Each pair's graph is capped at 100 KiB. Timer and memory limits are enforced through ObservationWorld.
• The interpreter and the RVM each keep a HistoryMatchState. History errors are fatal (VmError::HistoryMatchFailure, HistoryMatchValidationError) and never turn into undefined.
• Numbers: Data::Number holds a canonical key {rank, units}. Two keys are equal exactly when fix(number): make equality and ordering exact #846's NumberView::cmp_values returns Equal (src/verify/value_numeric.rs, lemma_numeric_of_eq). Array path steps convert floats to indexes with float_array_index, which is proved equal to float_index_spec (Some(i) iff the float is exactly i and 0 <= i <= u64::MAX). Nothing saturates, so 2^64 as a float never selects u64::MAX.
• The Lean spec (verification/aeneas/history/lean/RegorusHistory/Spec/Data.lean) follows fix(number): make equality and ordering exact #846 for NaN: every NaN keeps its sign and payload, negative NaNs order below -inf, and positive NaNs order above +inf.
• The Lean/Aeneas extraction scaffold is in verification/aeneas/history (cargo xtask extract-history-lean).

Verification

Verus 0.2026.10.04.426d8b0 with vstd 0.0.0-2026-09-06-0133:

Command	Verified	Errors
cargo verus verify --locked	109	0
cargo verus verify --locked --features history	1132	2
cargo verus verify --locked --no-default-features --features history,arc,std	1121	2

Both errors are the inherited PartialEq postcondition (obeys_eq_spec() ==> r == self.eq_spec(other)) on Term::eq and Primitive::eq in src/builtins/history/kernel.rs. They come from verus-lang/verus#3298, a declaration-order bug: Verus can check the impl before the axioms of the spec helpers it inherits. The minimized reproducer is verification/verus/inherited_ensures_order.rs. Every other function verifies.

Runtime (Rust 1.95.0):

• cargo test --locked --features history: 572 passed.
• cargo test --locked --features history,cache: 572 passed.
• cargo test --locked --features history,rvm --test history_match: 6 passed.
• src/builtins/history/tests.rs::float_path_steps_index_arrays_exactly covers the new float index path: 1.0, 0.0, and -0.0 select elements; 1.5, -1.0, subnormals, 2^64, and 1e300 select nothing.
• cargo xtask ci-debug and cargo xtask test-no-std (thumbv7m-none-eabi) pass.

[Anand Krishnamoorthi (anakrish)]

Lef Ioannidis (@elefthei) This will likely cause problems in internal builds since it is not under microsoft org and can be used (in theory) for supply chain attacks.

[Anand Krishnamoorthi (anakrish)]

It would be nice if we can devise a cleaner syntax for this.

[Copilot]

🟡 Changes recommended

The new Git-only dependencies prevent crates.io publication of Regorus even when the history feature is disabled.

1 open issue

• Add registry versions for Git-only dependencies · New

What changed in this PR

Adds the opt-in history.match builtin to Regorus for matching prior events against request-bound policies. It builds on #846’s exact numeric equality and integrates with both the interpreter and RVM.

Changes:

• Adds matcher state, caching, resource-limit handling, and binding feature forwarding.
• Introduces formal specifications, proof support, semantic tests, and performance benchmarks.
• Documents policy syntax and verification boundaries, and adds history-enabled Verus CI checks.

File	Description
verification/​verus/​inherited_ensures_order.rs	Adds an upstream Verus bug reproducer.
tests/​history_match.rs	Tests evaluator parity, errors, and serialization.
src/​verify/​value_specs.rs	Defines mathematical value views.
src/​verify/​value_numeric.rs	Models exact numeric keys and array indexes.
src/​verify/​value_assumptions.rs	Specifies trusted value operations.
src/​verify/​mod.rs	Registers history verification modules.
src/​verify/​history_examples.rs	Connects example policies to evaluator contracts.
src/​verify/​history_assumptions.rs	Defines native and storage verification boundaries.
src/​value/​set/​mod.rs	Adds set views and structural proofs.
src/​value/​object/​mod.rs	Adds object views and structural proofs.
src/​value/​mod.rs	Enables verification of the Value representation.
src/​value/​array/​mod.rs	Adds array views and structural proofs.
src/​tests/​interpreter/​mod.rs	Exposes shared timer test support.
src/​rvm/​vm/​rules.rs	Propagates fatal matcher errors.
src/​rvm/​vm/​machine.rs	Owns and resets matcher state.
src/​rvm/​vm/​functions.rs	Dispatches contextual matching and maps errors.
src/​rvm/​vm/​execution.rs	Clarifies fatal-error handling comments.
src/​rvm/​vm/​errors.rs	Adds matcher-specific error variants.
src/​lib.rs	Enables allocator APIs for verification builds.
src/​interpreter.rs	Integrates matcher state and preserves fatal errors.
src/​builtins/​mod.rs	Registers and dispatches the builtin.
src/​builtins/​history/​tests.rs	Tests semantics, limits, cleanup, and numeric cases.
src/​builtins/​history/​mod.rs	Implements matcher state and pair caching.
src/​builtins/​history/​error.rs	Defines typed matcher errors.
docs/​builtins.md	Documents syntax, semantics, caching, and proofs.
Cargo.toml	Adds the feature, dependencies, and benchmark target.
Cargo.lock	Locks new matcher dependencies.
bindings/​wasm/​Cargo.toml	Forwards the opt-in history feature.
bindings/​wasm/​Cargo.lock	Locks matcher dependencies for WASM.
bindings/​ruby/​ext/​regorusrb/​Cargo.toml	Forwards the opt-in history feature.
bindings/​ruby/​Cargo.lock	Locks matcher dependencies for Ruby.
bindings/​python/​Cargo.toml	Forwards the opt-in history feature.
bindings/​python/​Cargo.lock	Locks matcher dependencies for Python.
bindings/​java/​Cargo.toml	Forwards the opt-in history feature.
bindings/​java/​Cargo.lock	Locks matcher dependencies for Java.
bindings/​ffi/​Cargo.toml	Forwards the opt-in history feature.
bindings/​ffi/​Cargo.lock	Locks matcher dependencies for FFI.
benches/​history_match.rs	Measures cold, cached, and incremental matching.
.github/​workflows/​verus.yml	Updates Verus and adds history verification profiles.

_{Review effort: Balanced}