Metadata-Version: 2.4
Name: darwin-cre
Version: 0.1.1
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Rust
Classifier: Topic :: Security
Summary: Darwin — universal black-box crypto extraction from binaries: compositional instruction-granular synthesis with machine-checked equivalence proofs (forall 2^32 / 2^64).
Keywords: reverse-engineering,malware,cryptography,synthesis,smt,proof
License: MIT
Requires-Python: >=3.9
Description-Content-Type: text/markdown; charset=UTF-8; variant=GFM
Project-URL: Homepage, https://github.com/Ashibalt/Darwin-Crypto-Reverse
Project-URL: Repository, https://github.com/Ashibalt/Darwin-Crypto-Reverse

# Darwin

**Universal black-box crypto extraction from binaries** — compositional,
instruction-granular program synthesis with machine-checked equivalence proofs.

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
"which bytes feed this code": data-window sites plus labeled key candidates.

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

**The honest-verdict doctrine.** Every lift ends in exactly one of three states:
`PROVEN` (machine-checked over all inputs), `SELF-TEST ONLY` (sampled
conformance, no ∀-guarantee), or `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 rather than approximated,
and the verdict surface is hash-pinned so an unintended change cannot pass
silently.

**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. Hostile binaries are only ever emulated: all execution happens
inside the emulator sandbox, never natively on the host. And every number in
the Benchmarks section is a measurement on this project's fixture corpus —
stated as a measurement, never as a guarantee.

- License: **MIT** (see [`LICENSE`](LICENSE); the bundled/vendored third-party
  components keep their own licenses — see
  [`THIRD_PARTY_NOTICES.md`](THIRD_PARTY_NOTICES.md)).
- Platform: **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), and 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), and 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.
- Toolchain: Rust (stable, edition 2021), the `z3` and Unicorn libraries, a C
  toolchain; Python >= 3.9 for the bindings and the proof-log checker; the `cvc5`
  backend is vendored under `tools/` (optional, run as a subprocess).
- Core: **zero external crates** — hand-rolled FFI to the system libraries; the
  Python bindings crate owns the workspace's only dependencies.

## Quickstart

The Python surface (full reference: [`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 = 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)
```

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

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

## Deep dive

### The lift pipeline

Four steps, one verdict:

1. **Emulation.** 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.
2. **Per-instruction synthesis.** 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.
3. **Symbolic composition.** The per-instruction expressions compose into the
   delivered model: branches merge as `ite` trees, loops take one of three
   lanes (below), memory resolves through the region engine (below). The
   composed candidate is self-tested against the emulator on sampled inputs
   before anything is claimed.
4. **Proof.** 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 below. 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.

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 expression DSL

The delivered model is a small, closed bitvector language: every node is
`Const`, `Var`, `Un(Op1, x)`, `Bin(Op2, a, b)`, `Ite(c, t, e)`, or
`Sel(table, index)` — a byte-exact table lookup, fingerprinted and
VA/RVA-anchored. Expression depth is capped (4096) with a typed error on
every constructor path. The op set:

| 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` is the table select: 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.

`Op2::Mul` (a true var×var integer multiply) is in the DSL — landed
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`.

### Memory models

Two models, one switch. `Legacy` (the 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):

- `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 is discharged as live obligations in the manifest: 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`. An `Unknown` or `Violated` obligation **vetoes**
`delivery_validated` — it never upgrades a claim level.

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

- **Count loops** (fixed body): 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^9-logical-path composition runs in ~0.5 ms.
- **Path-merge loops** (variable body — different per-iteration body
  lengths, the -O0 data-dependent-branch shape): 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.
- **Round induction** (long fixed-shape loops): 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^n
  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.

Every path-merge / round-induction verdict routes through a 3-part
soundness contract: (a) per-shape body equivalence, (b) condition
discrimination — the merged condition separates the observed shapes, and
(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:

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.** 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.
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^n 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, narrowed when `identify()` names a
  cipher.

Candidates are discovery, never verdicts: confirming that a candidate is
the key (decrypting a known pair with the candidate bytes) is the caller's
step. 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).

### 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 the Benchmarks section).

**CLOSED (D10, measured):**

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

**CONTRACTS (present-tense designed behavior):**

- **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 ~2x 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.

## Benchmarks

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.

The full battery (every suite, zero failures), re-measured at the D10 close
battery (2026-09-28; the core-library suite runs chunked-serial — 241
family filters, one process each, the wall is the sum of harness walls):

| suite | result | wall |
|---|---|---|
| core library (serial, full) | 913 passed / 0 failed / 46 ignored | 5834 s |
| integration boundaries | 81 passed / 0 failed / 3 ignored | 572 s |
| census parity (integration) | 16 passed / 0 failed / 4 ignored — the 3 heavy legs are declared diagnostic probes | 147 s |
| Python bindings (pytest) | 269 passed / 0 failed | 525 s |
| Alethe checker suite | 16 passed / 0 failed | 243 s |
| per-instruction validation demo | V=37 / R=0 / N=3 of 40 — zero Validated-to-Refuted | 50 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 (byte-identical across two full runs
each; the certificate-sweep canary via the instrumented procedure). Native bindings: 17 passed / 0 failed; the region, multi-output,
and inverse demos all PASS.

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 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) | 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 (default 30 s rung) run, 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) | 314.1 s |

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 (x2) |
| XTEA register form, B=64, 32 rounds | PROVEN (round-summarized) | 220.6 s / 181.0 s (x2) |
| XTEA gcc-form, stack-carried state, 32 rounds | PROVEN (round-summarized), 3 carriers | ~69 s |

## Documentation

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

## License

MIT (see [`LICENSE`](LICENSE)). 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**.

