Echovalidum

The echo, validated.

Echovalidum is a Python library for lattice-based memory. Every value is a Cell(value, trust, phase) living on a bounded trust-coherence lattice; every loop carries a declared termination bound; and every non-interference judgment can be discharged as a Z3 / QF_BV obligation and signed through a post-quantum attestation pipeline.

Rust hot path, Python analysis path

The echovalidum crate is the canonical implementation of the operations performed on every cell: ψ₁₆₈ embedding, gradient binding, trust clipping, alignment, meet, join, ordering, coherence, addition, and subtraction. Since 0.3.2 it also holds Memory64: its capability checks, page-table walk, TLB, and pages. The PyPI wheel exposes that crate through a thin private PyO3 module, echovalidum._native.

Python retains the analysis path: Cell convenience APIs, ct-echo, AST loop discovery, Z3 discharge, PQC signing, receipt construction, and the NumPy and pure-Python fallbacks used when the native extension is unavailable. The fallbacks are compatibility code and are parity-tested against the Rust engine.

It contributes a unified substrate for four things that are usually studied in isolation: refinement types over memory, Cayley-disjoint borrow checking, abstract interpretation with widening, and information-flow control sensitive to iteration count. The result is the first unified discharge of all four Sabelfeld–Sands (2000) iteration-count covert channels as kernel-checked attestations inside a single lattice substrate.

Internally codenamed Σoilith. Echovalidum is the public-facing brand for the v0.3.0 facade. The underlying engine, arena format, and 45+ soilith_* modules retain that name in the source tree, similar to how PyTorch ships the torch import name. Both spellings refer to the same objects; import echovalidum is the recommended public API.

Research build, not in the PyPI package. The Semantic OS substrate and its semantic-os kernel below belong to the Σoilith research tree.

Architecture: For the full Semantic OS Substrate evaluation (layer model, package matrix, boot sequence, maturity scorecard), see SEMANTIC_OS_SUBSTRATE.md in the Masterpieces RCP docs tree.

Kernel: Boot and run the substrate via semantic-os (or python soilith_substrate.py): semantic-os boot --profile wow3-full --rcp-root RCP_ROOT --verify-after, semantic-os verify, semantic-os-health (writes SUBSTRATE_HEALTH.json), semantic-os run program.sol --from-slice PATH.

ct-echo — the unified Z3 + PQC discharge of all four Sabelfeld-Sands channels

After pip install echovalidum the package installs a ct-echo console script. Run it on any Python file and it AST-extracts every for loop, discharges Ch1–Ch4 of the Sabelfeld-Sands (SS 2000) iteration-count covert channels through Z3, packs the four verdicts into a single PQC-attested bundle per loop, and writes a JSON receipt you can pin under a launch post.

# Audit real Python source, sign each loop's four-channel bundle,
# emit a parseable JSON receipt:
ct-echo --source path/to/loops.py --sign --receipt out.json

# Same as above, plus quantitative leakage analysis (bits/query)
# with Z3 certificates of the leak bound and adaptive K-query
# composition:
ct-echo --source path/to/loops.py --qif --budget 0.5 --queries 16 \
        --prove --sign --receipt out.json

# Or run the built-in 5-loop demo (no source files needed):
ct-echo --demo --sign --receipt out.json

The four Sabelfeld-Sands channels discharged by ct-echo:

Channel	Description	Z3 obligation
Ch1	loop bound NI — declared loop bound must not depend on HIGH	verify_loop_bound_ni
Ch2	outer-schedule NI — outer-loop count of nested loops must not depend on HIGH	verify_outer_schedule_ni
Ch3	touch-pattern NI — array indices read/written in the loop must not depend on HIGH	verify_touch_pattern_ni
Ch4	iteration-bound NI — a finite numeric ceiling exists on the iteration count	verify_iteration_bound

For each loop a single SSChannelBundle is built: the SHA-256 transcript digest commits to all four channel SMT-LIBs in fixed order, the PQC signature commits to the digest, and a third-party auditor verifies by (1) re-running the four Z3 checks on the published SMT-LIBs, (2) recomputing the digest, (3) verifying the signature against the digest with the signer's public key. Tampering with any single channel's proof changes the digest and breaks the signature.

Install

pip install echovalidum                # core
pip install "echovalidum[verify]"      # adds the Z3 backend (z3-solver)

Requires Python ≥ 3.10. The hard dependencies are numpy >= 1.24 and scipy >= 1.10. The Z3 backend is optional — empirical 2-trace NI checks work without it.

What pip installs

• import echovalidum: cells, Memory64, Arena and SparseScaleMemory, the φ operator algebra, IFC, the loop forms, the Z3 + PQC verification pipeline, QIF, and the discovery-catalog engine.
• The ct-echo console script.
• The soilith_* modules the 22 departments ship under, including the .sol interpreter and bytecode VM.
• On Windows with Python 3.12, the compiled Rust hot path. Elsewhere pip builds it when a Rust toolchain is present and otherwise uses the parity-tested Python fallbacks.

Sections marked Research build describe Σoilith tools that are not part of the package.

60-second tour

import echovalidum as ev
import numpy as np

# 1. Empirical iteration-count non-interference
#    (Sabelfeld-Sands channel 1: loop bound).
#    The operator-range loop visits exactly 41 values regardless
#    of HIGH inputs — count_a == count_b is the NI witness.
report = ev.iteration_count_ni_check(
    ev.loops.factory_operator_range(0, 40),
    high_inputs={"secret": (
        ev.Cell(value=np.array([1.0]),  trust=1.0, phase=0.0),
        ev.Cell(value=np.array([99.0]), trust=1.0, phase=0.0),
    )},
    low_inputs={},
    form=ev.LoopForm.OPERATOR_RANGE,
    name="audit_all_phi",
)
assert report.noninterfering
assert report.count_a == report.count_b == 41

# 2. Z3 + PQC: discharge the SS loop-bound channel as UNSAT.
proof = ev.verify_loop_bound_ni(high_drives_bound=False, low_n_writes=41)
assert proof.verified
assert proof.judgment == "ss_channel_1_loop_bound"

attestation = ev.sign_with_pqc(proof)
# attestation["signature"], attestation["signer_id"], etc.

Navigation (five pillars)

Research build, not in the PyPI package. echovalidum.navigation and the pillar APIs in this section belong to the Σoilith research tree.

Echovalidum is not "bigger memory." Sparse lattice capacity is an implementation detail behind kernel(precision). The product is echovalidum.navigation — five first-class pillars, each backed by typed primitives over Cell(value, trust, phase) and each returning a signable NavigationReceipt.

Pillar 1 — Time navigation

echo_write, echo_recall, EchoStack, echo_transaction, phase_inspect, phase_spawn, spine_attractor, angular_lift.

Pillar 2 — Topological control flow

BraidWord, EchoSite, transport, crystallize, sparse_walk, z2_gauge_evolve, z2_plaquette, cayley_qec_validate, variational_graph, quantum_export.

Pillar 3 — Self-modifying semantics

LawRegistry, LawSpec, discover_law, falsify_law.

Pillar 4 — Fidelity-aware execution

Kernel, select_kernel, precision(), standard(), consume() (SALG slice policies), residual_io (theorem-gated IO).

Pillar 5 — Living theorems

@law, verify_law, assert_law_holds, meet_with_receipt, join_with_receipt, TrustRef, trust_gradient.

import echovalidum as ev
import numpy as np

cell = ev.Cell(value=np.linspace(-1.0, 1.0, 168), trust=1.0)

# Pillar 4 — pick a kernel and declare consume slice.
with ev.precision(lattice_k=168, rank=210109), ev.consume("audited_six"):

    # Pillar 1 — atomic phase-reversible block with rollback on failure.
    with ev.echo_transaction(cell) as txn:
        twisted, _ = ev.braid(2, 23, 22).apply(txn.cell)    # Pillar 2
        txn.cell = twisted
    assert txn.committed and txn.receipt.residual < 1e-14

    # Pillar 2 — full problem-class engines as navigation primitives.
    walk = ev.sparse_walk(k=12, steps=32)
    gauge = ev.z2_gauge_evolve(k=3)
    qec   = ev.cayley_qec_validate(k=8, n_syndromes=16)
    assert walk.ok and gauge.ok and qec.ok

    # Pillar 2 — export to runnable circuits.
    ev.quantum_export(name="walk_k12", k=12, steps=32, output_dir="out/")

    # Pillar 5 — lattice meet with trust-residual receipt + proof-carrying ref.
    a = ev.Cell(value=np.array([1.0, 2.0]), trust=0.99)
    b = ev.Cell(value=np.array([2.0, 1.0]), trust=0.97)
    meet, _ = ev.meet_with_receipt(a, b)
    ref = ev.TrustRef.attest(meet, law="gem_phi22_bind_triple_echo")
    ref.dereference()  # raises TrustError if law fails

# Pillar 3 — runtime ingest + adversarial fuzzer.
reg = ev.navigation.default_registry()
def probe(i): return {"residual": 1e-16, "trust": 1.0}
ev.falsify_law("user_session_law", probe, trials=256, registry=reg)

# Every receipt is signable via the existing Z3 + PQC pipeline.
attestation = ev.sign_with_pqc(txn.receipt.to_signable())

Integrated program (all five pillars)

from echovalidum import run_integrated_program, NavigationSession

# One-shot: mirrors examples/echovalidum_pillars.sol with T4 receipts
result = run_integrated_program()
assert result.ok
attestation = result.signable_bundle()  # sign each receipt via sign_with_pqc

# Or drive showcase modes individually:
session = NavigationSession()
session.invoke("echo_recall")
session.invoke("sparse_walk", k=10, steps=16)

CLI probes still work via python -m echovalidum.navigation_runtime --go-live; by default they route through echovalidum.navigation.bridge (product T4 path).

The bundled scientific manifest (echovalidum/data/scientific_manifest.json) hydrates the default LawRegistry automatically. Override with ECHOVALIDUM_SCIENTIFIC_MANIFEST=/path/to/manifest.json.

What's inside

• Trust-graded refinement types. Every cell carries (value, trust, phase) on a bounded lattice; ψ{trust ≥ τ} predicates compose with meet / join and survive cross-process gossip.
• Six basic loop forms with declared termination bounds. Operator range, Cayley ball over (ℤ/2)ᵏ, mem64 pages, fixpoint widen, DAG replay, ESS resample. Each carries a proven (or, for one form, explicitly empirical) bound.
• Cayley-disjoint borrow checking on (ℤ/2)ᵏ for k up to 30, plus a hierarchical 64-bit virtual hierarchy with CHERI-flavored capabilities for larger address spaces.
• Sabelfeld–Sands four-channel non-interference. Loop bound, outer schedule, touch pattern, and data-dependent convergence are each encoded as Z3 / QF_BV obligations. UNSAT on the negation proves termination-sensitive NI; SAT yields a concrete (hₐ, h_b) counterexample. Every result is signed through a post-quantum SignedCertificationResult pipeline.
• Discovery-catalog engine. scan_arena and build_manifest auto-index machine-found laws and judgments out of any Arena you populate — including empirical qif/<program> leakage rows (Zone 155) and z3verify/qif_leak_bounded/<name> certificates (Zone 151) next to Cayley, SS-channel, and loop-IFC slots. The reference catalog the author maintains internally (1,608 indexed entries spanning the 22 research-department implementations) is not redistributed with the package — it is the output of the author's own discovery runs over a proprietary starting arena, kept as internal research evidence. Downstream users run the engine on their own arenas to build their own catalogs. Licensed extracts from the reference catalog are available under a separate commercial agreement — contact hello@echovalidum.com.
• Adoption-contract DSL. A small embedded .sol surface declares which predicates external callers must honour (fn name(report) : ψ{trust ≥ 1.0}: yield report end); everything load-bearing is still plain Python.

Public API at a glance

echovalidum
├── memory      — Cell, Arena, SparseScaleMemory, Memory64, Capability
├── phi         — PHI dict of operators (φ₀..φ₆₀)
├── ifc         — Label, LabeledStore, noninterference_check, declassify
├── loops       — LoopForm, SSChannel, IFCVerdict, LoopNIReport,
│                 iteration_count_ni_check, discharge_loop_form_ni
├── verify      — Z3VerifyResult,
│                 verify_cayley_disjoint, verify_frame_disjoint,
│                 verify_ai_sound, verify_loop_bound_ni,
│                 verify_outer_schedule_ni, verify_touch_pattern_ni,
│                 verify_iteration_bound, sign_with_pqc
└── catalog     — scan_arena, build_manifest

Top-level shortcuts (ev.Cell, ev.verify_cayley_disjoint, etc.) cover the most common entry points; see echovalidum.__all__ for the full list.

The 22 research departments

Echovalidum is not a library of techniques — it is a single substrate (lattice cells × Cayley topology over a finite group × trust grading) that lets twenty-two established programming-language and verification research programs run as readings of the same geometry and evidence rather than as twenty-two orthogonal annotation layers. The table below is the operational summary: what each department contributes to the literature, which shipped module hosts it, what is actually shipped to PyPI, and the epistemology label (proven / machine-checked / mechanizable / empirical) that the package itself reports for that department.

#	Research department	Shipped under	Soundness	What Echovalidum adds to the field
1	Separation logic (Reynolds 2002)	soilith_separation.py + ev.verify_frame_disjoint	machine-checked (Z3)	Footprints become subsets of a group; the frame rule is checked over Cayley-reachable closure.
2	Linear & affine types (Wadler; Tov–Pucella)	soilith_linear.py	empirical	Consume / move discipline runs on arena-backed cells with trust grades.
3	Capabilities (CHERI lineage; Watson 2015)	soilith_capability.py + ev.Capability	proven (monotone attenuation)	Capabilities carry min_trust alongside perms; meets on attenuation are lattice operations.
4	Ownership / borrows (Rust lineage; Boyland 2003)	soilith_ownership.py + ev.verify_cayley_disjoint	machine-checked (Z3)	Mutable-borrow exclusion is closed Cayley neighborhood disjointness — strictly refines disjoint-write-set tests.
5	Refinement types (Liquid Haskell; F*)	soilith_refinement_check.py	mechanizable	ψ{trust ≥ τ} predicates compose with meet / join and gate φ-operator outputs by min(τ_in, τ_cat).
6	Session types (Honda et al.)	soilith_session.py	mechanizable	DFAs are built from finite-order operator composition laws, not declared by hand.
7	Algebraic effects (Plotkin & Pretnar)	soilith_effect.py	mechanizable	Effect rows are mined from categorical signatures in the discovered operator algebra.
8	Information-flow control (Goguen–Meseguer 1982; Sabelfeld–Myers 2003)	soilith_ifc.py, soilith_loop_ifc.py + the ev.verify_*_ni family	empirical + machine-checked (loops)	First library to lift IFC from data labels to iteration counts: all four Sabelfeld–Sands covert channels are kernel-checked.
9	Concurrency & race detection (Lamport 1978; Mattern 1989; ThreadSanitizer)	soilith_concurrent.py	proven (vector clocks)	Interference is a join of Cayley footprints, not address equality — strictly refines "disjoint write sets".
10	Regions (Tofte–Talpin 1997)	soilith_region.py	empirical	Nested lifetimes with escape checks; stale handles after free become detectable via trust drop.
11	Gradual typing (Siek & Taha 2006; Findler–Felleisen)	soilith_gradual.py	mechanizable	ψ{trust ≥ τ_0} is itself a gradual type; arrow domain checks flip blame polarity.
12	Behavioural contracts (Findler–Felleisen 2002)	soilith_contract.py	mechanizable	Pre/post on Cell with arrow blame parity flip — standard higher-order contracts, native to the substrate.
13	Probabilistic programming (Gordon et al. 2014; Doucet)	soilith_prob.py	empirical	Catalog trust grades serve as Bernoulli priors; ESS / resample is one of the six declared loop forms with a proven bound.
14	Incremental computation (Naiad, Murray 2013; Adapton)	soilith_incremental.py	empirical	Dirty propagation runs on a catalog-shaped DAG — the discovery graph itself is the dependency graph.
15	Abstract interpretation (Cousot & Cousot 1977)	soilith_abstract.py + ev.verify_ai_sound	empirical + machine-checked	Sign-lattice transfer functions per φ-operator with a hold-out soundness audit that refuses a transfer rather than reporting false confidence.
16	Weak memory, vector clocks, fractional permissions (Lamport; Mattern; Boyland 2003)	soilith_weakmem.py	proven (vector clocks); release-acquire empirical	A Group abstraction (non-abelian dihedral, non-involution cyclic) so the borrow rule extends beyond (ℤ/2)^k.
17	Mechanizable soundness witnesses (Iris / RustBelt; Verus)	soilith_soundness.py	mechanizable + Coq export	Every accepted judgment emits a structured derivation with named rules (FRAME, CAYLEY-DISJOINT, NI, AI-SOUND) plus an export_coq skeleton.
18	Intervals with widening / narrowing (Cousot & Cousot 1977)	soilith_intervals.py	proven (Cousot fixpoint theorem)	A Kleene-fixpoint CFG engine with widening ∇ and narrowing △ that collapses infinite ascending chains in one step.
19	Scale-aware sparse memory (novel; cf. CHERI; WebAssembly linear memory)	soilith_sparse.py + ev.SparseScaleMemory	proven (borrow rule); sampled (global χ)	SparseScaleMemory(k) runs at k up to 30 (≈ 10⁹ virtual cells) with lazy neighbours and BFS-ball local audits in milliseconds.
20	Reproducible benchmark harness (SIGPLAN AE practice)	soilith_bench.py	empirical	Warmup + repeated timing against pinned baselines (bench/baseline.json) so a single python -m soilith_bench re-runs race detection, weak-memory sync, widening convergence, sparse audit, AI hold-out, the directed φ-algebra identity scan, and Memory64 hot-read throughput; comparative Z3-scaling experiments live in bench/comparative.py.
21	SMT-backed machine-checked judgments (Z3 / de Moura–Bjørner; nlsat — Jovanović 2012)	soilith_z3verify.py + ev.verify_* family + ev.sign_with_pqc	machine-checked (Z3 kernel in the loop)	The frame rule, borrow disjointness, AI soundness, and all four Sabelfeld–Sands non-interference channels are encoded as QF_BV / nlsat obligations; UNSAT-on-negation accepts; SAT yields a concrete counter-example; every result is PQC-signed via the AegisOps SMT pipeline.
22	64-bit virtual address space + CHERI-flavoured capabilities (Watson et al. 2015; x86-64 ISA)	soilith_64bit.py + ev.Memory64, ev.Capability	proven (access-control); structural (page-walk)	A 2⁶⁴-address sparse trie with software TLB and CHERI-flavoured Capability (base + length + RWX + monotone attenuation) — same algorithmic shape as a hardware four-level page-table walk.

How to read the soundness column. Each accepted judgment carries one of four labels:

• proven — correct under a published theorem (Lamport / Mattern; Cousot fixpoint; graph-theoretic borrow disjointness).
• machine-checked — Z3 (or compatible SMT solver) in the loop: UNSAT on the negation, SMT-LIB obligation captured on result.smtlib.
• mechanizable — a structured derivation witness with named inference rules plus a Coq-skeleton emitter; the witnesses are ready to feed a proof assistant.
• empirical — calibration + hold-out audit, with unsound predictions blocking high-trust persistence.

The package itself reports the label on each accepted judgment so downstream tooling can route different epistemology classes to different consumers (e.g. accept machine-checked, log mechanizable, audit empirical).

What is not on this list. Hardware weak memory (TSO / ARM relaxed), sealed CHERI capabilities, hardware-enforced tag bits, and industrial-scale shootouts against ThreadSanitizer and Astrée are the remaining honest frontier; see the Honest scope section.

Proof witnesses you can hand to Coq

Research build, not in the PyPI package. soilith_witness and its Coq export belong to the Σoilith research tree. The packaged static checker, soilith_refinement_check, reaches the same verdicts without the witness trees.

Every trust gate Σoilith decides — the static refinement checker's accept/refuse verdicts, and at runtime let refinements, function return refinements, when guards and when fidelity branches — records a derivation tree with named inference rules, refusals included. The tree exports to a single self-contained Coq file:

python soilith_witness.py program.sol --run --emit-coq witness.v
python soilith_witness.py program.sol --emit-coq witness.v   # static

The export targets QArith, not Reals: every number a gate compares is a concrete rational, so each side condition is closed by kernel computation (Qle_bool … = true by reflexivity) rather than by a tactic. It needs no micromega and loads in a browser Coq. What the kernel checks:

Leaves	cross-checked against generated Env/Obs tables — a mis-transcribed literal does not typecheck
Rule applications	well-formed per the calculus
Side conditions	φ min-propagation and every gate/branch comparison, tolerances included
Metatheorems	each verdict family is exclusive and exhaustive — a verdict is a total function of the recorded facts

Tampering is rejected, not merely undetected: a leaf claiming a trust the table contradicts fails to unify, and a flipped verdict fails with Unable to unify "true" with "Qle_bool ((17 # 20) - 1e-12) 0.3".

What this does not claim. The Env/Obs tables are generated, not verified; each T_Phi step trusts that its depth literal is what Interpreter._depth_trust(k) really returns; and the calculus is not mechanically tied to the interpreter's execution semantics. Those three assumptions are stated in the header of every file it emits.

Trust is observable — refinements and function-return refinements gate on it — and since Zone 161 φ propagates trust: the runtime stamps min(trusts of every Cell-valued argument, depth_trust(k)), so a low-trust value stays low through any operator chain and a binary φ is only as trustworthy as its weakest input. That includes ψs passed by keyword — the stdlib does this for φ₅₅ — while numeric knobs (n, seed, factor, …) are never Cells and contribute nothing. Three invariants back this up, all regression-tested:

• the law-driven rewriter preserves trust exactly, not just value. A rewrite caps the payload at the min of the removed operators' depth trusts — precisely what the chain would have computed — so an optimisation can never change whether a gate passes.
• the static checker's φ rule is the runtime rule: min over every positional ψ argument's bound, the catalog floor, and the depth trust. A whole-operator-set sweep (71 operators × 3 input trusts) asserts the static bound equals the runtime trust exactly whenever the catalog doesn't bind.
• both engines agree: the tree-walk interpreter and the bytecode VM share one phi_trust implementation and record identical witness logs.

Both execution engines — the tree-walking interpreter and the bytecode VM — record identical witness logs, so the evidence is a property of the program rather than of how it was run.

Proof-carrying self-optimization

Research build, not in the PyPI package. soilith-selfopt, the ouroboros checker, and the generation tooling in this section and its subsections belong to the Σoilith research tree.

soilith-selfopt turns the existing law-driven rewrite into a fail-closed compiler protocol:

soilith-selfopt program.sol --lawbook lawbook.arena
soilith-selfopt program.sol --lawbook lawbook.arena --apply

The first command emits a separately named optimized .solc; --apply atomically installs the proven result as the source's normal bytecode cache. The auditable .sol source is never overwritten. Before installation the optimizer binds the source and lawbook hashes, records the exact persisted law behind every replacement, and runs the original and optimized program through both the tree interpreter and VM.

Engine parity is bit-exact. Across a rewrite, trust, phase, printed output, echo topology, and gate witnesses are exact; numerical value is checked with the discovery engine's relative-L2 metric against the declared 1 - trust-threshold budget. A generated Coq file re-decides each law's admission, every concrete trust equality, non-value observable equality, and the measured numerical bound. Coq is required by default. The kernel runner prefers a caller-supplied or local coqc; otherwise it uses the digest-pinned coqorg/coq:8.20.1 image already cached by Docker. The container runs with no network, no host mount, no Linux capabilities, and proof text supplied over stdin. Prepare that fallback once with:

docker pull coqorg/coq:8.20.1

Receipts state the backend, Coq version, immutable image digest, return code, and output hashes. If neither kernel is available, the pinned image is absent, or Coq rejects the file, no executable artifact is installed. The explicit development override can emit an artifact, but labels its receipt UNCHECKED rather than CERTIFIED.

Separated ouroboros checker

Coq is only the final kernel. The parser, rewriter, two execution engines, and observable comparisons previously still ran inside the process proposing the optimized artifact. A compromised producer could therefore try to forge a self-consistent transcript before asking Coq to check the generated claims.

soilith-selfopt now requires a second, independently built replay checker before it emits CERTIFIED. Build it explicitly:

soilith-checker-build
# equivalent: python -m soilith_replay_checker

The producer sends source bytes, lawbook bytes, candidate bytecode, generated Coq proof, and its claimed transcript over stdin. The checker container:

1. independently parses the source and reloads the lawbook;
2. reruns the rewrite and both language engines;
3. regenerates the optimized artifact and Coq proof;
4. compiles that proof with its local Coq 8.20.1 kernel; and
5. requires byte-identical artifacts and proofs plus identical rewrite traces, execution transcripts, and host checks.

No host directory is mounted. The container is read-only, offline, capability-free, and writes only to an ephemeral /tmp. The configured tag is resolved once and execution uses the immutable image ID. Its response is bound to a nonce and records the image ID, entrypoint hash, full soilith_*.py verifier-bundle hash, request/response hashes, replay hashes, and kernel version. A mismatch or missing image refuses installation.

This is process and build separation, not hardware remote attestation: a host administrator controlling Docker remains inside the threat boundary. Pin SOILITH_CHECKER_IMAGE_ID in CI when a release must accept exactly one pre-approved checker build.

Term-proposal generations

The checker now has two deliberately distinct generations. The original echovalidum/soilith-selfopt-checker:1 retains the byte-replay protocol. soilith-checker-build builds :2 and refuses to do so unless :1 is present; the new image records the immutable parent image ID and parent bundle hash without moving or rebuilding the parent tag. Once a generation tag exists, the builder is idempotent only for identical inputs and refuses to overwrite it after any bundle change. Set a fresh SOILITH_CHECKER_BUILD_IMAGE tag (and the prior tag as SOILITH_CHECKER_PARENT_IMAGE) for the next generation. Current byte-replay and term-proposal verification both route through :2; :1 is retained as the immutable bootstrap ancestor, not used to judge v4 term-aware bytecode it predates.

Generation 2 accepts a Σoilith term pass plus a proposed canonical AST. The pass receives the target AST in input and must leave its result in proposal. Inside the pinned, offline checker it:

1. decodes the canonical AST independently;
2. runs the pass through the tree interpreter and bytecode VM;
3. requires identical proposal terms, witness logs, and canonical AST bytes;
4. runs the source and proposal through both engines and requires exact observable and root-trust equivalence; and
5. regenerates and compiles the Coq term/match certificate.

The receipt preserves three identities rather than conflating them: the full soilith_*.py byte bundle, a meaning-bearing semantic-module manifest, and a generation edge binding parent checker, producer bundle, pass hash, source AST hash, and proposal AST hash. The pinned generation-2 manifest is docker/selfopt-checker/generation-2.json.

This is the program-scope bridge toward compiler evolution, not yet a claim of whole-stack self-hosting. Generation 1 predates the semantic proposal protocol, so generation 2 is explicitly marked as its bootstrap generation: the parent edge proves ancestry, not that generation 1 understood and proved generation 2's new semantics. Future generations can now be proposed to a checker that already understands the protocol.

Five-step generation promotion

soilith_generation.py turns the long-range self-replacement roadmap into one fail-closed acceptance theorem. It does not award progress for nearby capabilities: all five predicates must hold in the same candidate release.

1. Self-representation. Canonical, hashed representations must cover modules, types, effects, trust rules, rewrite laws, and the build graph. The decoder must be closed, its round trip byte-identical, and both engines must reify the same model.
2. Self-hosting. The parser, type/trust checker, optimizer, and bytecode compiler must be Σoilith components. Stage 0 must compile stage 1, stage 1 must compile stage 2, and the stage-1/stage-2 artifacts must be byte-identical under the pinned toolchain.
3. Compiler rewrites. Parser normalization, AST transformation, trust propagation, dead-code removal, bytecode selection, runtime specialization, and fixture/harness generation must each carry semantic equivalence, trust-exactness, cross-engine agreement, external replay, and a checked Coq artifact.
4. Stack transformation. One acyclic, hash-bound migration graph must cover language programs, compiler/VM, applications, Rust adapters, ctweapon laws, ctrust harnesses, CI, ledger theorems, and deployment definitions. Every component needs verified evidence and the candidate must bind a valid signed release-dominance ledger theorem.
5. Generational replacement. The immutable checker image and bundle must be generation N, the replay target must be exactly N+1, and the certifier identity must equal N and differ from N+1. Coq, both engines, ct measurement, and the signed evidence chain are mandatory. The proposer must also sign the exact parent, candidate transport, supplied evidence, and checker-derived component/change-class set. Generation N—not N+1—owns the capability policy.

soilith-generation input.json --out promotion.json derives and, by default, seals that theorem with ML-DSA-87. Verification independently re-derives the entire theorem before checking the signature. A SHA-256 fallback remains useful for development integrity but is explicitly rejected by production promotion policy.

The current maturity is intentionally recorded without promotion language:

Step	Durable capital now	Missing acceptance condition	Status
1	Source-derived per-module/per-domain identity, build-graph closure, closed decoder, 34-program round trip, and dual-engine reification	Effect and rewrite-law domains are still structural; soilith_effect has no production consumer	STRUCTURAL + REIFIED / EFFECT SEMANTICS OPEN
2	Python parser, trust checker, optimizer, compiler, and VM are a working stage 0	No Σoilith implementation of all four compiler components; no stage-1/stage-2 artifact fixed point	NOT SATISFIED
3	A program-scoped term pass is replayed by both engines and Coq in a pinned checker	The seven compiler-pass classes are not yet represented and proved	PARTIAL / REFUSED
4	ctweapon/ctrust/ctproject components and a signed release-dominance ledger theorem exist	No single proposed, topologically replayed migration spans all nine component classes	PARTIAL / REFUSED
5	Pinned generation N ingests N+1 source, derives its identities, computes structural/evidence non-regression, and reproduces language behaviour. Generation 7 adds checker-side Rust closure replay; generation 10 pins native ML-DSA-44/65/87 policy; generations 11→13 add exact target identities and cross-target refusal. Generation 14 adds parent-pinned capabilities, ML-DSA-87 proposer identity, exact change-set authorization, and checker-owned counterexamples.	Generations 7, 10, and 14 are protocol bootstraps: each new predicate can first govern its child edge. Linux/x86_64 remains an EXPECTED ctrust target, so noisy or inconclusive closure remains refused.	B1/B3 ACTIVE · B2 NATIVE MECHANISM PINNED · B4 IMPLEMENTED / CHILD EDGE OWED · B5 MECHANISM PINNED / TARGET VALIDATION OPEN

The pinned promotion checker is echovalidum/soilith-selfopt-checker:6 (sha256:3c1512c9f888f9204d57acf50d3c637e86472cd8baee05531bec4231dd508b0d). Generation 2 could not retroactively verify a protocol it predates, so generation 3 is explicitly a protocol bootstrap—not a self-hosting or complete promotion claim. It pins the five-step acceptance vocabulary and proves the separated transport. A Windows CLI hardening change then produced generation 4 as a new child instead of overwriting generation 3, exercising the immutability rule on this sprint itself. Generation 5 is the derive/diff/measure bootstrap: it binds its 34-program corpus and refused its first real candidate on a tree/VM deployment-layout divergence. The corrected shallow-container runtime was replayed by generation 5 and pinned as generation 6. That edge establishes the B1/B3 slice. Generation 7 pins the B2 mechanism: Rust 1.94.0, the exact ctrust replay engine, safe deterministic Cargo-workspace transport, signed invocation parameters, and checker-side before/after rebuild and measurement. Generation 6 predates that predicate, so generation 7 is explicitly a bootstrap; the first B2-grounded edge can only begin after it. Generation 8 added native ML-DSA-44/65/87 and correctly remained immutable when validation exposed a liboqs 0.13.0 / wrapper 0.12.0 mismatch. Generation 9 is its child, pins matched liboqs and wrapper 0.14.0 source revisions into the ctrust-engine identity, and has verified all three receipt families in both directions with the Windows project venv. Its audit then exposed a policy fail-open: require_pqc meant any verified non-SHA-256 algorithm. Generation 10 is the immutable child that requires pure ML-DSA-44/65/87, matching NIST category, native liboqs metadata, and one algorithm/public-key chain across the before, after, and aggregate receipts. This closes native signature availability, not machine-dependent timing validation. Generation 11 is the B5 bootstrap: its candidate self-model derives six target classes from source, ctrust signs an exact runner identity, and checker-side Rust replay refuses to transfer timing evidence between different runner identities. Its pinned validation caught that Linux CPU identity selected the numeric processor: 0 index; generation 12 is the immutable child that prioritizes model name and refuses numeric indices. Generation 12's follow-on audit found that the standalone ctclose verifier trusted its aggregate signature without independently verifying both nested ctrust target profiles; generation 13 closes that boundary and binds every CI item timer to the signed profile. Generation 14 introduces governed proposal authority. Its self-model derives the literal capability policy with ast, while the pinned parent verifies an ML-DSA-87 proposer signature over the exact generation subject and actual module/change classes N measured. A candidate cannot authorize itself by editing its policy: that edit is classified as authority_policy and judged against N's still-pinned grants. Unauthorized candidates are not executed, and checker-owned refusal counterexamples are folded into promotion evidence. The current transport classifies soilith_*.py; cross-language capability scope awaits the cross-language candidate bundle. Linux/x86_64 remains an EXPECTED target and inconclusive measurements still fail closed. The immutable records are generation-3.json and generation-4.json, generation-5.json, and generation-6.json, and generation-7.json, generation-8.json, and generation-9.json, and generation-10.json, and generation-11.json, and generation-12.json, and generation-13.json, and generation-14.json.

The receipt seals the input hashes, optimized bytecode hash, law evidence, four execution transcripts, Coq result, separated replay result, and installation state. This supports future products such as proof-carrying deployment specialization, hardware-specific optimizer profiles, independently replayable compiler receipts, and a cross-engine regression oracle. It does not recast an empirically discovered numerical law as a universal formal theorem; the receipt preserves that evidence boundary explicitly.

Rust measure → close → prove

Research build, not in the PyPI package. ctrust-close and applications.ctweapon belong to the Σoilith research tree.

ctrust-close closes the missing Rust half of the remediation loop:

ctrust-close path/to/crate item::verify
ctrust-close path/to/crate item::verify --write

The protocol first requires a signed LEAKY ctrust measurement over a linked workspace artifact. Σoilith then applies one exact registered Rust law in a private copy, checks the law with Coq, confirms the rewrite is a fixpoint, rebuilds the workspace, and requires a fresh signed CONSTANT_TIME measurement over a different linked-artifact hash. Only the aggregate receipt may say CLOSED; --write changes the original source atomically only after that result.

The initial law table is deliberately narrow: equal-length byte-slice equality and all-zero byte predicates whose secret-dependent early return can be replaced by a full-length boolean accumulator. An unfamiliar body is refused, not approximately rewritten. Coq proves source-level boolean equivalence; ctrust's remeasurement is the separate evidence that the compiler emitted a flat artifact on the declared runner.

For generational admission, each ctrust item receipt now signs a echovalidum.ctrust.reproduce.v1 block containing the exact item, fixture, features, adapter, lock policy, timer, sample, and voting inputs. A deterministic regular-file-only workspace archive supplies the bytes. The parent checker rejects traversal, links, oversized archives, unsupported-target overrides, source/fixture/item drift, signer changes, rewrite drift, cross-target inference, and any before/after verdict it cannot reproduce. Each signed ctrust.target-profile.v1 separates a portable target class from an exact runner digest; before, after, and replay must share the latter. Rebuilt artifact hashes are recorded rather than assumed portable: this remains machine-dependent evidence.

The shared compliance ledger now derives and signs release theorems:

python -m applications.ctweapon --ledger-theorem-since 42

It proves—or returns concrete counterexamples for—no component regression since the boundary, machine-code evidence behind every current clean claim, and evidence dominance over the previous release. Two permanent targets, self:soilith-signing and self:soilith-verification, must each carry current MACHINE_CODE_CLOSURE evidence. Until native implementations are actually closed and recorded for those identities, that self-gate remains visibly false; the existing Python/liboqs surface is not mislabeled as Rust machine-code proof.

Honest scope

The four-channel discharge proves NI for the structural model of each loop form — what the iteration count is a function of. It does not lift arbitrary user Python programs into Z3; that would require a separate symbolic-execution layer Echovalidum does not claim to provide. For programs whose loop parameters are LOW literals, the discharge is end-to-end machine-checked; for programs whose parameters are computed at runtime, the discharge runs on the live runtime object that the loop primitive received, and the empirical 2-trace check covers the remainder.

Channel 4 (data-dependent convergence, e.g. particle filters) is fundamentally HIGH-dependent in the iteration count. Echovalidum discharges the bound in that case (c ≤ max_iter) — the Sabelfeld–Sands declassification budget — rather than claiming non-interference where none exists.

Status

Item	Value
Version	0.3.0 (β)
Test suite	499 passing tests
Research departments	22 mainstream PL programs running on a single substrate (see table below)
Discovery-catalog engine	scan_arena, build_manifest ship; the author's reference catalog (1,608 entries) is not redistributed
Median Z3 discharge	< 5 ms per judgment (QF_BV)
Hard dependency	numpy >= 1.24, scipy >= 1.10
Optional dependency	z3-solver >= 4.12
License	PolyForm Noncommercial 1.0.0 + paid commercial

Citation

@software{echovalidum_2026,
  title   = {Echovalidum: a Python library for lattice-based memory
             with kernel-checked Sabelfeld--Sands four-channel
             non-interference},
  author  = {Koch, Brisen},
  year    = {2026},
  version = {0.3.0},
  license = {PolyForm-Noncommercial-1.0.0},
  url     = {https://echovalidum.com/}
}

A CITATION.cff is also shipped in the repository for the GitHub citation widget.

References

• Sabelfeld, A. and Sands, D. (2000). Probabilistic Noninterference for Multi-threaded Programs. Proc. CSFW.

Contact

Commercial licensing, research collaboration, enterprise support, trademark / naming clearances, and coordinated security disclosures: hello@echovalidum.com.

License

Echovalidum is source-available under the PolyForm Noncommercial License 1.0.0.

You may use, modify, and redistribute Echovalidum at no cost for any noncommercial purpose:

• academic research and teaching,
• personal projects, hobby work, study, experimentation,
• evaluation and internal R&D by educational institutions, public research organizations, governments, and other noncommercial organizations as defined in the PolyForm license text.

Any commercial use requires a separate paid commercial license from the copyright holder. "Commercial use" includes — without limitation — deployment in a for-profit product or service, redistribution inside a commercial offering, paid consulting that depends on Echovalidum, and use by a for-profit company's engineering or R&D organization with anticipated commercial application. Contact hello@echovalidum.com.

The names Echovalidum, Σoilith / Soilith, AegisOps, and the tool names ct-echo, borrowsmith, provenance, particle-bound, and scale-heap are trademarks of Brisen Koch. PolyForm Noncommercial is a copyright and patent license only — it does not grant any right to use these marks in derivative product names, branding, or marketing. See NOTICE.

Enterprise tier — hosted attestation registry, PQC key custody, the full AegisOps SMT certification pipeline, integrations, SLA — is sold separately under the proprietary AegisOps stack.