Metadata-Version: 2.4
Name: echovalidum
Version: 0.3.2
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: Programming Language :: Rust
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?cb=031)](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.

## Rust hot path, Python analysis path

The [`echovalidum` crate](https://crates.io/crates/echovalidum) 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.

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

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

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

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

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

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

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

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

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

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

```bash
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`](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`](docker/selfopt-checker/generation-3.json) and
[`generation-4.json`](docker/selfopt-checker/generation-4.json),
[`generation-5.json`](docker/selfopt-checker/generation-5.json), and
[`generation-6.json`](docker/selfopt-checker/generation-6.json), and
[`generation-7.json`](docker/selfopt-checker/generation-7.json),
[`generation-8.json`](docker/selfopt-checker/generation-8.json), and
[`generation-9.json`](docker/selfopt-checker/generation-9.json), and
[`generation-10.json`](docker/selfopt-checker/generation-10.json), and
[`generation-11.json`](docker/selfopt-checker/generation-11.json), and
[`generation-12.json`](docker/selfopt-checker/generation-12.json), and
 [`generation-13.json`](docker/selfopt-checker/generation-13.json), and
 [`generation-14.json`](docker/selfopt-checker/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:

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

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

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