Metadata-Version: 2.4
Name: echovalidum
Version: 0.1.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.
Author: Brisen Koch
License-Expression: LicenseRef-Proprietary
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
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"

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

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

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

## 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

```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.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](https://www.echovalidum.com) for inquiries.
