formal(dlv): binding value continuity — the temporal property the binding register does not enforce

[cryptskii]

What

One new Lean module, lean4/DSMBindingValueContinuity.lean, plus the Lean gate count. No Rust changes.

A raw-transport probe on 2026-09-15 showed that a chosen binding value can be replaced. An honest client drove A to Committed; a second registered client then bypassed QuorumBind entirely — no prepare, no adoption of the accepted value — read the records, built a different value at a strictly higher round under its own proposer id, and issued raw CompareExchangeMany to every member. Applied 3/3. Honest Class K then reported BoundFinal on the attacker's value.

This module states the property that violates, and proves the violation:

Chosen(K, A, t1) and Chosen(K, B, t2) with t1 < t2  =>  A = B

Why it is a new theorem and not a broken one

DSMLineageQuarantine.one_read_cannot_show_two_chosen_values is a snapshot property — two strict-majority sets cannot be disjoint within one read — and it remains correct. The attack establishes A, then establishes B at a later time. The gap is temporal. To keep the two from ever being confused, this module re-proves the snapshot property in its own model alongside the counterexample.

What it contains

• applyCas — the shipped member-side rule: byte-identical replay is idempotent; otherwise the caller must still hold exactly what it expected and supersede it with a strictly greater round; then any value is written. That last omission is the defect.
• a_higher_round_raw_cas_can_choose_a_different_value — the counterexample, by computation.
• one_read_cannot_show_two_chosen_values — the snapshot property, preserved.
• ValueContinuity — a definition, not a theorem. No mechanism enforces it yet, and an unproved target is an obligation, never a stubbed proof.

Faithfulness to the shipped code: roundLt is lexicographic counter-then-proposer, matching the derived Ord whose own comment calls that field order load-bearing; chosen mirrors the documented rule that q members hold ACCEPTED at one exact round.

Verification

• lean -DwarningAsError=true lean4/DSMBindingValueContinuity.lean — exit 0.
• Axiom report, per theorem: the three concrete runs depend on no axioms; the general statements only on core propext / Quot.sound. No sorryAx.
• Mutation control, executed: restricting the higher-round branch to require prior.value = replacement.value makes the kernel prove both counterexample theorems FALSE — the strongest grade, not merely a broken proof. Reverted from a byte copy, cmp clean, recompiled.
• Lean gate expected=23 -> 24, matching ls lean4/*.lean | wc -l.

Scope

No repair is proposed here. The mechanism is deliberately kept out so a partial fix cannot narrow the defect, and the storage node stays application-blind either way.