Metadata-Version: 2.4
Name: echovalidum
Version: 0.2.0
Summary: 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.
Author: Brisen Koch
License-Expression: LicenseRef-PolyForm-Noncommercial-1.0.0
Project-URL: Homepage, https://echovalidum.com/
Keywords: programming-language,lattice,memory-model,non-interference,information-flow-control,separation-logic,cayley-graph,abstract-interpretation,smt,z3,pqc,attestation
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Compilers
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Classifier: Topic :: Security
Classifier: Operating System :: OS Independent
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: NOTICE
Requires-Dist: numpy>=1.24
Requires-Dist: scipy>=1.10
Provides-Extra: verify
Requires-Dist: z3-solver>=4.12; extra == "verify"
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == "dev"
Dynamic: license-file

# Echovalidum

*The echo, validated.*

[![PyPI](https://img.shields.io/pypi/v/echovalidum.svg)](https://pypi.org/project/echovalidum/)
[![Python](https://img.shields.io/pypi/pyversions/echovalidum.svg)](https://pypi.org/project/echovalidum/)
[![Homepage](https://img.shields.io/badge/web-echovalidum.com-0f6160.svg)](https://www.echovalidum.com)

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

```bash
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

```python
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
  <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

```text
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.2.0 (β)                          |
| Test suite                | 330 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

```bibtex
@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.2.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**](./LICENSE).

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`](./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.
