Differential Tests

What differential testing does

proptest generates inputs, or replays a committed regression seed, runs both implementations on the same value, and asserts the outputs are equal. On a failure it shrinks toward a minimal input that still diverges, and the seed is committed to a tests/<name>.proptest-regressions file so later runs exercise it before any generated case.

The crate root states its own scope:

//! Differential testing: executable Chio reference spec vs the production
//! capability structs and the normalized proof-facing AST in `chio-kernel-core`.
//!
//! This crate is the shipped proof-style release gate for scope attenuation
//! semantics and the bounded treaty predicate fragment. The treaty oracle is
//! independent differential evidence. It does not establish a Lean extraction
//! or whole-runtime refinement proof.

pub mod counterexample;

pub mod generators;
#[cfg(not(target_arch = "wasm32"))]
#[path = "../../itf/receipt_before_allow.rs"]
mod receipt_before_allow_trace;
pub mod spec;

The two modules a harness draws on are:

• spec · the executable reference. It mirrors the chio_core::capability::* types and reimplements is_subset_of for SpecToolGrant, SpecResourceGrant, SpecPromptGrant and SpecChioScope without calling into chio-core.
• generators · proptest strategies producing paired (spec, impl) values built from the same source bits. The pairing is what guarantees the two implementations see equivalent inputs.

Two more sit alongside them, and together they are how a model-checker counterexample becomes a Rust test. counterexample exposes assert_trace_shape and replay_receipt_before_allow, the second of which drives a real ChioKernel. receipt_before_allow_trace is a #[path] include of formal/itf/receipt_before_allow.rs, which parses an Apalache ITF trace and requires the four variables allowed, budget_checked, clock and receipt_log. Both compile only off wasm32.

The harnesses

Eight test files under formal/diff-tests/tests/ exercise six surfaces. The count in the last column is the number of #[test] functions the file declares on a native target; the browser file declares five more under #[wasm_bindgen_test] that compile only for wasm32.

Scope subsumption

The headline harness pairs the spec's SpecChioScope::is_subset_of against the shipped chio_core::capability::ChioScope::is_subset_of. It sits inside a proptest! block, which is what makes the in arb_paired_scope_pair() argument syntax legal:

fn scope_subset_spec_matches_impl(
    ((spec_a, impl_a), (spec_b, impl_b)) in arb_paired_scope_pair()
) {
    let spec_result = spec_a.is_subset_of(&spec_b);
    let impl_result = impl_a.is_subset_of(&impl_b);

    prop_assert_eq!(
        spec_result, impl_result,
        "Scope subset mismatch!\n  spec: {}\n  impl: {}\n  child grants: {}\n  parent grants: {}",
        spec_result, impl_result, spec_a.grants.len(), spec_b.grants.len()
    );
}

Twelve differential properties run in this file: four base spec-against-impl subset checks (scope, tool grant, resource grant, prompt grant) at scope_diff.rs:471-536, then eight normalized variants pairing a projection check and a subset check for each of the four grant kinds at :538-630. Each runs 256 cases by default, read from PROPTEST_CASES at :29-42:

PROPTEST_CASES=4096 cargo test -p chio-formal-diff-tests --test scope_diff

The reference is formal/diff-tests/src/spec.rs, with SpecToolGrant::is_subset_of written for clarity. It mirrors the shipped Rust but does not call into it, so a regression in chio_core shows up as a divergence rather than a self-confirming pass. Agreement is not correctness: a mistake made identically on both sides passes.

The remaining twelve tests in the file are the four fixture-driven checks at the top and the eight standalone attenuation properties at scope_diff.rs:632-811, which assert on the spec side alone: the empty scope is a subset of any scope, subset is reflexive, removing a grant or an operation produces a subset, reducing max_invocations produces a subset, a wildcard tool name subsumes a specific one, different servers never produce a subset, and subset is transitive.

Canonical JSON

canonical_json_diff.rs cross-checks chio_core::canonical::canonicalize against an oracle defined in the same file, which its own header calls a deliberately small, separately-derived implementation of RFC 8785. The oracle exercises a subset of the production code paths: there is no f64 shortest-form rendering, and the proptest strategy is restricted to integer numbers so the two implementations agree byte for byte over the strategy's domain.

The file enumerates its own invariants in its module docstring:

//! The harness hosts at least six named property tests, each exercising one
//! invariant from RFC 8785 section 3:
//!
//!   1. `idempotence`              -- canonicalize(canonicalize(x)) == canonicalize(x)
//!   2. `key_sort_utf16`           -- object keys sort by UTF-16 code unit order
//!   3. `no_insignificant_whitespace` -- output has no whitespace outside string literals
//!   4. `integer_no_decimal_point` -- integer numbers serialize without trailing `.0`
//!   5. `string_minimal_escaping`  -- only required controls are escaped
//!   6. `parse_round_trip_equal`   -- parse(canonicalize(x)) is semantically equal to x
//!   7. `byte_stable_oracle_match` -- production output matches the independent oracle
//!   8. `valid_utf8_output`        -- output is always valid UTF-8
//!   9. `determinism`              -- two independent calls produce byte-equal output
//!  10. `null_bool_literals`       -- null/true/false serialize exactly
//!  11. `empty_collections`        -- {} and [] serialize exactly
//!  12. `nan_infinity_rejected`    -- non-finite numbers fail canonicalization

The file declares one test beyond that list, del_and_c1_controls_pass_through_in_production_and_oracle, which pins the escaping boundary the fifth invariant leaves open: DEL, the C1 controls, U+2028 and U+2029 pass through unescaped on both sides.

The manifest scopes what this reaches at formal/proof-manifest.toml:229 and :230: float-valued JSON leaves in compound receipt fields are outside the mechanized canonical-JSON domain, their production rendering stays covered by frozen vectors and ASSUME-CANONICAL-JSON, and refinement from the mechanized projection to crates/core/chio-core-types/src/canonical.rs is excluded beyond the checked integer-domain fixtures and these differential tests.

browser_canonical_json_diff.rs is a different shape from its name. On a native target it runs three tests: the Rust oracle against the frozen canonical vector bytes, a headless-browser wasm run against the same vectors, and a unit check on the RUSTFLAGS filter that run needs. The five parity properties named browser_wasm_* are #[wasm_bindgen_test] functions compiled only for wasm32, so they run inside the browser rather than beside it.

Anchored roots

anchored_root.rs emits the Rust-side (receipt_id, leaf_hash, inclusion_proof, root) tuple for the replay fixture corpus, and the TypeScript conformance runner at sdks/typescript/packages/conformance/src/replay.ts emits the same shape. The three tests check that the Rust side emits in deterministic order, that the two sides match by root bytes and proof structure, and that Rust fails closed on an invalid fixture root.

anchored_root_tamper.rs builds the same tuple shape from a canary replay fixture and mutates it four ways: flip a receipt byte, reverse odd-index sibling order, truncate a path, pad a path. Its stated contract is that Rust and TypeScript must reject the same malformed tuples, so a divergence here is one side accepting what the other rejects rather than a wrong root.

Both files shell out to the TypeScript runner, so they need node and the built conformance package on the machine that runs them.

Receipt encoding

receipt_encoding_diff.rs is a cross-language encoder check. Its stated contract is that the Rust, Python and TypeScript encoders emit byte-identical canonical JSON for the same receipt body, so that the kernel signature attaches to one agreed byte string.

By default the oracle is a corpus rather than a subprocess. The harness reads the receipt vectors at tests/bindings/vectors/receipt/v1.json, which the Python and TypeScript SDK test suites compare against in lockstep, so the three languages meet at the vector file instead of at a live process. Five tests run that way: the canonical body against the blessed vector bytes, signature verification against those canonical bytes, idempotence, round-trip stability, and one signed-receipt signature check.

The two live-encoder tests are #[ignore] by default and name their own opt-in in the skip line: live_python_encoder_matches_rust needs python3 with the chio-py SDK installed and live_ts_encoder_matches_rust needs node and the chio-ts SDK built. Both run under CHIO_LIVE_SDK_DIFFERENTIAL=1 cargo test -- --ignored. A machine without either toolchain skips them rather than failing.

Reproduce

The lane runs on a bare Rust toolchain and is one of the gate_commands entries in formal/proof-manifest.toml:

cargo test -p chio-formal-diff-tests

That builds nine test binaries: one for the crate's own unit tests and one per file in tests/. Two of them shell out to the TypeScript conformance runner and skip cleanly when it is absent, and the two live cross-SDK encoder tests stay ignored unless opted in.

One file at a time:

cargo test -p chio-formal-diff-tests --test scope_diff
cargo test -p chio-formal-diff-tests --test canonical_json_diff
cargo test -p chio-formal-diff-tests --test anchored_root
cargo test -p chio-formal-diff-tests --test receipt_encoding_diff
cargo test -p chio-formal-diff-tests --test treaty_predicate_diff

A heavier sweep, and the opt-in variants:

# more proptest cases per property
PROPTEST_CASES=4096 cargo test -p chio-formal-diff-tests

# the live Python and TypeScript encoders
CHIO_LIVE_SDK_DIFFERENTIAL=1 cargo test -p chio-formal-diff-tests -- --ignored

# the wasm32 parity properties, which need wasm-pack and a browser
wasm-pack test --node --features browser formal/diff-tests

The binary paths cargo prints under target/debug/deps/ carry a content-addressed suffix that moves on every rebuild. Match on the file name, never on the suffix.

What a divergence looks like

When the two sides disagree on a case, the prop_assert_eq! fails, proptest prints the failing input, and the shrinker starts. It repeatedly tries smaller inputs that still fail, converging on a minimal counterexample, and the panic message is the format string the harness wrote: for scope_subset_spec_matches_impl that is the spec verdict, the impl verdict, and both grant counts.

The shape of the report is what to read from it. A spec-true, impl-false result and a spec-false, impl-true result are different bugs, and the minimized input is the thing that tells you which axis broke. A path-prefix constraint that shrinks to a pair differing only in a trailing slash localises the disagreement to that comparison.

proptest writes the failing seed to a regression file beside the test, named tests/<test file>.proptest-regressions. One is committed today, tests/canonical_json_diff.proptest-regressions, holding three seeds. Its own header says the file is read automatically and its cases re-run before any novel ones, and each line records what the seed shrank to: one is shrinks to s = "\u{7f}", the DEL character that the escaping boundary test now pins.

Triage from there:

• Reproduce by re-running. The committed seed is exercised before any generated case, so the failure comes back first rather than after a wait.
• Classify. A spec bug means the reference disagrees with the protocol document; an implementation bug means the shipped code drifted; a generator bug means the strategy produced an input outside the domain either side promises to handle.
• Fix, re-run, and commit the regression seed with the fix so the counterexample stays pinned.

Relation to the other lanes

The crate root scopes itself: it is the shipped proof-style release gate for scope attenuation semantics and the bounded treaty predicate fragment, and the treaty oracle is independent differential evidence that does not establish a Lean extraction or whole-runtime refinement proof.

Against the neighbouring lanes:

• Lean and Aeneas · prove statements about a Lean model and about definitions extracted from registered Rust sources, under the assumptions the registry names. They hold for every input in their domain, and that domain is not the running program.
• Kani · explores selected Rust functions exhaustively inside a configured bound. It runs the shipped code, over the input shapes a harness builds.
• Differential tests · detect drift between two implementations across generated inputs. They run the shipped code on inputs nobody chose, and they cannot see a mistake both sides make.

The three cover different objects, and none of them subsumes another. A regression outside all three may still be caught by fuzzing or integration tests, which give coverage rather than a proof.

P1 in this lane

P1 is capability attenuation: a delegated capability can only narrow. The differential lane catches drift between the executable reference and the shipped Rust by running both implementations of is_subset_of on paired generated inputs and asserting they agree. The headline harness is scope_subset_spec_matches_impl, quoted above, and eleven further differential properties in the same file cover the three other grant kinds and the normalized layer.

arb_paired_scope_pair() builds one value and splits it into a SpecChioScope and a production ChioScope from the same source bits, so a failure is a genuine result difference rather than a conversion artifact. The default is 256 cases per property.

Concretely, suppose a change to ChioScope::is_subset_of in chio-core-types started accepting a wider child when parent.max_invocations is None. The Lean model and the spec-side SpecToolGrant::is_subset_of have not changed, so the Lean proofs still hold; the Aeneas lane covers formal_aeneas.rs rather than this function, so it is unaffected; and the Kani harnesses that pin this shape use concrete fixtures that might not carry a None parent cap. proptest draws an input where the spec says false and the new production code says true, the assertion fails, and the shrinker minimizes it. That is the gap this lane exists to cover: shipped Rust the other lanes do not reach, on inputs nobody chose.

The counterexample is committed as a seed beside the test so it is replayed first on every later run, and cargo test -p chio-formal-diff-tests is a gate_commands entry, so the lane runs wherever that manifest list is honoured.

See also

• Aeneas Pipeline · the proof-side lane for the same surfaces.
• Lean 4 Proofs · the proof structure that the differential tests complement.
• Kani Harnesses · the bounded model-checking lane on the same Rust paths.