docs: propose and exercise the v0 semantic architecture - #27
Draft
0xwonj wants to merge 18 commits into
Draft
Conversation
The coverage tool measured whether a witness reaches the boundaries an invariant claims, and reported closure on that alone. Reaching a boundary is mechanical; deciding that reaching it discharges a stated requirement is a judgment, and the tool had nowhere to record that judgment or check it. F-06 asks for a semantically inert permutation or field to be removed or justified. It was filed as closed on `logup:derived-anchors`, whose test asserts that an authored anchor may not diverge from derived material. That is a derived-stays-derived property, so the boundary now sits under X-02, where it belongs, and F-06 is open: no witness permutes an identity-bearing collection. Quoting each invariant's required pressure next to the boundaries claimed to deliver it made two more mismatches readable. F-01 asks for two independent implementations and gets one, on a finite-field algebra profile rather than a rotated regime. F-05 asks for stored bytes, peak structure, memory, and work; the guards witness measures node count and work. Both now state the shortfall and are held to partial. Verification: witnesses 160 tests OK; FRI and Schnorr --check reproduce their frozen identities; ruff clean; public tree guard clean. Coverage moves from 19 closed / 0 partial / 1 open to 16 closed / 3 partial / 2 open of 21 tracked.
The guards witness claimed to answer whether a canonical guard is cheap by measuring "real/adversarial node and work measurements". It measured nodes. `robdd_size` recursed over every assignment and memoised each node on the function it denotes. That yields the correct reduced node count, but it visits 2^|order| leaves whatever the diagram looks like, so both orders cost the same to build: 65536 predicate evaluations and ~0.085s each at eight pairs, for diagrams of 18 and 512 nodes. A cost model whose cost does not vary with the representation says nothing about the representation, and the figure this witness has been cited for — 2n+2 against 2^n — is two node counts. The diagram is now built the way an implementation builds one: from guard syntax, by `apply` over a unique table with memoisation on operand node pairs. Work then tracks structure. The interleaved order costs exactly n^2 expansions and the separated order more than doubles at every step, so the two separate in work as well as in size, and the gap widens with scale instead of holding at a constant factor. Two further defects the rewrite exposed. The declared default bound never bound anything: MAX_GUARD_NODES was 512, the separated diagram at eight pairs is exactly 512, and the comparison is `>`, so every refusal the witness demonstrated came from an ad-hoc narrower profile invented in the test. The default is now 256 and is shown refusing the adversarial case. And the corpus admits two atom kinds while only `BooleanAtom` was exercised; `FiniteValueEquals` is modelled, because it is the kind whose encoding makes the variable count depend on declared domain size. Work is bounded separately from size, at its own boundary, because a bound on one does not bound the other. Verification: 22 guard tests, up from 7, including exhaustive checks that the diagram denotes its formula under both orders; all six witnesses OK; FRI and Schnorr --check reproduce their frozen identities; ruff and tree guard clean. The guards probe moves from 1 negative to 3. F-05 stays partial: stored bytes and memory are still unmeasured, and the guards are still the textbook separating family rather than a corpus of real ones.
`check_relation_honest_prover_correspondence` pairs an admitted relation with an admitted Core and the honest prover contract over it. It carries five named codes and a real affirmative, and it had zero callers anywhere in the repository — no test, no self-check, no report case. Unreached source reads as coverage from the outside while establishing nothing. It is the only place in this witness where a relation and a Core are held against each other, so its absence is what made the relation half of the Relation/Protocol pair the only half that executed. Six tests now drive it, including one that keeps the two judgments apart by disagreement rather than by assertion: the canonical pair corresponds while a perturbed witness assignment fails satisfaction. Every field of the correspondence is shown load-bearing by perturbing each in turn. The report layer omitted this law for the same reason it had no callers, so the frozen oracle gains four cases and rotates. The outcome, boundary, and code of each were predicted from reading the law and then confirmed against the run; the digests are machine-derived, as they must be. All twelve pre-existing cases are asserted unchanged, so the rotation is growth rather than a changed judgment. R-07 gains the exact-law boundary and states what it still does not reach: Protocol acceptance, soundness direction, completeness direction, and full equivalence are not exercised, so it is partial rather than closed. Verification: 40 Schnorr tests, up from 34; all six witnesses OK; FRI and Schnorr --check pass; ruff and tree guard clean. Coverage moves to 15 closed / 4 partial / 2 open of 21 tracked.
A witness declares boundaries and codes in source. Whether any input drives them
is a separate question, and nobody had asked it. Two judgments in the Schnorr
witness were found today carrying five named codes and a real affirmative with
no caller anywhere in the repository — coverage from outside, establishing
nothing.
This answers the question by running rather than reading. It wraps the result
type each witness builds its judgments through, runs that witness's own suite
and its report layer where it has one, and compares the codes that were actually
carried by a constructed result against the codes its sources declare.
The first measurement:
witness declared fired unreachable
r2-p01-schnorr 270 77 193
r2-p02-commitment 27 11 16
r2-p03-logup 24 16 8
r2-p04-bridges 16 15 1
r2-p05-guards 4 4 0
r2-protocol-model 225 79 146
566 202 364 (36% reached)
Unreachable codes cluster rather than scatter, so the count is grouped by the
module declaring them: `execution.py` accounts for 150 of the 364 across the two
largest witnesses, and it is also where three of the five known dead judgments
live. The small recent witnesses reach nearly everything they declare; the large
early ones reach about a third.
An unreachable code is not automatically a defect — a witness may declare a
refusal for an input its fixtures cannot yet build. Not knowing which ones those
are is the defect.
Two measurement bugs were found while building it and are recorded in the source:
requiring a letter after the code prefix reported three witnesses as declaring no
codes while they were plainly firing them, and counting only the test suite would
have reported report-only judgments as unreachable.
…es suggest Every mapping in the tool was re-read against the invariant's quoted pressure, one auditor and one adversary per entry. Of eighteen, two were sound. R-06 joins F-06 as filed against the wrong property. It asks that PIR distinguish relation Witness occurrences from confidential Context, ProtocolValue, and internal obligation outputs. Its claimed boundaries refuse an operand that names a foreign parent — referential binding between admission layers. No witness models the Witness/Context/ProtocolValue vocabulary at all, so the boundaries are cleared and the invariant is open. Twelve more were overstated: the right property, with conjuncts of the pressure clause undelivered. The pattern repeats — a single boundary claimed for a clause demanding several distinct mutations. F-03 claims algorithm closure on two name checks that a sampler is cited and supported; nothing encodes a value or steps a sampler, so no round-trip runs. R-04 claims lossless bridge laws on a boundary that checks which obligations each lane declares; no bridge carries an executable map, so neither round trip is driven. R-03 has no position mutation and its evaluation-order rule cannot be made to fire. R-08's two boundaries both refuse inside admit_core, so neither operand was ever admitted, which is the layered case the pressure actually names. Two were understated, and F-05 gains the boundaries it had earned. Each entry now carries the shortfall as prose next to the quoted requirement, so the judgment is where a reader can check it rather than implied by a boundary name. The tool still cannot mechanize that pairing and still says so. Verification: all six witnesses OK; FRI and Schnorr --check reproduce their frozen identities; ruff and tree guard clean. Coverage moves from 16 closed / 3 partial / 2 open to 3 closed / 15 partial / 3 open of 21 tracked. The number fell because it stopped counting boundary names as evidence.
No composed protocol had ever been projected. The reason was structural rather than deliberate: composition leaves its operands in the module beside the composite, this fixture's producer only exports a claim, and pir-project walks every seal in the module — so projecting a composite refused at zkc-E234 for an empty verifier face on a protocol nobody asked to project. The pass gains a `protocol` option naming which seal to project. It is a development adapter over the projection boundary, and selecting one protocol out of a module holding several is what the link workflow creates a need for. With that, the composition-context question becomes answerable by running something. When a composite's consumer derives a challenge, does the producer's material influence it? The three answers — carry the whole lineage, carry a smaller domain identifier, exclude provenance — differ in whether a proof for one composite replays inside another. The answer is not in the domain string. Link renames the coins `left.producer.challenge` and `right.consumer.challenge`, and those prefixes are positional: they would read the same whichever producer had been linked. The answer is in the sponge, and the new test follows it by SSA value across the segment seam. The producer's squeeze result is absorbed into the state the consumer's own values extend, and the consumer's squeeze consumes exactly that state. Nothing resets at the boundary. It is written as a falsifier and it fails in a reachable world: a link that opened the consumer's segment from a fresh sponge, which is what excluding provenance looks like once implemented, would absorb into an initial state instead. Verified by breaking exactly that capture, which fails this test and no other. Verification: check-zkc 171 tests, up from 170, all passing; unit tests clean; public tree guard clean.
The ledger asked whether a selection had an executable inhabitant. Read literally that admits one inhabitant, which all fifteen registered rows already have, so it filtered nothing. The stronger unwritten reading — build every alternative and compare — was tested against this repository and failed in both directions. Not sufficient: composition context has all three alternatives inhabited by running code and stays incomparable, because nothing carries a composition context at the moment a challenge is derived, so the dimension never varies. Not necessary: four alternatives are unrepresentable because a shipped refusal makes them so, and inhabiting those means deleting a guarantee to measure the hole, where the refusing code is already the argument. Meanwhile the failure that actually occurred, four times in one day, was a real artifact sitting adjacent to a claimed property and counted as it. An invariant filed closed on a boundary testing something else. A guard witness reporting diagram size as build work, both orders costing 65536 predicate evaluations for diagrams differing 28-fold. A witness-surface invariant closed by an identity-equality check. Building more alternatives produces more of these. So each row now names what would show the selection wrong, and whether that has been run. A falsifier that cannot fail is worse than none because it reports success, so every row states the wrong result and why a reachable state produces it. Rows are tiered: uncontested closes on the falsifier plus a costed rejection with no rival built; contested owes the rival and a shared substrate where one input drives both and the outcome can differ. Section 7 grows from fifteen rows to thirty-four. The nineteen additions were already load-bearing selections carrying no row — nine of them in pir/protocol-model.md alone, and two in analysis/, where the ledger had registered nothing at all. Registering them did not create the work; it made work already being relied upon visible. Seventeen of the nineteen drafted falsifiers failed adversarial attack before landing: nine could not reach their failing outcome, three were vacuous, three restated the decision, two named a task instead of an observation. That rate is the reason the attack step is part of writing a row rather than a review of one. Statement scope's clause is read as a conjunction. A single Sigma protocol fixes its statement up front and cannot exhibit a later introduction at all, so only sequential composition exercises what that row is about. Verification: check-zkc 171 tests passing; ruff clean; public tree guard clean; no absolute paths, private references, or internal shorthand in the tracked text.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This draft presents the research-stage v0 semantic redesign, its durable target documents, and the executable witnesses and falsifiers used to pressure-test the model. The existing
docs/authority map remains controlling; nothing indocs-next/changes current product semantics, support, or release status.Research review contract
The primary review surface is:
docs-next/project/;docs-next/pir/,relations/,analysis/, andcompiler/;foundation/,oir/,realization/, andevidence/; andevaluation/, plus the bounded composed-protocol projection change and its lit test.docs-next/notes/is an optional, non-authoritative research appendix. It preserves source research, rejected alternatives, pressure tests, failed snapshots, and decision history. Reviewers are not expected to read it sequentially or exhaustively. Consult it when a durable decision lacks clear rationale, an alternative appears omitted, a claim needs its source or falsification trail, or a durable page may have failed to absorb an important qualification.A note does not repair a missing definition in a durable document. Findings should be stated against the durable owner, implementation, or executable evidence; notes may be cited as supporting context. Review the current HEAD as the selected snapshot rather than treating intermediate commits as current design states.
Merge gate
This PR is intentionally a draft and is not merge-ready. Before squash merge, all still-needed conclusions and rationale must be absorbed into their durable owners,
docs-next/notes/and its remaining references must be removed, the manifest and navigation must be reconciled, and the final checks must be rerun.Verification
cmake --build --preset ci --target check-zkc: 171/171 lit tests and all 50 C++ unit cases passed (8 encoding, 11 registry, 13 relation, 18 soundness).evaluation/r2-protocol-model: 39/39 tests and the source-bound report runner passed.evaluation/r2-p01-schnorr: 69/69 tests and the exact public report replay passed.Decisions