echovalidum 0.1.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.

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.1.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.

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 (Zone 154).
#    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.
• Self-growing discovery catalog. A persistent lawbook auto-indexes machine-found laws and judgments by zone and kind; the current snapshot contains 1608 entries across zones 116–154.
• 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.

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.1.0 (β)
Test suite	330 passing tests
Spec zones	154 numbered zones
Discovery catalog	1608 indexed entries (zones 116–154)
Median Z3 discharge	< 5 ms per judgment (QF_BV)
Hard dependency	numpy >= 1.24
Optional dependency	z3-solver >= 4.12
License	Proprietary

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.1.0},
  url     = {https://www.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.

License

Proprietary. Public extraction and citation of the architecture is fine; redistribution of the implementation is not yet open. Contact via echovalidum.com for inquiries.