Differential Tests

Two implementations answer the same scope question

A generator constructs a child and parent scope and converts each into reference and implementation representations. The reference evaluator in spec.rs and the Rust methods compute separate decisions; a mismatch fails the comparison, and Proptest then searches for a simpler input that still fails.

scope_diff.rs compares the reference with the public capability types and with the normalized kernel representation. Its checks include explicit fixtures, public-type comparisons, normalized projection and subset checks, and reference-only algebra properties. The reference evaluator calls nothing in the production evaluator, while input conversion stays part of the evidence: paired construction reduces accidental differences, a faulty projection can invalidate a comparison, and separate normalized projection tests check that relationship.

The default is 256 generated cases per property, with up to 10,000 shrink iterations. The strategies choose bounded collections from finite name pools: 0 to 7 tool grants, 0 to 3 resource and prompt grants each, and a present invocation cap from 1 through 99. A larger case count samples that domain more heavily without widening it. Read the generators and conversions before interpreting a pass; their local P1 to P8 comments number reference-only properties, separately from the formal property matrix.

The release lane runs at the default; a maintainer who suspects a sparse region raises PROPTEST_CASES for one target, as Qualification: formal gates shows.

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()
    );
}

//! 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;

A parent cap of 10 admits a child cap of 5 and refuses 11 or none

The first scope test fixes a parent invocation cap of 10 and checks three child caps in all three representations: the reference, the public capability types, and the normalized kernel scope.

Other authority fields stay part of each fixture. An absent parent cap imposes no bound on the field; the refusal fixture challenges the removal of an explicit one. The P1 walkthrough connects these cases to the attenuation theorem and its proof boundary.

Signed bytes match an independently written canonicalizer

canonical_json_diff.rs compares the production canonicalizer with a separately implemented oracle over generated JSON with integer numbers; floating-point shortest-form rendering is outside the oracle’s domain. The file also checks ordering, escaping, round trips, determinism, and fixed outputs, so some of its tests are invariants rather than oracle comparisons.

//! 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 committed regression file holds three seeds. One shrank to DEL, U+007F, and the focused regression asserts that DEL and U+009F stay unescaped in both the production and oracle output; another exercises UTF-16 object-key ordering. The test named nan_infinity_rejected checks that serde_json refuses to construct a Number from non-finite floats, before any value reaches the canonicalizer; frozen vectors and the wasm suite cover further number and rejection cases.

browser_canonical_json_diff.rs declares five wasm-bindgen tests and three native tests, one of which launches the wasm suite. Its auto mode uses headless Chrome when browser and driver versions match and falls back to Node, and a native summary can include an early return when the wasm C compiler or wasm-pack is missing. Set the runner to chrome for browser evidence or node for Node-hosted wasm; the crate has no browser Cargo feature.

The release lane sets the runner to chrome, so the recorded result is browser evidence.

Check the full output for setup skips. The compiler probe tries CC_wasm32_unknown_unknown, TARGET_CC, CC, then clang, so on macOS an installed LLVM compiler with wasm support can serve that target without changing the native compiler. The runner source defines the prerequisites and fallback.

Receipts, anchored roots, and treaty predicates agree across implementations

Each Cargo test target asks one question of two implementations:

• anchored_root. Rust and TypeScript produce matching receipt IDs, root bytes, and inclusion-proof structure over the replay fixtures. The TypeScript side runs the conformance source under Bun, and this parity test returns early when Bun is absent.
• anchored_root_tamper. Changed receipt bytes or mutated proof paths make both sides refuse the malformed evidence. These tests require Bun and fail without it.
• receipt_encoding_diff. Five default tests exercise canonical bodies, signature verification, idempotence, and round trips against constructed inputs and frozen vectors. Two live encoder comparisons are ignored by default and need explicit opt-in, the Python SDK import or the built TypeScript SDK, and the matching runtime.
• treaty_predicate_diff. Shared receipt and predicate data feed an independent reference interpreter and the bounded evaluator in chio-runtime-core. Three generated properties compare predicate evaluation, whole-constitution admission, and refinement over a supplied finite receipt domain, and a fourth fixture exercises each atom with a matching case.

The release lane opts into the live encoders with CHIO_LIVE_SDK_DIFFERENTIAL=1 against the Python and TypeScript SDKs it publishes, so the receipt bytes those packages produce are compared with the kernel's before they ship.

A live encoder test returns early for a missing runtime or SDK import and fails on an encoder exception or a byte mismatch, so read its diagnostics to confirm both encoders ran. Each live comparison uses one constructed receipt. The treaty suite fixes its case count at 1,024 over a refinement domain of 0 to 7 receipts, and its refinement agreement covers that finite domain. Its ScopeContains atom compares a target with receipt_id, which is narrower than capability-scope evaluation.

An eighth target, the receipt-before-allow regression, validates a retained Apalache trace and replays its scenario through a ChioKernel, and the crate also has unit tests. They share one Cargo package, and each supplies its own kind of evidence.

A disagreement becomes a retained regression

The whole crate runs before every release is tagged: the native comparisons, the live encoder targets with their Bun and SDK subprocesses, and the treaty suite at its fixed 1,024 cases. The proof report records the result against the tag's source commit, with every early-return message, so a skipped live encoder cannot pass as a comparison. Check it for the binary you run:

chio release verify --evidence formal

binary     /usr/local/bin/chio  chio 0.2.0  aarch64-apple-darwin
checksum   matches SHA256SUMS for v0.2.0
signed by  release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal     proof report bound to v0.2.0, every gate passed
           lean        root-imported theorems checked
           aeneas      production extraction and equivalence
           kani        public PR lane
           apalache    positive and negative invariants
           creusot     core contracts
           diff-tests  scope, canonical JSON, receipts, treaties
           timing      dudect threshold
verified

The diff-tests line is this crate. Maintainers run it, or one target with a larger sample, from source as Qualification: formal gates describes.

On a failure, start with the failing input and the two outputs. If the reference permits an operation that Rust refuses, check the intended rule and the projection; if Rust permits a child the reference rejects, inspect the widened authority. The implementation, the oracle, or the generator can each be wrong.

Shrinking follows the strategy’s simplification rules and configured limits, so the shrunk case is the smallest the strategy reached, which can exceed the global minimum. Proptest persists a seed and replays it before new cases, and a changed strategy can change what that seed produces, so keep an explicit regression too. The three canonical-JSON seeds and the DEL regression show both forms; Proptest documents persistence and shrinking.

Agreement supports a claim through the matrix that names it

The formal matrix declares differential_test evidence for P1 (capability attenuation), P4 (receipt integrity). The mapping locates supporting evidence for those properties; each file in the crate supports them only through the relationship it compares.

Next: inputs beyond the generator