Metadata-Version: 2.4
Name: darwin-cre
Version: 0.2.0
Summary: Darwin — universal black-box crypto extraction from binaries: compositional instruction-granular synthesis with machine-checked equivalence proofs (forall 2^32 / 2^64).
License: MIT with the condition that commercial use mentions the authors Ashot G. and Trisha M. (see LICENSE)
Requires-Python: >=3.9
Keywords: reverse-engineering,security,cryptography,synthesis,smt,proof
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Rust
Classifier: Topic :: Security
Description-Content-Type: text/markdown

<div align="center">

# 🧬 Darwin

### Universal black-box crypto extraction from binaries

**Compositional, instruction-granular program synthesis with machine-checked equivalence proofs.**

[![License: MIT + attribution](https://img.shields.io/badge/License-MIT%20%2B%20attribution-blue.svg?style=flat-square)](LICENSE)
[![Rust](https://img.shields.io/badge/Rust-stable%20·%20edition%202021-000000?style=flat-square&logo=rust)](#build-from-source)
[![Core deps](https://img.shields.io/badge/core%20crates-zero-success?style=flat-square)](#at-a-glance)
[![Python](https://img.shields.io/badge/Python-%E2%89%A5%203.9%20·%20abi3-3776AB?style=flat-square&logo=python&logoColor=white)](docs/PYTHON-API.md)
[![Platform](https://img.shields.io/badge/platform-Windows%20x64%20·%20Linux%20(typechecked)-0078D6?style=flat-square)](#platform--toolchain)
[![Proofs](https://img.shields.io/badge/proofs-Z3%20%2B%20cvc5%20%2B%20Alethe-6E4AFF?style=flat-square)](#the-proof-stack)
[![ISAs](https://img.shields.io/badge/ISA-x86--64%20·%20x86--32%20·%20AArch64-informational?style=flat-square)](#platform--toolchain)

<samp>emulate → synthesize → compose → **prove** → extract · verify · decrypt</samp>

</div>

---

Point Darwin at compiled code — a raw blob or a PE function. It emulates the code,
observes per-instruction input/output behavior, synthesizes the exact semantics of
every instruction as a bitvector expression, composes them symbolically, and
**proves** the reconstruction equivalent — for **ALL 2^B inputs**, not sampled runs.

Lookup tables (S-boxes) are extracted byte-exact. Data-dependent branches are
reconstructed as `ite(...)`. Ciphers are fingerprinted against a structural database
(TEA family, AES S-box, magic constants). A key-material report answers the one
question that matters in practice: *which bytes feed this code?*

**D11 closes the practical loop.** The report's candidates now carry an **origin**
(`embedded-static` — the bytes are in the artifact, or `supplied-symbolic` — the
caller supplied them), the **verify oracle** measures a candidate into a
`VERIFIED` / `REJECTED` verdict from real emulation runs, and the
**held-out-gated decrypt runner** turns a verified key plus the data into
plaintext — the plaintext renders only when both gate legs are green. A
**frozen-instance export** and an **attack bridge** (SAT over the exported
instance, with the oracle — never the solver — gating the key claim) complete the
rung ladder.

> [!IMPORTANT]
> **Positioning.** LLM-based lifters report Pass@1 ≈ 74% on sampled tests.
> Darwin's output carries a proof **∀2^32 / ∀2^64** — or an honest `Unknown`
> / typed refusal. There is no third option, and there is no "looks right".

---

## Table of contents

- [The honest-verdict doctrine](#the-honest-verdict-doctrine)
- [What Darwin is not](#what-darwin-is-not)
- [At a glance](#at-a-glance)
- [Quickstart](#quickstart)
- [How it works](#how-it-works)
  - [The lift pipeline](#the-lift-pipeline)
  - [The expression DSL](#the-expression-dsl)
  - [Memory models](#memory-models)
  - [Loops](#loops)
  - [The proof stack](#the-proof-stack)
  - [The claim vocabulary](#the-claim-vocabulary)
  - [Soundness rules](#soundness-rules)
  - [The key-material report](#the-key-material-report)
  - [The artifact-key pipeline (D11)](#the-artifact-key-pipeline-d11)
- [Honest limits](#honest-limits)
- [Benchmarks](#benchmarks)
- [Documentation](#documentation)
- [License](#license)
- [Authors and credits](#authors-and-credits)

---

## The honest-verdict doctrine

Every lift ends in **exactly one** of three states:

| verdict | meaning |
|---|---|
| 🟢 **`PROVEN`** | machine-checked over **all** inputs |
| 🟡 **`SELF-TEST ONLY`** | sampled conformance — **no** ∀-guarantee, carries a named residual |
| 🔴 **`REFUSED`** | a typed error naming the **exact blocker and its address** |

A **false `PROVEN`** is the one failure class the architecture treats as
unacceptable:

- an unconfirmed solver result is **never** delivered as proof;
- an out-of-scope shape is **refused**, never approximated;
- the verdict surface is **hash-pinned**, so an unintended change cannot pass silently.

### Why this matters

| | LLM / heuristic lifters | **Darwin** |
|---|---|---|
| Guarantee | Pass@1 on sampled tests | ∀2^32 / ∀2^64, machine-checked — or a typed `Unknown` |
| Failure mode | plausible-looking wrong code | typed refusal naming blocker **+ address** |
| S-boxes / tables | approximated or inlined | byte-exact, VA/RVA-anchored, coverage-classified |
| Verification | sampled tests | normalization → Z3 → cvc5 → **external Alethe checker** |
| Key material | brute force / search | inversion of the PROVEN model, witness verified twice — then the emulation oracle measures `VERIFIED` / `REJECTED` (D11) |
| Hostile input | may execute | emulator sandbox only, **never natively** |

---

## What Darwin is not

- **No brute force.** Key material comes from inverting the PROVEN model (an
  EXISTS-claim over the model, the witness verified twice) — never from search.
  The D11 attack bridge's SAT solve is *discovery* — a candidate generator over
  the frozen instance; every claim it produces is gated by the measured verify
  oracle, never by the solver.
- **No native execution.** Hostile binaries are only ever emulated: all execution
  happens inside the emulator sandbox, never on the host.
- **No guarantees dressed as numbers.** Every figure in
  [Benchmarks](#benchmarks) is a *measurement* on this project's fixture corpus —
  stated as a measurement, never as a guarantee.

---

## At a glance

| | |
|---|---|
| **License** | **MIT with a commercial-attribution condition** — commercial use must mention the authors Ashot G. and Trisha M.; see [`LICENSE`](LICENSE). Bundled/vendored third-party components keep their own licenses: [`THIRD_PARTY_NOTICES.md`](THIRD_PARTY_NOTICES.md). |
| **Core dependencies** | **Zero external crates** — hand-rolled FFI to the system libraries. The Python bindings crate owns the workspace's only dependencies. |
| **Toolchain** | Rust (stable, edition 2021) · `z3` + Unicorn libraries · a C toolchain · Python ≥ 3.9 for bindings and the proof-log checker · `cvc5` vendored under `tools/` (optional, run as a subprocess). |
| **Proof stack** | normalization → Z3 (QF_BV, guarded) → cvc5 → external Alethe certificate checker. |
| **ISAs** | x86-64 (primary) · x86-32 (end-to-end) · AArch64 (third architecture). |

### Platform & toolchain

**Windows x64** is the development platform; the code is standard Rust plus a C
toolchain. The tier beyond it is **measured, not promised**:

- the workspace and its full test surface **type-check for Linux** (a local
  cross-target check, green);
- the CI workflow is authored — a targeted subset per push, the full battery
  weekly, under a private-repo budget discipline (the first green CI run lands
  with the first published push);
- the **32-bit x86** mode runs end-to-end (a blind proof cell on a 32-bit loop fixture);
- **AArch64** is the third architecture (a new decoder module, the core form family,
  blind proof cells on a chain and a loop — *no x86 file changed*).

On the x86 side the decoder covers **96.549%** of decode sites on the measured
corpus (zlib1.dll, libgmp, the project's own optimized builds; a linear-sweep
walk, the D10/T12 re-run) — the unsupported mass sits behind
[recorded decisions](#honest-limits).

---

## Quickstart

The Python surface — full reference in [`docs/PYTHON-API.md`](docs/PYTHON-API.md):

```python
import darwin

job = darwin.lift(blob)              # blind black-box lift (no truth needed)
res = job.wait()                     # Job: poll / wait / cancel / progress events

print(res.proof)                     # "PROVEN (lifted_binary)" (blind, default) / "SELF-TEST ONLY"
print(res.expr)                      # recovered formula

res.expr.eval([0xDEADBEEF])          # exact semantics, any input
res.expr.to_c()                      # self-contained C unit, bit-exact with eval

res.tables                           # S-boxes byte-exact WITH offsets / RVAs
res.key_material                     # "which bytes feed this code": sites + labeled key candidates

# PE images: section-mapped, so .rdata tables are found outside the function window
pe  = darwin.load_pe("tests/fixtures/pe_table/fixture.exe")          # committed PE fixture
res = pe.function_at(0x140001000).lift(inputs=[3], width=32).wait()  # RCX = Var3

darwin.lift_many(blobs, workers=4)   # batch: results-or-exception-INSTANCES, ordered
darwin.prove(expr_a, expr_b)         # machine-checked equivalence (3-state Verdict)
```

The D11 artifact-key surface (the same reference documents every contract):

```python
import darwin

pe = open("tests/fixtures/ransom_embed/fixture.exe", "rb").read()

report = darwin.keymat_json(pe, 0x14000101F)
# the v2 report JSON: sites; candidates, each with origin
# ("embedded-static" | "supplied-symbolic"); iv_sites; weakness_flags
# ("static-iv" | "constant-nonce"); mode_hint (discovery-grade)

v = darwin.verify_key(pe, 0x14000101F, 0x140002000, key, pairs)
# {"verdict": "VERIFIED"|"REJECTED", "pair_results": [(i, ok), ...]} —
# the verdict comes from MEASURED emulation runs, never from a guess

d = darwin.decrypt(pe, 0x14000101F, 0x140002000, key, data, heldout)
# {"heldout_ok", "data_len", "plaintext", "notes"} — the plaintext hex
# renders ONLY when the held-out gate is green (measured forward leg AND
# native-inverse leg); otherwise the withheld marker — to_json / summary /
# Debug all withhold, never the computed bytes

x = darwin.xor_recover(c1, c2)       # C1^C2 = P1^P2 under a REUSED keystream
                                     # (the constant-nonce consequence) —
                                     # the XOR of the plaintexts, NOT a plaintext

m = darwin.ecb_repetitions(ct, 16)   # the ECB repetition map:
                                     # [{"block": n, "equal_to": [i, ...]}, ...]
```

### Build from source

The extension module is a Rust cdylib:

```sh
cargo build --release                    # core (zero external crates) + native demo binary
cargo build --release -p darwin-python   # the Python extension
cp target/release/_impl.dll python/darwin/_impl.pyd   # Windows cdylib; same role elsewhere
cd python && python -m pytest tests -q   # Python >= 3.9
```

> [!NOTE]
> The `z3` and Unicorn libraries must be visible to the linker at build time and
> on the loader path at run time. An **abi3 (Python 3.9+)** wheel can be built
> from `python/` with maturin.

### Run the end-to-end demo

A decryptor-class PE function lifted blind, then a truth-mode proof over all
2^32 input tuples, then a batch over mixed blobs:

```sh
PYTHONPATH=python python examples/python/class_decryptor_demo.py
```

### Run the D11 demos

The whole artifact-key pipeline over the committed ransomware-class fixture
(an XTEA-8 encryptor with its 16-byte key embedded in `.rdata`), and the SAT
attack bridge with its oracle-closed loop (with the toolchain's `bin` directory
on `PATH` — the demo binary links the ucrt64 runtime, and the bridge needs
`z3`):

```sh
./target/release/darwin.exe d11          # keymat -> verify -> decrypt, ~41 s, end to end
python tools/attack-bridge/run_demo.py   # export -> CNF -> SAT -> the oracle gates the claim
```

The `d11` demo PASSes only when every recorded expectation holds: the
embedded-static 16-byte candidate at the recorded `.rdata` VA, byte-exact
against the fixture's key; the candidate `VERIFIED` on the known pair; the
held-out gate green on both legs; the released plaintext equal to the recorded
3-block buffer.

---

## How it works

```mermaid
flowchart LR
    IN["Raw blob<br/>or PE function"] --> E
    subgraph PIPE [" "]
      direction LR
      E["① Emulation<br/><sub>Unicorn sandbox<br/>concolic + random</sub>"]
        --> S["② Per-instruction<br/>synthesis<br/><sub>CEGIS sketch search</sub>"]
        --> C["③ Symbolic<br/>composition<br/><sub>ite · loops · memory</sub>"]
        --> P["④ Proof<br/><sub>normalize → Z3 → cvc5</sub>"]
    end
    P --> V{verdict}
    V --> A["🟢 PROVEN"]
    V --> B["🟡 SELF-TEST ONLY"]
    V --> D["🔴 REFUSED<br/><sub>typed, with address</sub>"]
    A --> K
    subgraph D11PIPE ["D11 — the artifact-key rungs"]
      direction LR
      K["⑤ keymat v2<br/><sub>origin classes<br/>IV/nonce · mode hint</sub>"]
        --> O["⑥ verify oracle<br/><sub>measured runs:<br/>VERIFIED / REJECTED</sub>"]
        --> X["⑦ decrypt<br/><sub>held-out gate:<br/>plaintext only on green</sub>"]
    end
    K -.-> N["no-key utilities<br/><sub>keystream-XOR<br/>ECB map</sub>"]
    K -.-> F["frozen-instance export<br/><sub>the DAG-faithful artifact</sub>"]
    F -.-> Z["attack bridge<br/><sub>CNF → SAT →<br/>the oracle gates the claim</sub>"]
```

### The lift pipeline

Four steps, one verdict.

<details open>
<summary><b>① Emulation</b> — observe, never execute natively</summary>
<br>

The code runs under the **Unicorn** engine inside a sandbox — never natively. PE
input is section-mapped, so `.rdata` tables are found outside the function window.
A 15-register x86-64 GPR file is tracked with frozen input-var slots (`Var0..5`)
and 8 stack-argument slots; the calling convention is auto-detected; flags are
tracked **semantics, not decoded fields** (`cmp` yields `CF := Ult(x, y)`, `cmovb`
becomes an `ite`). Each instruction is observed on random and concolic inputs, and
a path-condition collector gathers one symbolic condition per branch leaf.

</details>

<details>
<summary><b>② Per-instruction synthesis</b> — CEGIS over the expression DSL</summary>
<br>

Every instruction column is fit separately by a CEGIS-style sketch search over
the expression DSL (an escalating node-budget ladder) against the emulator oracle.

Table-load addresses come from the **DECODED addressing structure**
(base/index/scale/disp/RIP-relative) — *not* from re-synthesizing the index as an
opaque sketch problem; index masks and range bounds are mined from the code with
per-table dataflow attribution.

When enabled, each column is additionally validated against an *independently
encoded* reference (the decoder's own per-form semantics, not the fitter's oracle)
— `Validated` / `Refuted` / `NotValidated`: a separate confidence layer that
**never upgrades the claim level**.

</details>

<details>
<summary><b>③ Symbolic composition</b> — branches, loops, memory</summary>
<br>

The per-instruction expressions compose into the delivered model: branches merge
as `ite` trees, loops take one of [three lanes](#loops), memory resolves through
the [region engine](#memory-models). The composed candidate is self-tested against
the emulator on sampled inputs **before anything is claimed**.

</details>

<details>
<summary><b>④ Proof</b> — ∀-equivalence plus domain coverage</summary>
<br>

The candidate is proven equivalent — to the caller's truth expression (*prove
mode*) or to the independently encoded `lifted_binary` substrate (*blind mode*,
the default) — by [the proof stack](#the-proof-stack).

A **blind domain-coverage obligation** then closes the ∀-claim over the entire
declared input domain: an SMT query asks whether any input takes no traced path;
each such input is appended to the run set and re-lifted, and a persistent gap
certificates as a **typed residual, never as silence**.

For every run, the emulator's actually-taken branch must agree with the
symbolically synthesized condition on the same input — a disagreement is a typed
*emulator-fidelity residual*. When ≥ 2 distinct row-consistent candidates survive,
one SMT query finds a distinguishing input and feeds it back into the next round.

</details>

#### Inverting for key material

From the proven model, `solve_for_outputs` inverts for key/nonce material: a
conjunctive solve on the PROVEN bundle, every component forward-verified, then an
emulator re-check inside the sandbox; multi-pair confirmation with a
machine-checked injectivity classification (`Unique` / `NonUnique` / `Unknown`).

> The inverse is an **EXISTS-claim over the model** — never worded as a
> key-recovery proof.

The D11 rungs continue from here — [the artifact-key
pipeline](#the-artifact-key-pipeline-d11).

---

### The expression DSL

The delivered model is a small, **closed** bitvector language. Every node is one of:

```
Const · Var · Un(Op1, x) · Bin(Op2, a, b) · Ite(c, t, e) · Sel(table, index)
```

`Sel` is a byte-exact table lookup, fingerprinted and VA/RVA-anchored. Expression
depth is capped (**4096**) with a typed error on every constructor path.

| class | ops | notes |
|---|---|---|
| bitwise / ARX | `Not`, `Neg`, `Xor`, `And`, `Or`, `Add`, `Sub` | the core straight-line class |
| comparisons | `Ult`, `Slt`, `Eqz` | unsigned / signed less-than, equal-zero — flag-semantics building blocks |
| constant shifts | `Rol(k)`, `Shl(k)`, `Shr(k)`, `Sar(k)` | `Sar` = sign-fill arithmetic shift; the sign-extend composition `sar(shl(x,32),32)` is representable |
| variable shifts | `ShlV`, `ShrV`, `RolV`, `SarV` | x86 CL-shift semantics, count masked to B−1 as part of the op; `SarV` is the `sar r/m, cl` form; `ROR(x,c) = RolV(x, B−c)` |
| bit-scan | `Bsf`, `Bsr` | zero-input defined as "no bit found"; x86-UNDEFINED inputs are guarded compositions |
| const multiply | `MulC(c)`, `MulHighC(c)` | multiply by a **mined** constant / its signed high half (the Barrett magic class) — coefficients are never invented |
| GF(2^n) | `GfMul(poly)` | carryless multiply with an optional reduction polynomial (GHASH word anatomy, MixColumns) |

**`Ite`** reconstructs data-dependent branches (a degenerate `ite(c, X, X)`
collapses to `X`).

**`Sel`** coverage is classified `Full` (the mask-bound full extent is read from
the image) or `Sampled` (the discovered window is all there is — **no invented
bytes**), with the coverage bound's source exposed. `Expr.eval` is strict: an
out-of-domain `Sel` raises a typed `TableDomainError`, not a silent default.

<details>
<summary><b>On <code>Op2::Mul</code> (true var×var multiply)</b> — what's in, what's excluded, and why</summary>
<br>

`Op2::Mul` is in the DSL — landed at **D10/T6**: decoder-known multiply forms take
the **form-templated arm** (the decoder's own form semantics as the row-gated
column candidate, validated against the `Mul` reference), and genuine var×var
sites lift and prove.

What stands is the **search-side exclusion** of multiply-composition paths: the
sketch grammar never gains a multiply cell (the intractability ruling for the
search), and the fit-shape class — a composition column the ladder does not model
— keeps its typed `Unsynthesizable` (closed as a boundary at D10/T18: the k=5 rung
was implemented, measured dead, and reverted).

The constant-coefficient and carryless classes remain covered by `MulC`,
`MulHighC`, and `GfMul`.

</details>

---

### Memory models

Two models, one switch.

- **`Legacy`** (default) — reproduces the pre-region behavior byte-identically.
- **`memory_model="region-backed"`** — engages a byte-addressed **SSA memory
  engine** over *declared region contracts*: loads resolve to **existing**
  expressions (input vars for symbolic-init cells, the same stored expression for
  written cells) — **no new `Expr` node ever reaches the delivered model**.
  Unresolvable shapes are typed refusals, never fallbacks.

#### Declared contracts (uniform — no per-target tuning)

| contract | meaning |
|---|---|
| `stack_region=(below, above)` | an RSP-anchored window; `above` covers the MS x64 shadow/home space |
| `buffers=[{arg_reg, extent, init, align?, output?}]` | pointer-input buffer contracts: `symbolic` (free input vars, named in the manifest), `fixed` bytes, or `uninitialized`; `output=(off, len)` projects the exit-version cells of a declared window |
| `preserved_regs=[...]` | callee-saved obligations, each a separate equivalence query with a recorded counterexample on violation |

#### Memory safety as live obligations

Discharged in the manifest, in order: **vacuity first** (`sat_p` — a contradictory
precondition that would fake UNSAT is caught), then `bad_access` (no out-of-region
access), `output_mismatch`, and `preserved_regs`.

> [!WARNING]
> An `Unknown` or `Violated` obligation **vetoes** `delivery_validated`.
> It never upgrades a claim level.

#### Loop-carried stack state

The region engine builds a **slot map**: a slot is a memory VA both written and
read across the back-edge. With multiple loop forms the slot map is the **union**
over all bodies, and aliased spill VAs (one logical slot at different VAs — the
`-O0` spill shape) are merged into one state slot by a
**trace-value-continuity witness**: the value written to `VA_A` by iteration *i*
equals the value read from `VA_B` at the loop-top of *i+1*, on **every** observed
iteration. Ambiguity, a partial witness, or an un-witnessable co-observation is a
typed refusal with a full-compose fallback that names the cause.

Unresolvable memory shapes surface as **27 typed exceptions** carrying address,
region, and reason — never flattened into a generic read failure.

---

### Loops

Three lanes, chosen by loop shape.

<details open>
<summary><b>Count loops</b> (fixed body)</summary>
<br>

Composed by bounded unrolling — full unroll for short bodies (≤ 8 iterations), the
round-induction lane beyond that. A memoized substitution bounds the exponential
path blowup: a **3.5×10⁹-logical-path composition runs in ~0.5 ms**.

</details>

<details>
<summary><b>Path-merge loops</b> (variable body — the <code>-O0</code> data-dependent-branch shape)</summary>
<br>

Each body shape is composed separately, a **carrier** discriminates the shapes, and
the bodies merge into a nested `ite`. Carriers come from counter-style register
evolution or from the trace's own per-iteration loop-top register snapshots — a
snapshot carrier is admitted **only** through a MANDATORY input-independence gate:
its trajectory must be identical across every run of the group, and a differing
trajectory is an input-dependent carrier the lift refuses honestly. The evidence
class (trace snapshots, N runs, empirical gate) is disclosed on the claim surface.

</details>

<details>
<summary><b>Round induction</b> (long fixed-shape loops)</summary>
<br>

The one-round transition **F** is composed once; a step-witness proof
(`F∘F ≡` the composition of two blocks, escalated by a k-step ladder) plus the
proven base delivers **Rⁿ for the contract n** — the declared iteration count.

This is deliberately **NOT** an unbounded ∀n induction; the residual says so
verbatim. The D10 boundary measurement sits underneath: the step at symbolic *k*
(the free-state obligation + the implication *P(k) ⇒ P(k+1)*) is machine-checked;
the induction-rule application *k → ∀n* is not (no SMT engine applies it — the
typed research residual).

The lane engages only on a **whole single-group path** (a fixed trip count): a
data-dependent trip count refuses at the named multi-path shape, never a silent
round-summarized claim over a varying *n*.

</details>

#### The 3-part soundness contract

Every path-merge / round-induction verdict routes through:

1. **(a)** per-shape body equivalence;
2. **(b)** condition discrimination — the merged condition separates the observed shapes;
3. **(c)** the round-induction step.

Carrier trace values are **discovery, never the proof**. Self-test is waived for
round-induction lifts — the step witness and trace evidence replace the n-round
emulator run — which is exactly why the (a)/(b)/(c) contract is the gate.

---

### The proof stack

Three layers, weakest first, all machine-checked:

| # | layer | role |
|---|---|---|
| 1 | **Normalization** | structural rewriting that decides equivalence outright when candidates normalize to the same form. Free, no solver. |
| 2 | **Z3 (QF_BV)** | bitvector SMT via hand-rolled FFI. Every z3-UNSAT that gates a positive verdict is **GUARDED** (below). |
| 3 | **cvc5** | an independent third engine, and the certificate producer. |

Solver uncertainty always surfaces as a typed `Unknown` — never a silent maybe,
never an aggregated "passes".

#### 🛡️ The z3 false-UNSAT guard

> [!CAUTION]
> **Z3 4.16.0 was shown to return a false UNSAT on a satisfiable QF_BV formula** —
> reproduced through Darwin's own FFI path on a near-equivalent obligation pair,
> the exact shape a delivery-gating proof uses, where the wrong answer would have
> surfaced as a **false PROVEN**.

The mitigation is structural: every z3-UNSAT that gates a positive verdict (the
equivalence proofs, the bundle proofs, the coverage / index-range / memory-safety
checks) is **re-solved on a bit-blast+sat tactic solver**.

| outcome | result |
|---|---|
| Confirmed | the verdict stands |
| Contradicted | `Refuted` with an eval-verified witness, or `Unknown` |
| Unconfirmed | `Unknown` — an unconfirmed UNSAT is **never** delivered as PROVEN |

A cvc5-disagreement gate backs the same sites. **Measured cost: +13.5%** on the
verifier suite — the price of the guarantee.

#### 📜 Certificates

Every PROVEN verdict is exported as a **cvc5 Alethe proof log** and checked by an
external checker (`tools/alethe-check` — pure Python stdlib, a **44-rule
whitelist** with a small named trusted-axiom set, pinned by tamper-mutation tests).
Multi-output claims produce one conjunctive bundle certificate; blind multi-output
bundles are certified against the `lifted_binary` reference.

The certificate **NEVER changes the verdict**: checker disagreement means no
artifact plus a typed residual; checker timeout means an honest *not-run* plus a
weakened marker — never a fake `ACCEPT`. The checker subprocess is wall-bounded.

#### 🔑 Equivalence by fingerprint is discovery, not proof

An alpha-canonical, variable-renaming-invariant fingerprint indexes a lemma
registry: a fingerprint hit *proposes* the equivalence and recovers the variable
bijection, then a real ∀-proof decides it. **The hash never grants equivalence.**

---

### The claim vocabulary

| `res.proof` | claim level | meaning |
|---|---|---|
| `PROVEN (normalization\|Z3 QF_BV\|cvc5)` | model-equivalence | truth mode: candidate ≡ truth, ∀2^B over the joint domain |
| `PROVEN (lifted_binary)` | lifted-binary-equivalence | blind mode: candidate ≡ the independently encoded per-instruction substrate, ∀2^B over the covered class |
| `PROVEN (round-summarized)` | round-induction | base + step witness ⇒ Rⁿ for the contract *n* |
| `SELF-TEST ONLY` | sampled-conformance | sampled oracle runs, no ∀-guarantee; carries a named residual |

Three evidence kinds are reported **separately** and never aggregated into one
"passes" verdict: *model equivalence*, *per-instruction validation*, *sampled
binary conformance* — plus *memory safety* as its own group.

The delivery gate is explicit:

> `delivery_validated` is true **only** when the proof (or the blind ∀-proof)
> **AND** the self-test pass **AND** every table is `Full`.
> `Refuted` / `Unknown` force it false.

Model uncertainty is resolved by proof or by established irrelevance — sampled
values are never frozen into a model. The flags policy is the canonical example: a
carry-in is a symbolic input constrained by the observations; a flag nobody
consumes is *proven irrelevant*, not guessed.

---

### Soundness rules

- **Blind-∀ with a named residual.** The blind proof covers the declared subdomain;
  whatever is not covered is named in the atom's residual list (typed, with the
  counterexample or the budget note) — never silently dropped.
- **Refusal over approximation.** Out-of-scope shapes — unmodeled memory forms,
  unsupported instructions, unwitnessable slot unifications — raise typed errors
  that name the exact blocker **and its address**.
- **The canary discipline.** The demo battery's claim-summary lines are hash-pinned
  and re-measured after every change: a moved verdict hash that is not a
  deliberate, reviewed re-baseline is a **build failure**, not a diff to review.
  The claim line carries only level / validated / coverage — never solver internals
  — so the pin stays stable while internals evolve.
- **Sentinels never leak.** Discovery-time probe sentinels are guarded out of
  delivered expressions; a leak is a typed refusal, and a canonical candidate that
  would inject one is rejected by a complexity guard.
- **Unknown never aggregates.** No combination of partial evidence ever produces
  `validated=true`.

---

### The key-material report

`res.key_material` is the one-command answer to *"which bytes feed this code"*:

- **`sites`** — every external-data window the primary expression depends on:
  used tables, byte-exact and VA-anchored; region-symbolic runs with per-byte
  var↔VA wiring (unused bytes excluded and noted); fixed windows with the folding
  caveat stated.
- **`candidates`** — width-matched (16 / 24 / 32-byte) fully-used windows, each a
  labeled hypothesis with a reason **and an origin** — `embedded-static` (the
  bytes are in the artifact: a `.rdata` key table, a fixed region) or
  `supplied-symbolic` (the bytes are caller-supplied inputs: the key is NOT in
  the image, and the site carries the per-byte var wiring, never invented bytes)
  — narrowed when `identify()` names a cipher.
- **`iv_sites` / `weakness_flags` / `mode_hint`** (D11) — the IV/nonce windows of
  the identified family's width; the material weaknesses (`static-iv`,
  `constant-nonce` — fired on the material, independent of data wiring); and a
  discovery-grade mode hint (`ecb-ish` / `cbc-ish` / `ctr-ish` / `unknown` —
  a hint, never a claim).

> [!NOTE]
> Candidates are **discovery, never verdicts**. Confirming that a candidate is
> the key — decrypting a known pair with the candidate bytes — *was* the
> caller's step. **D11 makes Darwin the caller**: the [verify
> oracle](#the-artifact-key-pipeline-d11) measures the candidate into a
> `VERIFIED` / `REJECTED` verdict, and the decrypt runner releases the
> plaintext on a green held-out gate.

The report works on flat blobs (wiring-only, stated in the notes) and on PE images
(site bytes are byte-equal to the image read; `VA = image_base + RVA`).

---

### The artifact-key pipeline (D11)

D11 closed the loop the report used to leave open — one rung ladder from the
PROVEN model to measured key claims and (for the identified shape) the plaintext.
Every rung's verdict discipline is the same one the lift itself carries: measured
runs, honest refusals, never a guess.

#### ⑤ The key-material report v2 — origin classes

The report classifies every candidate's bytes by **origin**:
`embedded-static` (the bytes live in the artifact — extracted byte-exact from
the image) or `supplied-symbolic` (the bytes are caller-supplied inputs — the
key is not in the image; the site reports the wiring). The **all-surface walk**
covers the primary expression AND every output projection / bundle component
(v1 walked the primary only — the projection-only key dependency is now
visible). The IV/nonce classification, weakness flags, and mode hint land here
(see [the key-material report](#the-key-material-report)); every ambiguity arm
(the AES key/IV width collision, a mixed family, multiple IV-width sites)
**notes the fact and refuses to guess**.

#### ⑥ The verify oracle — measured verdicts

`verify` materializes the candidate at its key slot and runs the emulated
function once per recorded known pair, comparing the **measured** output bytes
against the recorded ciphertext:

| outcome | meaning |
|---|---|
| `VERIFIED` | every pair reproduced in a completed run |
| `REJECTED` | a completed, measured disagreement (one flipped key byte is enough) |
| `Err` — no verdict | a crashed or malformed run, an empty pair list, a key that does not exactly fill the declared slot — **an error can never degrade to `REJECTED`** |

The oracle never executes natively. A **code-page write guard** refuses any
write into an executable section (a stale translated-code cache is the hazard);
the key-slot exact-fill rule refuses a short key *before* any run; a wrong-length
or undeclared slot is a shape refusal, never a verdict.

#### ⑦ The held-out-gated decrypt runner

`decrypt` turns a key plus the data buffer into plaintext — gated by the
**held-out pair** (recorded alongside the known pairs, **never a solve input**):

- **(a) the measured forward leg** — the emulator reproduces the held-out
  ciphertext from the held-out plaintext with the candidate materialized at the
  key slot;
- **(b) the inverse leg** — the native decrypt of the held-out ciphertext equals
  the held-out plaintext.

`heldout_ok` is the AND of both legs (the mixed-leg outcomes are pinned by a unit
test — an OR gate fails it). A green gate is the only thing that licenses
decrypting the *other* bytes: leg (a) alone proves the key against the binary but
nothing about the native model; leg (b) alone proves the native model only against
caller-supplied bytes no emulator ever measured. The **withheld-plaintext rule**
is enforced in every rendering — `to_json`, `summary`, and the custom `Debug`
print the withheld marker on a red gate, never the computed bytes.

#### The no-key utilities

Byte-level facts about the ciphertexts themselves — no key, no emulator, no model:

- **`xor_recover`** — under a **reused keystream** (the `constant-nonce`
  consequence), `C1 ⊕ C2 = P1 ⊕ P2`: the key cancels. The result is the XOR of
  the two plaintexts, **not a plaintext** — recovering both requires
  crib-dragging; knowing either plaintext in full recovers the other.
- **`ecb_repetitions`** — the ECB repetition map: which ciphertext block
  positions hold equal bytes. Under ECB, equal ciphertext blocks leak equal
  plaintext — pattern structure with zero key material.

#### The frozen-instance export

`export` serializes a lift, its recorded pairs, its candidates, and the
expression AST into **one JSON artifact** — the substrate the attack bridge
consumes. The expression is a **DAG-faithful flat node array**: every unique DAG
node once, children by index. The supplied-key specimen's expression is a
**~700M-logical-node tree over ~170 unique DAG nodes**; the export writes
**245 nodes** (~10 KB of JSON) and the logical tree is recoverable by index
expansion — the losslessness contract. (The two DAG counts differ honestly:
pointer-unique vs value-consed identity; both are ~6 orders below the expansion.)

#### The attack bridge — solver = discovery, oracle = the claim gate

`tools/attack-bridge/` closes the loop on the export: a **generic Expr→CNF
bit-blaster** (no cipher knowledge), a **z3 DIMACS solve**, and the claim gated
by the product's own CLI oracle:

> A SAT model is a **candidate**. It becomes a claim ONLY when `darwin verify`
> measures it — materialized at the key slot, one completed emulation run per
> known pair, bytes compared. A collision key is REJECTED; UNSAT / TIMEOUT are
> honest non-results. The held-out pair runs **post-claim**, as evidence — never
> as a solve input.

The claim wording is exact: **"a key reproducing the artifact's measured
behavior"** — never "the unique key". At the demonstrated (calibrated) round
count, `k[0]` is the key's equivalence class under the oracle: the 2-cycle cipher
never reads it, so any value verifies. The encoding itself is validated
independently of the search wall (the unit groundchecks, a fully-pinned
differential, the committed full-grammar op sweep) — and the 1-cycle instance
that solves but is **REJECTED** by the oracle is the discipline's own proof that
the gate has teeth.

---

## Honest limits

> **The D10 ledger-emptying record:** every open item now holds a terminal state.
> What the stage closed is listed with its measurement; what remains is stated as a
> **contract** — present-tense designed behavior, each with its typed refusal and
> the site where it fires. **Nothing below is deferred work**, and every number is
> a measurement on this project's corpus (the battery walls live in
> [Benchmarks](#benchmarks)).

<details>
<summary><h3>✅ CLOSED (D10, measured) — 20 items</h3></summary>
<br>

- **The model-coin chain (T1/T16/T22/T23):** the unification ambiguity gate is
  model-independent on both value planes — the write-grounded and identity-grounded
  unions — and the chain terminated at the fourth order (the reviewer's independent
  census: 4 code sites, all unreachable; no fifth order). The N=20 parallel
  determinism pin holds; the D9 slotambig pair is un-retired and green serial and
  parallel; the serial suite checkpoints ran 890/0/49 → 896/0/49 → 898/0/49.
- **The round-lane whole-path guard (T10):** the mid-tree partial-path compose — a
  false `PROVEN (round-summarized)` whose model mismatched native at every input,
  measured pre-fix on `loop4_epi` — is dead; the round lane engages only on a whole
  single-group path, and the killer fixture pins it (model matches native
  everywhere, no round record, no round-summarized claim); the round corpus is
  byte-identical.
- **The path-merge whole-path guard (T21):** the same false-PROVEN class killed on
  the path-merge lane — RED twice (`loop4_vb_epi`; the `path_merge_inpkey` false
  PROVEN at an observed input); exactly two production routes exist, both guarded;
  the corpus is byte-identical.
- **The counter-init input-independence check (T20):** a data-dependent trip count
  with a single observed group refuses (typed `data-dependent-counter` /
  `data-dependent-stack-counter`) instead of generalizing — the `loopn_sel` RED
  fixture pinned the exposure.
- **The w0 pair demotion (T3):** all 40 matching co-observations of the
  `(0x7f00fea8, 0x7f00fee0)` pair are machine-derived PROVEN from the run's input
  and the pair's independent value chains — degenerate coincidences, not storage
  identity — and the pair is demoted (coincidence-explained, disclosed on the claim
  surface). The w0 refusal moved to the partial pair
  `(0x7f00fea8, 0x7f00ff10)`, 1/320, whose one match is refuted by a counterexample
  input.
- **The w0 full-compose arm (T4):** the byte-identical
  `SelfTestFailed {got: 2190979457, want: 904260009}` (both arms, since D8) is
  root-caused — the unchanged-register skip read the strided 10-row sample and
  dropped a real write; the full-evidence discipline (the skip, the tie-break alias
  checks, the post-fit guard — all reading the full pooled row set) passes the
  self-test on both lanes.
- **The preheader routing (T5):** the loop-summary lane is chosen at the preheader
  by a pure shape predicate with a typed re-route residual (6 pins); the w0 lanes
  are byte-identical.
- **The B=64 compose defect (T17):** the C7/REX.W immediate-width rule (the event-8
  write plane stored the 8-byte over-read constant where the emulator stores the
  sign-extended imm32) — the w64 full-unroll control now passes the self-test.
- **var×var multiply + imul (T6):** the one-operand decode gap closed (census `mul`
  1759→71, `imul` 36→4), the form-templated arm landed (the decoder's own form
  semantics as the column candidate, row-gated, downstream unchanged), two
  synthetic cells PROVEN and Validated, and the real zlib `adler32` R11 site — the
  genuine var×var — templated and row-validated; combined coverage 93.799% →
  94.782% (**+0.983 pp**).
- **The XMM/SSE register class (T7):** the lane-indexed modeling at B=64 (two qword
  lanes, a separate lane var space, zero new DSL machinery); the packed-lane and
  `pshufd` cells PROVEN; coverage 94.782% → 95.469% (**+0.687 pp**, unsupported
  9126→7844).
- **The AArch64 adjacent forms (T8):** the 28-entry checklist enumerated from the
  decoder's own refusal messages — 24 forms closed with goldens, 4 as boundary
  contracts; the arm64 test surface grew 73→86; the logical-immediate
  `DecodeBitMasks` algorithm fitted **312/312** encodings against the assembler
  oracle and is emulator-pinned.
- **Indirect-call dispatch (T9):** the table-driven fan-out lifts and PROVES — the
  dispatch fixture is PROVEN in truth mode and its blind `PROVEN (lifted_binary)`
  verdict pinned at runs=24; census coverage 95.469% → 96.402% (**+0.934 pp**;
  call-indirect 1713→0: 1463 table-driven sites now decode, 152 register-direct
  sites refuse by class, 98 RIP-relative sites stay the named PLT/IAT boundary).
- **The coverage progression:** 93.799% → 96.402% across the D10 decode closures
  (multiply +0.983 pp, SSE +0.687 pp, indirect-call +0.934 pp, each measured by its
  own sweep); the T12 linear re-run stands at **96.549%** (173,248 sites).
- **The census parity (T12):** AArch64 measured on real cross-compiled objects —
  **93.146%** over 2524 sites; the 32-bit x86 mode measured on linked PE32 DLLs and
  COFF objects — **94.011%** over 4074 sites; the CFG-reachable census measured:
  linear 96.549% (173,248 sites) vs reachable(entry+exports) 96.847% (134,772
  sites) vs the thin entry-only strand 94.669% (5252 sites).
- **The ignored-cells adjudication (T11):** all 56 ignored cells hold a terminal
  state — 46 ran to a verdict under a declared budget (42 re-pinned, 4 un-ignored
  into the running battery), 10 are permanent diagnostic probes; every ignored
  attribute carries a reason, enforced by the lint gate (roster 73).
- **The Python levers (T13):** `sketch_timeout_ms`, `round_induction`,
  `partner_entry` are typed kwargs on the lift surface, defaulting to the core's own
  defaults (`30_000` / `true` / `None`); 21 new pytest cells; the `.pyi` stub parses.
- **The lemma-registry parallel isolation (T24):** the reentrant registry gate (a
  registering lift blocks behind the counter tests' lock; the counter asserts stay
  exact) — the full parallel lib suite runs 910/3/46, and the 3 are the z3-budget
  class below, each green solo (the registry-bleed failures eliminated: 907/5/46
  before).
- **The cvc5 watchdogs (T19):** every solver spawn is wall-clock-bounded (the
  child's own `--tlimit` plus a grace margin; a past-deadline child is killed and
  reaped, the caller returns the honest `None` floor — never a hang, never a partial
  log), and the per-column prove loop checks its cancel deadline between columns
  (the typed between-columns timeout).
- **The verify-and-close trio (T2):** `cert_mode` verified ON since D6/T1 (the stale
  doc comments fixed); the cross-call canonization closed by design
  (`alpha_canonical` — 13/13 fingerprint lookup hits measured, every hit PROVEN);
  the `sar r/m, cl` asymmetry fixed as the contract below.
- **The stale mul expectation (absorbed at T13):** the pre-existing
  `test_validation_errors` expectation (mul ⇒ `ConfigError`) corrected in its own
  commit — the D10/T6 `Op2::Mul` surface had made it stale.

</details>

<details>
<summary><h3>📐 CONTRACTS (present-tense designed behavior) — 16 items</h3></summary>
<br>

- **Round induction is contract-n by design.** Everything the checker can check is
  machine-checked — the k-uniform step (`F∘y ≡ B(y)` over the free state, decided by
  the standard prover), the base, and the step implication at symbolic *k* (cvc5:
  unsat) — while the induction-rule application itself (base + step ⇒ ∀n) burned its
  full checker budget with no verdict: SMT-LIB has no induction engine. The claim
  lattice gains no level a checker cannot machine-check; the ∀n generalization stays
  a typed research residual, stated verbatim on the claim.
  *Fires at the round-induction lane's claim surface.*
- **Mutable tables only in declared regions.** A mutable-state shape in an
  undeclared region stops at the typed `MutableTableError`; a mutable-state cipher
  in a DECLARED buffer region (RC4-class) lifts + proves + delivers the keystream —
  declared-region discipline, not silent mutable-table support.
  *Fires at the region engine.*
- **The checker's 10 trusted bit-blast axioms (the documented TCB).** Of the
  external Alethe checker's 44-rule whitelist, the 10 `bv_bitblast_step_*` rules are
  accepted on solver trust and are not semantically re-derived (bit-blast
  re-validation is impractical at real proof sizes); every other rule is checked
  structurally or is a named STOP-threshold.
  *Fires at `tools/alethe-check` (the honesty register).*
- **No native execution, ever.** Sample code runs only inside the Unicorn emulator
  sandbox; the core never executes a sample on the host.
  *Fires at the lift pipeline's emulation step.*
- **The determinism contract (quiescent same-machine determinism).** Under
  concurrent in-process solver load a candidate selection can diverge (never the
  model's soundness); the serial protocol is the adjudicator. The named mechanism
  class — a solver model coin on a structurally underdetermined fit — is closed: the
  gate's decision path is model-free on the structural classes (the T1→T23 chain
  above). *Fires at the unification ambiguity gate and the battery's serial protocol.*
- **The checker budget policy.** Generous by design (a legitimate large proof fits
  with ~2× margin; a hang is detected at the bound, not sooner); every cvc5 spawn
  carries the wall-clock watchdog and returns the honest `None` floor on kill; the
  per-column prove loop exits at its cancel deadline with the typed timeout verdict.
  *Fires at the verifier's solver spawns and the prove loop.*
- **The verdict protocol is serial (the z3-budget parallel class).** Full parallel
  single-process suite runs are advisory: under 16-thread parallel z3 load the
  sketch-phase ladder cells can exhaust their ladders and fail — the known cells are
  `d3_multiterm`, `d3_rangeobligation`, the boundaries `setcc` cell, and
  `branching_fixtures_best_effort_with_typed_residuals`, each green solo. The
  registry-bleed subclass is closed (T24's reentrant gate).
  *Fires at the sketch ladder under parallel solver load.*
- **The AArch64 boundary families (measured in the 93.146% census).** ADRP (59
  sites) — the PC-page-relative address materialization, outside the tracked M13
  family; the V-register space (45 sites: FP/SIMD load/store 26, AdvSIMD load/store
  structures 17, SIMD ALU 2) — the V file is outside the tracked `X0..X14` surface;
  the never-claimed integer set (69 sites: general bitfield 25, conditional-select
  20, MADD/MSUB 17, TBZ/TBNZ 7); the reserved move-wide encodings refuse as
  encoding-space holes. Typed refusals with the census as evidence — no hidden
  classes. *Fires at `arm64dec`.*
- **The x86-32 boundary classes (measured in the 94.011% census).** `shld` (28), the
  GNU-ld i386 GOT thunks (FF /4 SIB-absolute, 24), the Bits32 absolute-addressing
  operand class (`xor r,r/m` 15 + `mov r8,r/m8` 15 — mod=00 rm=101 / SIB-base=101),
  the push-immediate family (12 + 8), `call [absolute disp32]` (10 — the IAT stub).
  *Fires at the decoder's Bits32 mode.*
- **The macOS platform boundary.** A platform decision recorded as a boundary, not a
  Darwin defect: the macOS wheel is a deliberate carry, and the CI surface is
  Windows + Linux. *Fires at the packaging/CI surface.*
- **`sar [mem], cl` stays decoder-`Unsupported`.** The asymmetry vs
  `shl/shr/rol [mem], cl` is deliberate — the RMW-through-memory class, the
  ImulWide/XchgRR precedents — and documented at the decode site. An honest typed
  refusal, not a silent gap. *Fires at `x86dec`.*
- **The var×var search exclusion.** The sketch grammar never gains a multiply cell
  (the intractability ruling stands for the search); decoder-known multiply forms
  take the form-templated arm instead; the high-half columns (ImulWide DX — the
  signed high; MulWide DX — the unsigned high, refusing even under const-prop) and
  the 16-bit pair forms refuse. *Fires at the sketch ladder and the templated arm.*
- **The indirect-call boundary classes.** Computed targets (`call reg` — register
  arithmetic), dispatch through non-committed tables (heap/vtable),
  `call [rip+disp32]` (the PLT/IAT stub table is outside the lifted image — 98
  corpus sites), tables with more than 8 in-image targets (the typed fan-out cap),
  and multi-way `jmp r/m` (jump tables) each refuse with the class named.
  *Fires at the dispatch gate.*
- **The SSE/XMM boundary contracts.** The memory-rm SSE class (the register-scope
  boundary), the VEX/EVEX forms, and the mixed GPR/SSE compose pipeline are outside
  the integer-SSE core that lifts and proves. *Fires at the SSE lane.*
- **The w64 memory-bound budget boundary.** At the raised sketch lever the deep
  `F∘F ≡ s2` proof grows past this host's memory-reap threshold (~6.5 GB DAG growth,
  no delivered verdict) — an honest budget boundary, not a correctness refusal; the
  named lever is the memory-bounded witness (the memoized-walker precedent).
  *Fires at the w64 path-merge lane.*
- **The fit-shape refusal (the ECX column).** The zero-extending 32-bit ALU write at
  B=64 is a shape the ladder does not model: the k=5 rung was implemented, measured
  dead, and reverted; the column keeps its typed `Unsynthesizable` with the measured
  reason. *Fires at the sketch ladder.*
- **The strict witness-gap rule, scoped per candidate pair.** An un-witnessable
  co-observation in an unrelated pair contributes nothing (the over-broad
  whole-union refusal is gone); within a candidate pair the strict rule stands —
  partial evidence never confirms. Soundness over capability.
  *Fires at the slot-unification witness.*
- **The typed refusal record on the error path.** A failed self-test on a blind path
  carries a typed record through the error path — the loop context, the refusal note,
  and the open residuals survive with the `Err`; the cause never dies in the progress
  log. *Fires at the error surface.*

</details>

<details>
<summary><h3>🔶 D11 — the artifact-key pipeline limits (measured)</h3></summary>
<br>

- **No chaining modes, no full-round recovery.** The demonstrated decrypt and
  bridge class is the reduced-round supplied-key specimen (ECB, XTEA-8 / the
  calibrated 2-cycle XTEA); CBC/CTR chaining and full-round (8-cycle) recovery
  are outside the demonstrated surface.
- **The AES key/IV 16-byte width collision.** 16 is both the AES-128 key width
  and the AES IV width: an integrated AES-family report reports the ambiguity
  note ("key or IV is ambiguous; not classified as an IV site") for a 16-byte
  window — never a `static-iv` flag. ChaCha/Salsa's 12/8-byte nonces do not
  collide.
- **The 1,000,000-logical-node identification budget gate.** Giant composed
  models (the ~700M-logical-node straight-line class) report origin/wiring but
  skip cipher identification and the structural fingerprint with **loud notes**
  (the note carries the node counts) — never silently; the origin classification
  does not depend on identify.
- **`mode_hint` is discovery-grade.** A hint (`ecb-ish` / `cbc-ish` /
  `ctr-ish`), never a mode claim; every ambiguity arm (a mixed family, multiple
  IV-width sites, the width collision) notes the fact and refuses to guess.
- **The bridge's calibrated 2-cycle count; the 4+-cycle CDCL round-chain wall.**
  Each Feistel cycle adds one guess-and-determine level to the chained
  intermediate states: the 2-cycle instance solves in 0.40 s and the oracle
  VERIFIES; 3 cycles has no answer within 1800 s (the 2→3 cliff is ≥ 3 orders of
  magnitude) — a **research boundary, not an encoding limit** (the encoding is
  validated three ways: the unit groundchecks, a fully-pinned differential, the
  committed full-grammar op sweep). The 1-cycle instance that solves but is
  **REJECTED** by the oracle (its recovered k[3] byte disagrees with the measured
  runs) is the discipline's own proof that the claim gate has teeth.
- **The claim wording.** "A key reproducing the artifact's measured behavior"
  — never "the unique key": at the calibrated count, `k[0]` is the key's
  equivalence class under the oracle (the 2-cycle cipher never reads it).
- **The bridge attacks the export's PRIMARY expression only** (the exit RAX
  word); the pointer-window output (v1') is not serialized in the artifact.

</details>

---

## Benchmarks

> [!NOTE]
> All numbers below are **measured on this corpus** — the project's own fixture and
> battery suites, run **serially on one quiescent machine**. They are measurements,
> **not guarantees**: walls scale with hardware and solver versions.

### Full battery — every suite, zero failures

Re-measured at the **D11 close battery (2026-10-02)**. The core-library suite runs
chunked-serial — the regenerated family-filter list (every D11 module included),
one process each; the wall is the sum of harness walls.

| suite | result | wall |
|---|---|--:|
| core library (serial, full) | **960** passed / 0 failed / 45 ignored | 5822 s |
| integration (boundaries · census · bitscan · guardite · exp16/exp16b) | **118** passed / 0 failed / 8 ignored | 873 s |
| Python bindings (pytest) | **285** passed / 0 failed | 546 s |
| attack bridge (pytest — the SAT loop with the oracle gate) | **10** passed / 0 failed | 31 s |
| Alethe checker suite | **16** passed / 0 failed | 237 s |
| native bindings | **17** passed / 0 failed | 56 s |
| per-instruction validation demo | **PASS** — 37/40 validated, 0 refuted, 3 not-validated — **zero** Validated-to-Refuted | 43 s |
| demos (region · multi-output · inverse · `d11` · the export verb) | **all PASS** — the `d11` demo 40 s, the export verb 40 s | — |
| workspace + examples build | **0** errors / **0** warnings | — |

The same battery re-measures the **determinism anchors** (three pinned fixture
hashes, unchanged) and the three **determinism canaries** — the claim summary, the
atom digests, the certificate sweep — **all three UNMOVED** (deterministic across
two full runs each; the certificate-sweep canary via the instrumented procedure).

### The soundness guard's price

The z3 false-UNSAT guard costs **+13.5%** on the verifier test module
(730.4 s → 828.9 s) — every delivery-gating z3-UNSAT is re-derived on a second
solver before it is trusted.

### The D11 pipeline modules — measured

One run each, the phase's detached verification runs (2026-10-01/02) on this
corpus; the D11 close battery re-measures and the LEDGER carries the record.

| module / surface | result | wall |
|---|---|--:|
| keymat v2 (origin classes, IV/nonce, weakness flags, mode hint — incl. the real `ransom_embed` and `supplied_key` PE lifts) | **28** passed / 0 failed | 183 s |
| verify oracle (the measured `VERIFIED` / `REJECTED` verdicts) | **7** passed / 0 failed | < 0.1 s |
| decrypt runner (the held-out gate, the withheld-plaintext rule) | **6** passed / 0 failed | < 0.1 s |
| frozen-instance export (incl. the ~3-minute `supplied_key` blind lift) | **5** passed / 0 failed | 182 s |
| no-key utilities (`xor_recover`, `ecb_repetitions`) | **8** passed / 0 failed | < 0.1 s |
| attack bridge (`tools/attack-bridge/test_bridge.py` — unit groundchecks, the full-grammar op sweep, the demo loop) | **10** passed / 0 failed | 32 s |
| Python bindings (pytest, the full suite) | **277** passed / 0 failed | ~570 s |
| `darwin d11` demo (keymat → verify → decrypt, end to end) | **PASS** (exit 0) | ~41 s |

The bridge's closing loop on the committed `rr_xtea` fixture (2 calibrated
cycles), step by step: **export** 88 DAG nodes / 4 pairs in 30.7 s → **CNF** 8
instances / 7099 vars / 27088 clauses in 0.06 s → **SAT** in 0.40 s → 12/16 key
bytes solver-determined → **`darwin verify` VERIFIED** → the held-out pair
reproduced post-claim.

### 🟢 PROVEN cells, measured

One run each unless noted.

| cell | verdict | wall |
|---|---|--:|
| `sar r/m, cl` roundtrip (B=32) | PROVEN, the SarCl column Validated against the frozen ISA reference | ~2.5 s |
| PE `.rdata`-table lift (committed fixture; table found outside the function window) | PROVEN (Z3) | — |
| synthetic 4-way variable-body loop (path-merge) | PROVEN (round-summarized) | ~1 ms |
| register-carrier loop | PROVEN (round-summarized), carrier EBX, trajectory [8..1] | — |
| spill-aliasing loop (unified slot map) | PROVEN (round-summarized) | — |
| XTEA register form, B=32, 32 rounds | PROVEN (round-summarized) | 64.2 s / 64.7 s (×2) |
| XTEA register form, B=64, 32 rounds | PROVEN (round-summarized) | 220.6 s / 181.0 s (×2) |
| XTEA gcc-form, stack-carried state, 32 rounds | PROVEN (round-summarized), 3 carriers | ~69 s |
| `ransom_embed` enc_block blind lift (the D11 keymat path) | PROVEN (round-summarized) — the embedded 16-byte key candidate byte-exact at its `.rdata` VA | ~47 s |

### 🟡 The honest endgame walls

The hardest cells in the corpus (a real `gcc -O0` XTEA), delivered as **typed
verdicts, not as proofs** — re-measured at the D10 battery after the A3 fix;
re-confirmed at the D10 close battery (2026-09-28), same typed verdicts at the
default budget: w0 49.5 s / 42.6 s, the w64 path-merge TIMEOUT at the 300 s cap, the
w64 full-unroll SELF-TEST ONLY at 363.0 s.

| cell | outcome | wall |
|---|---|--:|
| **w0 (32-bit), path-merge lane** | honest refusal: slot-unification resolve-or-refuse — trace-value continuity held on only **40 of 320** observed iterations for the degenerate pair; the full-compose fallback now **PASSES** the self-test (D10/A3) | 50.9 s |
| **w0 (32-bit), full-unroll control** | `SELF-TEST ONLY` (D10/A3: the self-test refusal root-caused and closed — was `SelfTestFailed {got: 2190979457, want: 904260009}`) | 43.0 s |
| **w64 (64-bit)** | see below | 314.1 s |

<details>
<summary><b>w64 (64-bit) — the full measurement record</b></summary>
<br>

**Path-merge lane:** `TIMEOUT` at the 300 s rung-ladder cap — the default sketch
budget masks the k = 3 sketch; at `sketch_timeout_ms = 120000` the sketch is found
in **56.1 s** (the budget-mask refutation). At that lever the D10/T17 re-route
composes the `s2` ground truth past the old `UninitializedRead{0x7f00fed0}` refusal
(the loop-entry threading), and the deep `F∘F ≡ s2` proof then runs past this
machine's memory-reap threshold (**~6.5 GB** DAG growth, no delivered verdict — an
honest budget boundary, **not** a correctness refusal).

**The honest-budget run** (default 30 s rung), re-measured at the close battery: the
typed `Unsynthesizable {reg: RAX, ladder: [1, 2, 3, 4, 6]}` at **426.6 s**
(rungs 68: 34 found / 25 unsat / 9 timeout) — the T11-era allocation abort did not
recur.

**Full-unroll control after D10/T17:** the B=64 compose defect **CLOSED** (the
C7/REX.W immediate-width decode — the event-8 write plane stored the 8-byte
over-read constant where the emulator stores the sign-extended imm32) — the
self-test **PASSES**: `SELF-TEST ONLY`, **173.2 s**, 73 rungs / 0 timeouts (was the
budget-racy pair: `Unsynthesizable {reg: RAX, ladder: [1, 2, 3, 4, 6]}` 413.0 s /
`SelfTestFailed {got: 5631894065274007705, want: 10608989695597250434}` 356.5 s —
the B=64 follow-up under the D10 absorption rule, resolved).

</details>

---

## Documentation

| document | contents |
|---|---|
| [`docs/SPEC.md`](docs/SPEC.md) | the platform design spec: architecture, module contracts, the Python API shape, the end-state examples |
| [`docs/PYTHON-API.md`](docs/PYTHON-API.md) | the full Python surface reference: every kwarg, claim level, typed exception, and manifest field |
| [`tools/attack-bridge/README.md`](tools/attack-bridge/README.md) | the D11 attack bridge: the oracle-closed loop discipline, the calibration ladder, the honest limits |
| [`THIRD_PARTY_NOTICES.md`](THIRD_PARTY_NOTICES.md) | licenses of the bundled/vendored components |

---

## License

**MIT with a commercial-attribution condition** — see [`LICENSE`](LICENSE).

Commercial use of Darwin must mention the authors, **Ashot G. and Trisha M.**
Everything else stays as open as plain MIT: the one added condition is an
attribution obligation — it closes nothing.

The bundled/vendored third-party components (libunicorn, libz3, cvc5, ABC, GMP, the
GCC runtime) keep their own licenses — see
[`THIRD_PARTY_NOTICES.md`](THIRD_PARTY_NOTICES.md).

---

## Authors and credits

Darwin was developed by **Ashot G.** and **Trisha M.** — a two-person team
throughout the project.

AI coding assistants contributed across the project's lifetime and are acknowledged
with thanks: **claude**, **glm**, **kimi**, **qwen**.

<div align="center">
<br>
<sub><b>Darwin</b> — if it says PROVEN, it means ∀. If it can't, it says so.</sub>
</div>
