test(formal): the economic SMT and register, formalized — and a vacuous theorem repaired on the way in - #785
Merged
Conversation
…g one that did not
lean4/DSMNonInterference.lean's operation_locality was vacuous. It read
theorem operation_locality (s1 s2 : PairState) (amount : Nat) :
let _ := pairCommit s1 amount
s2 = s2 := by rfl
The `let _ :=` binder is discarded, so the goal is `s2 = s2` and the proof is
`rfl`. It mentions the operation nowhere and holds for any operation whatsoever
-- yet the file header advertises it as "the mathematical core of Paper Lemma
3.1", and docs/reports/2026-04-28-formal-verification-report.md listed it among
proven theorems. It passed CI because sorry-free is not the same as non-vacuous.
The root cause is that PairState is a single pair with no notion of the others,
so "committing here does not touch there" was not expressible over it. This adds
PairWorld -- pair states indexed by relationship key -- and commitAt, which
updates exactly one key. operation_locality now states
j != k -> commitAt w k amount j = w j
with both the operation and both sides of the equation present.
Three theorems establish the repaired statement is not free:
commit_is_not_a_noop the operation CHANGES its own target, so
locality does not hold because nothing happens
commit_hits_its_own_target the target key IS the committed state; an
implementation that discarded the operation --
exactly what the old `let _ :=` did -- makes
this unprovable
distinct_pairs_do_not_interfere the paper's own form, over relKey, where
relKey_injective makes key distinctness mean
distinct unordered pairs
Mutation-controlled: dropping the j != k hypothesis leaves
`(if j = k then pairCommit (w j) amount else w j) = w j` unsolved, so the
hypothesis is load-bearing. The old theorem admitted no such control.
Also records in the header that relKey_injective is about the min/max
NORMALIZATION of an unordered pair, not about a hash -- this module contains no
hash, no SMT and no domain separation. Amendment 2c-C2 ruling G currently cites
this file as proving relationship-SMT leaf-key injectivity; that citation is
corrected separately.
Zero axiom, zero opaque, unchanged. #print axioms reports every theorem
depending only on propext. All ten modules pass `lean -DwarningAsError=true`.
347 domain tags are declared; 326 reached all_tags(). Every uniqueness and
prefix-freedom check in domain_tags/mod.rs traverses that registry, so 21 tags
were covered by nothing -- including two PRODUCTION signing domains:
DSM/add-device-admission genesis_identity/device.rs:17
DSM/add-device-self-attest genesis_identity/device.rs:22
both used by common/device_admission.rs:66,107 for §16.3 additional-device
enrolment. The remaining 19 are test/bench/trace fixtures in misc/testing.rs,
which is NOT cfg(test)-gated -- they compile into production builds and share
the one namespace, so a fixture colliding with a protocol tag would have been a
real defect that no test could see.
All 21 are now registered. Three checks replace the implicit trust:
every_declared_domain_tag_reaches_the_registry
scans the crate source INDEPENDENTLY of the TAGS arrays and compares
declared against registered as a MULTISET of tag bytes. Multiset, because
set equality absorbs a duplicate declaration or a duplicated entry --
multiplicity disappears. Bytes rather than (name, bytes), because
all_tags() returns TaggedHashDomain values and does not retain names;
all_tags() is not redesigned merely to make a CI check expressible.
The scan is source-wide rather than scoped to domain_tags/, since nothing
constrains a declaration to that directory and scoping it there would make
the guard depend on the convention it exists to enforce. Both declaration
forms in the tree are matched: tagged_domain! and from_static.
declared_domain_tag_constant_names_are_unique
source-side, since the registry carries no names.
the_declared_domain_tag_count_is_the_expected_one
EXPECTED_TAG_COUNT = 347, a consciously-bumped change-control tripwire --
the same idiom as the CI Lean gate's hardcoded module count. Explicitly
NOT a completeness guard.
the_domains_a_proof_depends_on_are_registered
the eight economic-SMT domains plus the two add-device signing domains,
asserted present by name. The economic-SMT separation proof reduces its
cross-domain obligations to "these tags are pairwise distinct", and that
premise is only as strong as the registry the distinctness test walks.
Mutation-controlled twice. Unregistering DSM/add-device-admission reddens the
completeness guard with the offending tag named. More importantly, DECLARING a
new tag and forgetting the array -- the case a count provably cannot catch,
since the registry still holds 347 -- leaves the count test GREEN and reddens
only the completeness guard:
the_declared_domain_tag_count_is_the_expected_one ... ok
every_declared_domain_tag_reaches_the_registry ... FAILED
declared domain tags that never reach all_tags(): ["DSM/mutation-probe"]
That is the class of bug the previous arrangement admitted, and it is why the
count is the weakest of the three rather than the guard.
The two economic register read endpoints stamped neither the register
incarnation nor an asserted absence, so on the live path NO economic read was
countable and every one degraded to Unavailable.
The client requires two axes to attribute an answer -- answer_counts_for
(dsm_sdk/src/sdk/storage_node_sdk.rs:663-669) counts a member only when the
echoed node id AND the echoed register incarnation both match the member the
vault committed -- and counts a 404 as an absence only when the response
asserts `x-dsm-slot-outcome: absent` (:1072-1082). The blanket layer supplies
the node id; nothing supplied the incarnation, and Ok(None) answered with a
bare 404.
The consequence composes with two further call sites into exactly the collapse
amendment 2c-C2 forbids:
every economic read -> Unavailable
-> read_cell_quorum's Unavailable => Ok(None) economic_registers.rs:232
-> winning_faucet_ticket's .ok().flatten() peer_lineage.rs:165-169
-> the verifier sees EMPTINESS
A quorum-unavailable read delivered as emptiness is the precise failure the
four-valued observation exists to prevent.
api/economic/mod.rs gains cell_read_response, which stamps the incarnation on
EVERY branch and asserts the absence on the empty one. Stamping only the held
case would leave the dangerous one -- a rebuilt member reporting emptiness --
indistinguishable from the real member reporting it, which is the whole reason
the second axis exists. A 500 carries the incarnation but asserts no outcome: a
failure is not an absence.
The incarnation comes from state.own_register_incarnation, set unconditionally
at main.rs:541 from the same DB value that builds the storage set at :553, and
NodeStorageSet::new refuses a mismatch (lib.rs:92) -- so the two sources agree
by construction and this one is present even when no set is configured.
Tests assert both branches on both registers, and both test_state helpers now
record the incarnation so every existing test's answers are countable too.
Mutation-controlled with the two realistic slips, each reddening the named test
at the exact assertion:
stamp only the held branch -> FAILED at the absent-branch incarnation
drop the absence assertion -> FAILED at the slot-outcome assertion
(Removing the stamp outright is a COMPILE error, since the crate is
#![deny(warnings)] and `state` goes unused -- a stronger signal, but not
evidence the test catches a realistic regression, which is why both mutations
above keep the code compiling.)
Clippy in this crate goes 117 errors -> 75: the two economic test modules never
carried the `disallowed_methods` allow that api/vault/settlement_slot.rs:237
has, and adding it for the new tests also covers the pre-existing test code.
278 dsm_storage_node lib tests pass; fmt clean.
…ons named and local
Discharges amendment 2c-C2 ruling G. lean4/ and tla/ contained ZERO references
to the economic tree; this is a THIRD tree, with a distinct leaf-key family, a
distinct node domain, and an all-zero ABSENT_LEAF that is the deliberate
opposite of the modelled one. 64 theorems, zero axiom, zero opaque, no Mathlib,
no imports -- matching every other module in the tree.
Three layers, and the separation between them IS the honesty claim:
§1-2 byte layer real byte lists, real tag literals 0 assumptions
§3-10 symbolic layer free term algebra over the encoder the abstraction
is declared, not
hidden
§11 adequacy bridge the only place cryptography appears LOCAL hypotheses
THE STRUCTURAL SPINE. Tags are NUL-free by type and the encoder appends exactly
one 0x00, so the first NUL sits at len(tag) and the (tag, message) split is
unique FOR ARBITRARY MESSAGES. This is stated as INJECTIVITY IN (tag, message)
and disjoint preimage spaces -- deliberately NOT called "prefix-freedom", which
it is not in either direction: `DSM/x||00||a` IS a prefix of `DSM/x||00||ab`,
and `DSM/foo` / `DSM/foo/bar` are both NUL-free with one a prefix of the other.
Literal tag prefix-freedom is a separate hygiene property with its own Rust test.
Obligations 2/3/4 then reduce to pairwise tag distinctness, DECIDED by the
kernel over the verbatim Rust tag literals. Mutation-checked: making smtNode's
tag collide with smtLeaf's fails the build with
Tactic `decide` proved that the proposition
¬EconDomain.smtLeaf.tag = EconDomain.smtNode.tag
is false
OBLIGATION 1 GETS A BYTE-LAYER BRIDGE. In a free term algebra, same-domain
injectivity holds because CONSTRUCTORS are injective -- which says nothing about
whether the real byte grammar maps distinct declared inputs to distinct message
bytes. Four per-key lemmas close that gap from fixed-width fields alone, so a
key collision requires a hash collision rather than an ambiguous concatenation.
THE HASH ASSUMPTIONS ARE SPLIT AND LOCAL. A single global "injective Digest ->
bytes" is stronger than collision resistance AND silently re-absorbs the
zero-sentinel assumption the inductive datatype was chosen to expose, because
absent maps to 0^256. Kept apart:
digest_width definitional; PROVED (encodeDigs_length), not assumed
h_collision_xy for the CONCRETE preimages of a statement
h_not_absent_x for a CONCRETE populated preimage
Neither is global. A universal "distinct preimages give distinct 256-bit
outputs" would be FALSE, not merely unproven -- collisions necessarily exist by
pigeonhole. And "no populated economic preimage produces 0^256" is not implied
by preimage resistance, which speaks to infeasibility of FINDING one.
`global_injectivity_would_smuggle_in_the_zero_claim` exhibits the conflation so
the decision to split is visible rather than accidental.
THREE CORRECTIONS TO RULING G, all recorded in the module header:
* Obligation 4 presupposes a root domain that does not exist.
empty_economic_root() = default_node(256) and every non-empty root is an
econ_node output, so node and root are ONE domain --
root_lives_in_the_node_domain proves it. A model separating them would
prove something false.
* The leaf-state domain is missing from ruling G's list but is step 2 of the
frozen five-step chain; it is included in the disjointness set.
* Obligation 1's input domain is not closed for settlement-receipt and
consumed-source, whose receipt_id and source_id are themselves domain
hashes. Injectivity is stated relative to the declared 32-byte inputs.
OBLIGATION 6 REACHES THE TREE. A map-level frame condition alone could be proved
for a standalone Map with no connection to R_econ -- repairing one vacuous
theorem and introducing a subtler one. All four layers are present: map
(frame + own-key hit), tree (fold_path_injective: a root plus its direction bits
determines the leaf AND every off-path sibling), canonicality, and anti-vacuity
witnesses that an update actually changes the root.
Obligation 7 is stated over QUALIFYING quorums (at least q), which is what the
protocol deals with; exact-q is kept as the underlying lemma. The predicate form
needs no Nodup to PROVE -- predicates cannot inflate their own cardinality -- but
carries members.Nodup as a `_`-prefixed hypothesis, the house signal for
not-load-bearing-in-the-proof, because it is what licenses reading S.length as
the number of DISTINCT members. Without it the lemma stays true and n stops
denoting membership.
#print axioms on every headline theorem reports only Lean's own logical axioms
(propext, and Quot.sound for the quorum results); beta_quorum_is_canonical
depends on none. That is because the cryptographic assumptions travel in §11
signatures rather than as file-global axioms -- so their ABSENCE from §1-§10 is
a checkable fact, not a claim. The summary block says explicitly that the module
must not be reported as "axiom-free" without that qualification.
Also records a source-tree finding: economic/tree.rs:29 says "Since every
present leaf is a BLAKE3 output, all-zero is unreachable as a present value."
The conclusion does not follow -- being a BLAKE3 output is what makes all-zero
POSSIBLE; preimage resistance is what makes it unreachable in practice. The
construction is fine; the comment asserts a theorem where an assumption belongs.
CI's hardcoded lean4/ module count moves 10 -> 11, the intended tripwire. All
eleven modules pass `lean -DwarningAsError=true`, which is the sorry check --
and, as the plan anticipated, also makes linter warnings fatal.
…failures finally gated
Models the BEHAVIOURAL half of the frozen observe_cell semantics: the write-once
economic register read while claimants are concurrently writing, members are
failing, and members are REBUILDING their registers.
The algebraic half -- canonical quorum, and 2q > n forcing any two qualifying
quorums to intersect -- is a universal statement over all n and stays in
lean4/DSMEconomicSmtSeparation.lean §10. Neither restates the other. Quorum is a
CONSTANT here, exactly as observe_cell takes it as an argument, and there is
deliberately NO operator computing a quorum from Cardinality(Member): a local
majority-of-catalog rule is the verifier's opinion, not the vault's.
What TLC uniquely buys is the ROUND -- what can happen to the register between
sampling one member and the next. NoEmptyAtQuorumAfterClaimed is the statement
only a model checker can make: a cell observed Claimed is never later observed
empty, across every interleaving of claims, outages and rebuilds. observe_cell
applied to one fixed list of reads is a pure function and is Lean's business.
Faithful config: 2,021,284 states, 135,349 distinct, depth 14, no error.
EXPECTED-TO-FAIL CONFIGS ARE NOW MACHINE-GATED. Previously the guarded family
shipped two configs asserted to fail in a README table, and nothing checked it.
TlaSpec gains expect_violation: Option<String>, and run_all inverts the verdict
-- the run passes only if TLC reports EXACTLY the named invariant. Three ways to
fail: no violation at all (the invariant is decoration), the wrong invariant
(the config is not modelling what it claims), or a TLC error.
Five falsifications, each modelling a real shipped defect:
_FlattenCollapse peer_lineage.rs:165-169 .ok().flatten()
-> EmptinessIsGrounded
_UnavailableIsNone economic_registers.rs:232 Unavailable => Ok(None)
-> EmptinessIsGrounded
_ErrorIsEmpty an unusable answer classified as "no value", the
historical defect cell_observation.rs exists to remove
-> EmptyAtQuorumIsWitnessed
_NoIncarnationEcho attribution on node id alone -- the live economic read
path before the incarnation header was stamped
-> EmptyAtQuorumIsWitnessed
_Reachability NON-VACUITY: Conflict must be REACHABLE from two
claimants racing one write-once cell, with no
misbehaviour at all. Without it the four above could
pass for the wrong reason
-> ConflictUnreachable
_NoIncarnationEcho violates EmptyAtQuorumIsWitnessed rather than
NoEmptyAtQuorumAfterClaimed: dropping the incarnation requirement makes a
rebuilt member's absence count as attributable when ground truth says it is not,
so the witnessed check fires first. Recorded as observed, not as predicted.
The gate machinery is itself mutation-controlled. Neutering _FlattenCollapse
back to the faithful consumer makes tla-check report
FAILED [expected-to-fail] (2021284 states, 135349 distinct, depth 14)
ERROR: falsification config must violate EmptinessIsGrounded,
but saw no violation at all -- the invariant is decoration
`cargo run -p dsm_vertical_validation -- tla-check`: all 13 specs PASSED.
…o of its obligations were wrong
Amendment 2c-C2's ruling G cited lean4/DSMNonInterference.lean as proving
"leaf-key injectivity for the relationship SMT". It does not. relKey is a
min/max sort of two naturals and relKey_injective proves that sorting an
unordered pair is injective; the file contains no hash, no SMT, no domain
separation and zero axioms. A reader following that sentence would have been
misled about both trees -- believing the relationship tree covered, and
believing the economic obligations had a template that did not exist.
Two of the obligations were also wrong as written, found while discharging them:
Obligation 4 presupposes a ROOT domain that does not exist.
empty_economic_root() = default_node(256) and every non-empty root is an
econ_node output, so node and root are ONE domain. The Lean module proves
that rather than asserting it; a model separating them would prove
something false. The real content is node vs leaf vs leaf-state.
The leaf-state domain DSM/economic-leaf-state/v1 is absent from the list but
is step 2 of the frozen five-step chain, so it belongs in the disjointness
set. Now included.
Plus one scoping caveat: obligation 1's input domain is not closed for the
settlement-receipt and consumed-source keys, whose receipt_id and source_id are
themselves domain hashes. Injectivity is discharged relative to the DECLARED
32-byte inputs; the nested derivations are a recorded dependency.
Status moves from "claims NO model coverage" to discharged, and the claim
boundary is stated in ruling G, in tla/PROOF_CLAIMS.md alongside the existing
boundaries, and in the verification report:
Formal coverage establishes the stated properties of the normative
economic-SMT and economic-register MODELS. It does NOT constitute a
machine-checked refinement proof that the shipping Rust implements those
models. Implementation correspondence is supported separately by
conformance vectors, source-level invariants, tests, and deliberate
falsification controls.
And the Lean module is explicitly NOT reported as axiom-free without
qualification. The quorum results are; the hash and non-aliasing results rest on
the symbolic abstraction declared in the module header, with the adequacy bridge
resting on a LOCAL collision hypothesis and, for the zero-sentinel obligation
only, a LOCAL preimage hypothesis. Neither is a global claim about BLAKE3: a
universal "distinct preimages give distinct 256-bit outputs" is FALSE by
pigeonhole over a 256-bit codomain, and "no populated economic preimage produces
the all-zero digest" is not implied by preimage resistance, which speaks only to
the infeasibility of FINDING one.
Documentation only.
… one does not The domain-tag source scanner tripped clippy::sliced_string_as_bytes and clippy::unnecessary_to_owned under `rustup run 1.98.0 cargo clippy --all-targets -- -D warnings`, which is what `make lint` runs. Recorded because the miss is instructive: `cargo clippy -p dsm` on the DEFAULT toolchain reported clean, and both lints only fire on the pin. Verifying a lint on whatever toolchain happens to be active is not verifying the gate -- the same shape as running a filtered test subset and calling it the board.
…unreachable by hashing
economic/tree.rs said:
Since every present leaf is a BLAKE3 output, all-zero is unreachable as a
present value.
The conclusion does not follow from the premise. Being a BLAKE3 output is
exactly what makes the all-zero digest POSSIBLE -- a fixed-width hash over an
unbounded domain has preimages of every value. What makes it unreachable in
practice is preimage resistance, which is an assumption, not a consequence of
the construction.
The comment now says ABSENT_LEAF RESERVES the all-zero digest, and that a
populated leaf could take that value only by producing a valid economic preimage
whose BLAKE3 digest is all zero -- which security treats as computationally
infeasible.
This aligns the source with the formal model's actual assumption boundary.
lean4/DSMEconomicSmtSeparation.lean draws the same line: the symbolic model puts
`absent` outside the image of the hash BY CONSTRUCTION, and the adequacy bridge
carries the byte-level claim as an explicit LOCAL hypothesis (h_not_absent_x)
rather than deriving it. Having the Rust assert a theorem while the Lean
carefully declines to would have left the two disagreeing about what is proved.
No behaviour change. The construction was never defective -- only the comment
overstated it, which is the same failure mode as the peer_lineage.rs:61-62
comment amendment 2c-C2 already records: a comment that certifies to the next
auditor something the code does not establish.
fmt and clippy clean on the pinned 1.98.0; the [`ABSENT_LEAF`] intra-doc link
resolves.
This was referenced Sep 8, 2026
cryptskii
added a commit
that referenced
this pull request
Sep 9, 2026
…ts (#786) * docs(ccb): land amendment 2c-C2's owed registry edits C2 was merged as PR #785 but its "Registry and cross-document edits" section never landed. All six of its markers returned zero against origin/main. C1's edits did land, so the asymmetry was easy to miss -- and the sentence C2 declares false was still sitting in the registry telling implementers the opposite of the ruling. Seven edits, one per obligation C2 recorded: §3.1 signature_alg 0x0001 is DSM BLAKE3-SPHINCS+-SPX256F, NOT FIPS-205 SLH-DSA-256f. The widths coincide exactly, which is what makes the substitution silent: a foreign verifier linking a standards-only SLH-DSA library gets byte-identical key and signature lengths and fails every signature with nothing to diagnose. The old closing sentence -- "the algorithm and the key bytes stand or fall together" -- is replaced; it was false as written, and false in the direction that made the substitution look safe. §2.10 BindingRecordWireV1 recorded as the ONE named non-CCB grammar, with its Class N argument and an explicit statement that it is not permission for arbitrary protobuf-derived identities. §2.11 New: the retrieval obligation. Recompute the identity over the bytes returned and compare to the address asked for, BEFORE reading any field. Consumer's obligation, never the fetcher's. Must be discharged by a single named construct, not by open-coding. §15.3 Reconciled in §2.11: Rev 15's H(N ‖ P) names no hash function, has no separator and no length discipline, so it is not injective in N. The frozen form is H_dom(N, P). Injectivity is a property of the NUL-free tag AND the separator together -- the separator alone would push the same ambiguity one byte deeper -- so §2.9's NUL-free condition is cited, not assumed. §3.2 New: normative network parameters. The dsm-testnet root-register profile -- three (member_id, register_incarnation_id) pairs, n = 3, q = 2, and the derived storage_set_id. A network absent from the table is unknown, not permissive. §5.2 Cross-references §3.2, so the frozen element encoding and the values instantiating it can be read against each other. §7 2c-C2 bullet added and marked WRITTEN, recording that authenticated retrieval is frozen as a rule and NOT met by the implementation. The decomposition's "P0-P6" citation is corrected to the authority-resolver contract; C2 ruling A declines to elevate P0-P6 into a SoFi interface. §4's counts do not move: framework and namespace content only, no field table added, changed or burned. Documentation only. Prerequisite for 2c-C3, which cites the registry. * docs(sofi): amendment 2c-C3 — freeze ValidDlvSuccessorCore C2 froze how a verifier obtains and authenticates the substrate and deliberately did not decide what makes a DLV continuation valid. C3 decides exactly that. Specification-first, on the owner's ordering: complete the read-only source reconciliation, freeze every clause, write the normative predicate, then implement. That ordering earned its keep twice -- both findings were invisible to clause-by-clause transcription and both change what the predicate must contain: - §8's Req 8.1 is a successor-validity condition, not background: "a claim is consumed at most once and its exact removal must be visible in the successor state". No earlier draft carried it. - Def 6.1's terminal close requires crediting released reserves to owner balance EXACTLY ONCE -- a property of the owner's balance, not of V_{n+1}, so no predicate over the successor can express it. Declared, owner named, explicitly not discharged. The expected "15-clause predicate" does not exist in the source. Def 6.1 is ten common checks plus kind-specific tails: sixteen items at its own granularity, ~34 atomically. FIFTEEN IS THE VaultStateV2 TUPLE ARITY AND THE REVISION NUMBER. That framing is revoked; no clause count is normative. Four Rev 15 errata corrected as exact predicates, two of which made the predicate unformulable as written: D1 the parent-reserves-digest operand does not exist -- it was part of p_v, which Req 6.6 burned. c_n commits the whole tuple. D2 Retired(V) := reserve_a = 0 ∧ reserve_b = 0. No new field; unambiguous BECAUSE market admissibility forbids a = 0, so a market successor can never zero both legs. D3 fee_t ≡ 0 in §7.1 for the beta market family. The fee stays in the reserves, so it is inside Σ R^(n+1), not subtracted from it. A verifier applying §7.1 literally REJECTS EVERY VALID BETA MARKET SUCCESSOR. D4 direction is carried nowhere and is derived from the policy- commit set equality. Total, because beta_constant_product refuses an unordered or equal pair, so the same check that establishes membership also refutes input = output. Canon(expected) = Canon(supplied) is the SINGLE AUTHORITATIVE SUCCESSOR-STATE CORRESPONDENCE test -- one conjunct, not the whole predicate. Authority, signatures, the parent relationship, binding finality and evidence validity stand alongside it. DeriveExpected is typed and partial (Derived | Invalid | Incomplete | SafetyViolation); the byte comparison happens only on the Derived arm, so failed arithmetic and unavailable evidence cannot hide inside an apparently total call. successor_ccb resolved unconditionally. canon() is encode_to_vec(), so the field IS frozen wire and IS the bundle-shape discriminator -- the opposite of the earlier draft's assumption. It is not deleted from a frozen encoding; the encoding is superseded in full, and 2c-A already prohibits it: "do not carry both the complete successor and a second independently encoded successor digest". Until that cut lands, b is computed over prost bytes, which §2.10 forbids. Recorded, not relied upon. C3 receives typed prerequisite RESULTS, not success-only facts. A component that owns INVALID / INCOMPLETE / SAFETY_VIOLATION cannot be handed only established successes; it would be blind to the outcomes it classifies. Two conjuncts are declared and undischarged -- TokenPolicyValid and the owner credit -- named so "C3 is closed" can never be read as "DLV succession is fully verified". Records the implementation debt this lands on: vault_state_composition .rs:572 binds the bundle's declared successor and discards it with `let _ = transition;`, folding its own derived next_state instead. The comparison this amendment makes normative does not exist today. Documentation only. No Rust, no proto, no tests. * test(formal): the DLV successor predicate, with its encoding hazards proved Phase C of amendment 2c-C3: definitions and theorem statements for ValidDlvSuccessorCore. Strictly additive -- new module, no existing proof touched. CI Lean count 11 -> 12. What it machine-checks: BRIDGE canonVault_injective. Canonical equality implies structural equality, so "every preserved field equals V_n" derived from a byte comparison carries no unstated assumption. Ruling B names this obligation precisely because omitting it would hide one. ENCODING The encumbrance set sits at field 10, in the MIDDLE of the tuple, so its §2.4 count prefix is load-bearing. Two genuinely different states -- one encumbered, one holding a live budget -- have byte-identical encodings without it, because the claim list borrows the presence marker's byte: no claims, β = some 0 -> [] ‖ (1 ‖ 0) = [1,0] claim [1], β = none -> [1] ‖ (0) = [1,0] A verifier comparing those bytes accepts a successor that silently converted a budget into an encumbrance. D2 market_never_derives_retired. This is the whole argument for erratum D2, formalized: admissibility forbids a = 0, so the input leg is R_in + a > 0 and at least one leg stays strictly positive. Both-zero is therefore reachable ONLY by the close family, which is what makes Retired an unambiguous marker with no new tuple field. D4 direction_refutes_equal_commitments. The set-equality check that establishes membership also refutes input = output, because token_a < token_b strictly. The derivation is total. DERIVED Preserved and mutated field equalities are obtained FROM correspondence, not checked beside it -- theorems, not acceptance conjuncts, so the independence obligation is satisfiable for them. TAXONOMY Each failing arm propagates its EXACT class and reason. Stated per constructor, because "propagates its class" is the claim that must not be approximate. One theorem was WRONG on the first pass and the compiler caught it: I had claimed correspondence's class always agrees with the derivation's class. It does not -- a successful derivation whose bytes mismatch is invalid, so the derived arm downgrades valid to invalid. That asymmetry IS the comparison's purpose. Replaced with correspondence_valid_iff_bytes_match, which states it exactly. Ruling H is formalized rather than promised: core_does_not_discharge_token_policy exhibits an input satisfying the core predicate while the complete predicate fails. The module cannot be read as claiming C3 closed a dependency it does not own. Mutation controls executed, not asserted. Both produced the strongest available result -- the kernel proving the NEGATION of a named theorem, not merely a broken proof: strip the count prefix -> canonVault_separates_the_samples proved FALSE; canonVault_injective falls back on sorryAx remove the comparison -> preserved_field_mutation_is_rejected, encumbrance_introduction_is_rejected, budget_introduction_is_rejected and market_successor_not_accepted_under_close each proved FALSE The encumbrance and budget controls matter most: beta's E is always empty and no Allocation type exists in Rust, so no beta-shaped test can exercise Req 8.1 at all. Stated at the model level or not tested anywhere. Axioms reported per theorem, never as a blanket claim. No result depends on sorryAx or Classical.choice; six depend on no axioms at all. propext and Quot.sound are Lean's logic, not assumptions added here. Gate: all 12 modules pass lean -DwarningAsError=true. * docs(sofi): correct three defects in 2c-C3 before it becomes authority A read-only survey of the Rust surface, run before any Phase D code was written, found three defects in this amendment. Two of them were confident, specific and wrong. Correcting them here rather than merging and issuing an erratum: this is the freeze point, and a normative document should not enter the record carrying a false factual claim. 1. THE PRODUCTION-DEBT STATEMENT WAS FALSE. The draft said vault_state_composition.rs:572 "binds the bundle's declared successor and discards it ... Both values are live at that point." There is no declared successor on the wire at all. successor_ccb is 32 bytes that do not commit the successor state: production market bundles write the route-set commitment x (dlv_routes.rs:3249, whose own comment says "there is no such commitment to name, so it carries the trade identity and nothing reads it as a successor"), and production closes write x_close (settlement_bind.rs:161), a pure function of (vault_id, parent_generation). Both composition arms derive the successor locally. So VDS.COMMON.10.a is not merely unimplemented -- it is UNIMPLEMENTABLE against the current encoding, and is now marked: NORMATIVE YES FORMALLY SPECIFIED YES PRODUCTION IMPLEMENTED NO BLOCKED ON the 2c-A canonical encoder cut with the exact blocker, the owning prerequisite, and what unblocks it. Blocked must not mean accepted-without: production may not report ValidDlvSuccessorCore = VALID for any path whose validity requires the conjunct until the byte comparison is actually performed. That gap is implementation status (BlockedOnCanonicalSuccessorEncoding), never a protocol reason code -- the INVALID/INCOMPLETE/SAFETY_VIOLATION taxonomy is not contaminated because a prerequisite has not landed. Also recorded: successor_ccb cannot simply be repurposed. is_close_transition derives BundleShape from exactly that field, so writing a real successor commitment into it silently reclassifies every close bundle as Market. The shape discriminator must move first, and that is 2c-A's to do. 2. RULING J NAMED THE WRONG OBSERVATION TYPE. The draft called binding_observation "C2's four-valued CellObservation, unchanged". Two distinct types exist over two distinct key spaces: CellObservation economic register cell FOUR arms BindingObservation DLV parent-binding slot FIVE arms The settle path reads the five-valued one. All five arms are now mapped normatively: Free -> INVALID NO_BINDING_ESTABLISHED BoundFinal -> proceeds to VDS.COMMON.10.a Conflict -> SAFETY_VIOLATION DUPLICATE_BINDING_FINALITY Undetermined -> INCOMPLETE BINDING_UNDETERMINED Unavailable -> INCOMPLETE BINDING_EVIDENCE_UNAVAILABLE Two of those are easy to get backwards and the defining module says so. Undetermined is neither emptiness nor forgery -- two quorums intersect, but one READ need not see the intersection, so a value chosen behind a down member lands there; reading it as Free composes past a live bind, and reading it as invalid "would make every concurrent settle permanently invalid". Free is INVALID rather than INCOMPLETE because a quorum of authenticated explicit absences is positive evidence that nothing is chosen. The Lean module was corrected first and the document follows it. Two new theorems pin the arms that invert: undetermined_is_incomplete_never_valid_never_invalid and free_is_invalid_not_incomplete. 3. THE CORRESPONDENCE CONDITION NEEDED A BYTE-LEVEL STATEMENT. Semantic successor equality and canonical-byte equality come apart here. decode_vault_state NORMALIZES rather than refuses -- StorageSetMembers::new and EncumbranceSet::new both sort, rejecting only duplicates, never bad order -- and CCB has no decode/re-encode equality check, though ~10 sibling modules apply exactly that discipline and one names it "the settlement-wire discipline". So two byte strings decode to one VaultStateV2 and a round-trip comparison launders non-canonical input. The acceptance condition is now stated as equality of canonical BYTES, with the round trip permitted only under the frozen normative encoder -- which does not exist: repo-wide there is exactly one `fn canon`, and it is protobuf. Phase D must build it. Ruling E additionally now forbids mapping a FAILED SIGNATURE to an absence, because the shipped code does it deliberately: fetch_verified_receipt discards a failed SPHINCS+ receipt verification with .ok()?, which becomes MarketRealization::Absent, breaks the fold and returns Ok(...) -- so a forged receipt is not an error at all. Its doc defends the collapse as sound about FOLDING, which it is; it is wrong about CLASSIFICATION. The amendment carries a "Corrections made before it merged" section recording all three rather than silently rewriting a circulated draft. All 12 Lean modules pass lean -DwarningAsError=true. No result depends on sorryAx or Classical.choice.
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.
Discharges amendment 2c-C2 ruling G, plus the two properties added during review — quorum intersection and observation non-collapse. Seven commits, deliberately separable.
Two things exploration changed before any proof was written
A sentence in merged ruling G was false. It cited
lean4/DSMNonInterference.leanas "proving leaf-key injectivity for the relationship SMT". It does not:relKey : Nat → Nat → Nat × Natis a min/max sort, andrelKey_injectiveproves that sorting an unordered pair is injective. That file has no hash, no SMT, no domain separation, zero axioms.And a theorem in it was vacuous.
operation_localityreadThe
let _ :=binder is discarded, so the goal iss2 = s2. It mentioned the operation nowhere and held for any operation whatsoever — yet the file header called it "the mathematical core of Paper Lemma 3.1" and the published verification report listed it among proven theorems. It passed CI because sorry-free is not the same as non-vacuous.The seven commits
lean4/DSMEconomicSmtSeparation.lean— obligations 1–7tla/DSM_EconRegisterObservation.tla— the concurrent half, expected failures gatedA.
PairStateis one pair with no notion of the others, so "committing here does not touch there" was not expressible over it. AddsPairWorldandcommitAt;operation_localitynow statesj ≠ k ⇒ commitAt w k amount j = w j. Three theorems prove it is not free, and droppinghneleaves the frame goal unsolved — a control the old theorem could never admit.B. 347 tags declared, 326 registered. Twenty-one escaped every domain-tag test, including two production signing domains —
DSM/add-device-admissionandDSM/add-device-self-attest(§16.3 device enrolment). Three checks now, proving three different things: a source-wide multiset comparison of declared against registered (the load-bearing guard), a consciously-bumped count tripwire, and membership assertions for the ten domains the proof's premise rests on.The decisive control is the case a count provably cannot catch — declare a tag, forget the array:
C. The economic read endpoints stamped neither the register incarnation nor an asserted absence. Since
answer_counts_forneeds both echo halves, every economic read on the live path was uncountable — and the two defects compose into exactly the collapse the amendment forbids:Fixed, tested on both branches of both registers, and mutation-controlled with the two realistic slips.
D. 64 theorems, zero
axiom, zeroopaque, no Mathlib. Three layers, and the separation between them is the honesty claim: a byte layer assuming nothing, a symbolic layer whose abstraction is declared rather than hidden, and an adequacy bridge that is the only place cryptography appears.DSM/x‖00‖ais a prefix ofDSM/x‖00‖ab, andDSM/foo/DSM/foo/barare both NUL-free with one a prefix of the other.decideproved that the proposition ¬EconDomain.smtLeaf.tag = EconDomain.smtNode.tag is false".E. Faithful config: 2,021,284 states, 135,349 distinct, depth 14. Five falsifications, each modelling a real shipped defect and machine-gated on the invariant it must violate —
TlaSpec::expect_violationinverts the verdict. Previously the guarded family's expected failures were asserted in a README and checked by nobody. Neutering one now reports:Corrections to ruling G's obligations, found while discharging them
empty_economic_root() = default_node(256)and every non-empty root is anecon_nodeoutput — node and root are one domain. The module proves that rather than asserting it; a model separating them would prove something false.receipt_idandsource_idare themselves domain hashes. Discharged relative to the declared 32-byte inputs.The claim boundary
And the Lean module is not reported as "axiom-free" without qualification: the quorum results are; the rest rest on the declared symbolic abstraction and, in the bridge, on local hypotheses.
#print axiomsreports onlypropext(andQuot.soundfor quorum) precisely because the crypto assumptions travel in signatures rather than as file-global axioms — so their absence from the earlier sections is a checkable fact.Verification
lean -DwarningAsError=trueon all 11 modules, count matches the bumped CI expectation. That flag is the sorry check, and it also makes linter warnings fatal.cargo run -p dsm_vertical_validation -- tla-check: all 13 specs PASSED, including the five expected-to-fail.cargo test --locked --workspace --exclude dsm_storage_node --release: 4,074 passed, 0 failed across 76 test binaries (dsmlib 1743,dsm_sdk1855).dsm_storage_node(excluded from the board) — 278 passed, 0 failed.cargo fmt --all --checkandcargo clippy --all-targets -- -D warningson the pinned 1.98.0, both clean. Commit G exists because the default toolchain missed two lints the pin catches; verifying on whatever toolchain is active is not verifying the gate.Also records a source-tree finding:
economic/tree.rs:29says "Since every present leaf is a BLAKE3 output, all-zero is unreachable as a present value." The conclusion does not follow — being a BLAKE3 output is what makes all-zero possible; preimage resistance is what makes it unreachable in practice. The construction is fine; the comment asserts a theorem where an assumption belongs.