echovalidum 0.3.0

The echo, validated — a Python library for lattice-based memory with kernel-checked attestations for the Sabelfeld-Sands four-channel iteration-count NI model. Source-available under PolyForm Noncommercial; paid commercial license available.

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.

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.

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 only hard dependency is numpy >= 1.24. The Z3 backend is optional — empirical 2-trace NI checks work without it.

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.

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. 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 [e-mail].
• 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	Pinned in-process baselines so a single python -m soilith_bench re-runs race detection, memory throughput, sparse audit, Z3 scaling, and AI hold-out.
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.

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	389 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: [e-mail].

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 [e-mail].

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.