Architecture notes

Why the code is shaped the way it is. Written for someone deciding whether to build on it.

Eleven repositories, not one

Each tool is independently installable, independently versioned, and depends on as little as possible. pqc-sizes and pqc-mfb have zero runtime dependencies; the MCP server implements JSON-RPC directly rather than pulling a framework.

The cost is duplication — the SARIF emitters in pqc-sizes and pqc-mfb are separate — and that is accepted deliberately. Sharing them would mean one package depending on another, which would break the zero-dependency property that makes them safe to drop into a constrained environment.

Compute is separated from presentation

Window.explain() returns one unbroken string. The MCP server embeds it in JSON, the GitHub Action in an annotation, the Space in Markdown — none of which want hard line breaks. Wrapping happens at print time in the CLI and nowhere else.

The Hugging Face Space follows the same split: logic.py imports no Gradio and is unit-tested headlessly; app.py is presentation only. A Space exercised only by clicking it in a browser is an untested Space.

Caching is keyed on file identity

load_cases() caches on (path, mtime, size) — never on the path alone. A cache keyed on path would serve a stale corpus after the dataset is regenerated, and the scorer would report confident numbers for data that no longer exists on disk. Nothing in the output would look unusual.

The function returns a fresh list each call so a caller mutating the result cannot corrupt the shared copy. That copy costs ~0.3 µs against a ~900 µs parse.

A cache attempt that failed: the taxonomy was first cached with an lru_cache keyed on the tuple of 322 frozen dataclasses. Hashing all eight fields of all 322 on every lookup cost about what it saved. Re-keying on file identity produced the actual 6.5× speedup.

Refusal is a first-class outcome

Exit code 3 means "the tool could not earn an answer" and is distinct from both success and failure. Four tools use it. Every instance exists because a confident wrong answer was shipped first and then found:

Tool	Refuses when	Because
farkas-check	arithmetic would overflow	it reported a false implication as VALID
farkas-check	the goal has all-zero coefficients	verifying 0 ≤ d proves nothing
pqc-mfb	any case is unanswered	{} once scored PASS
pqc-sizes-js	a value exceeds 2^53	it overstated safe concurrency

Verifiers assert verdicts, not exit codes

Yosys exits 0 whether it proves a property or refutes it. Lean exits 0 with a warning when a proof is admitted by sorry. So both verify.sh scripts parse output text and assert the expected verdict per proof — and in the RTL case, two of those expectations are "a counterexample must exist".

Both scripts have CI jobs that plant a defect and require the verifier to catch it. Those jobs also assert the suite is green before mutating, because the first version passed whenever the verifier failed for any reason at all.

Documentation is executable

tools/check_readme_examples.py extracts every $ command from every README, TUTORIAL and dataset card, runs it in the package directory, and diffs the output against the transcript beneath it. Only an allowlist of read-only local commands runs; pip install and npm publish are reported as skipped.

A README showing stale output is a promise the code no longer keeps, and no ordinary test suite catches it.

Three checks of one bound

Layer	System	Trusted base
Mathematics	Lean 4	the kernel alone — no mathlib
Silicon	Yosys k-induction	a SAT solver over RTL
On-device	integer C	123 auditable lines, no solver

Independent toolchains, independent failure modes. A bound only one of them believes is a bound you are trusting that toolchain for.

The moat boundary

Detection ships; repairs do not. Enforced mechanically, not by convention:

• The benchmark's public projection drops repair_mechanism, repaired_detail and repaired_held, and a test asserts they never reach the published file.
• A test calls describe_family for all 39 families plus every other MCP tool, concatenates the responses, and fails if any withheld field appears.
• The formal corpus ships names, never proof bodies; a test greps the shipped file for proof syntax.

The boundary is where it is because of a measurement: only 4 of 32 mechanisms are externally distinguishable under a replicate noise control.