docs: add bounded exhaustive model for NIP-RS manual-unread encoding - #1958
Closed
wpfleger96 wants to merge 3 commits into
Closed
docs: add bounded exhaustive model for NIP-RS manual-unread encoding#1958wpfleger96 wants to merge 3 commits into
wpfleger96 wants to merge 3 commits into
Conversation
wpfleger96
force-pushed
the
duncan/nip-rs-unread-model
branch
3 times, most recently
from
July 17, 2026 18:58
56e5c8a to
62f97c2
Compare
…d model Replaces delete-on-dominance compaction with a tombstone-floor rule (RegB(0, max(S,C), 0)) so dead/dominated registers never lose the counter ceiling that blocks stale-replay resurrection; only virgin (never-set) registers still compact to None. Adds a directed deep-history parameter cube (2,016 points) covering compact -> local set/clear counter reuse -> delayed stale delivery (single- and 2-slot-split) for the same-device replay shape, proving the tombstone floor holds where the depth-4 BFS explorer structurally cannot reach. Reworks the M4 mutant to revert to the old delete-on-dominance rule and directly reproduce Thufir's exact resurrection witness (RegB(3,0,10) -> None -> reuse -> RegB(3,2,20), override_is_set=True). Adds a collision-safe reserved-key escape (ov_/esc: prefixes) so a pre-existing opaque NIP-RS context ID cannot be misparsed as override control state, with an adversarial round-trip test. Adds a cross-device compaction-transparency check: a tombstone's counter ceiling can one-shot suppress an unrelated device's concurrent fresh set (never resurrect it, per a structural merge-monotonicity lemma over 1,728 points), recoverable by one more local action. This requalifies I5c's original "compaction never changes the semantic outcome" claim, which only holds for same-device replay of a device's own pre-compaction ancestor; NOTE.md states the narrower proven property and cites the pre-existing clear-wins false-negative tradeoff this shares with an uncompacted stale clear. Makes canonical publication mandatory rather than advisory: DeviceB.publish_blob() now canonicalizes every override against the device's own effective frontier at serialization time, unconditionally -- live unchanged (3 keys), dead folded to the tombstone floor (1 key, ov_c: only), virgin omitted (0 keys) -- regardless of whether do_compact was ever called locally first. This closes a CRITICAL found in independent review: two individually-dead but *uncompacted* published registers from different device histories could componentwise-max-merge into a live resurrection, because publication previously depended on an unstated compact-before-publish discipline. do_compact remains a separate, optional local storage-GC transition, decoupled from publication correctness. Adds test_published_merge_closure: Thufir's exact witness pair under both tie policies plus a general search over a 300-point-per-policy cube of independently-dead published states pairwise-joined in both delivery orders, including a one-hop relay-republish path for delayed/multi-hop delivery (45,074 pairs checked, 0 violations). Adds mutant M7 (publish-without-canonicalization), caught directly via the witness reproduction. Fixes the tombstone wire shape to match the sizing claims: a dead override now serializes as exactly one ov_c: key instead of three zero-padded keys, closing an IMPORTANT finding that the schema and storage-budget tables assumed a 1-key tombstone while the serializer emitted 3. Adds an exact wire-shape regression (live=3 keys, tombstone=1 key, virgin=0 keys, both tie policies) and extends I8/test_bounded_growth to check the tombstone shape after 100 set/clear round trips. Documents (rather than silently carries) the model's legacy drop-on-receive simplification: DeviceB(is_legacy=True) does not forward ov_* sibling keys it receives, unlike production's sanitizeContexts pass-through -- explained with the reason the BFS's own convergence/compaction verdicts are unaffected (legacy devices never act on overrides in the explorer). States canonical publication in NOTE.md as a protocol requirement (spec-amendment implication: production clients MUST canonicalize before publish) and scopes the reserved-namespace escape codec explicitly as a backward-compatibility limitation, not a collision-safe migration of pre-existing unescaped ov_-prefixed legacy data. BFS explorer: 7,129 states/policy; published-state merge closure: 45,074 pairs/both policies; both suites (exhaustive.py, mutation.py) exit 0, 7/7 mutants caught. Co-authored-by: Will Pfleger <pfleger.will@gmail.com> Signed-off-by: Will Pfleger <pfleger.will@gmail.com>
wpfleger96
force-pushed
the
duncan/nip-rs-unread-model
branch
from
July 17, 2026 20:22
62f97c2 to
47a476a
Compare
…nread model Resolves Thufir's final-pass NOT CLEAR findings on PR #1958: CRITICAL (transport atomicity): encode atomic slot-grouping rule. A context's frontier entry and all ov_s:/ov_c:/ov_b: sibling entries MUST travel in the same slot. Adds DeviceB.split_blob_into_slots (model.py) which round-robins per-context groups, not per-entry. Updates _ancestor_split_ctx_dicts and test_multi_slot_union to use grouped splits. Adds test_interleaved_delivery_grouping exercising both slot orders and delayed transient re-publication to a third observer (Thufir's exact witness). Adds mutant_m8 (M8_PerEntrySplit) which reverts to per-entry splitting and confirms the new test catches the false-clear counterexample. Documents the rule in NOTE.md under Multi-slot union with same normative weight as canonical publication. IMPORTANT (Candidate A coverage): NOTE.md invariant table marks I2, I3, I4, I6 as 'not exercised' for A instead of incorrect PASS. IMPORTANT (I5e cube-size wording): '300 points per tie policy' corrected to '156 clear-wins + 144 set-wins = 300 total'; 45,074 = 156^2 + 144^2 + 2 directed witnesses. MINOR (mutation section): count updated from 6 to 8; M7 and M8 added to table and narrative; M1-M6 subclass list updated to include M7,M8. Cosmetic MINOR: restore Candidate-comparison heading consumed by prior I5e insertion. Co-authored-by: Will Pfleger <pfleger.will@gmail.com> Signed-off-by: Will Pfleger <pfleger.will@gmail.com>
…e rewrite, M9, cleanup
CRITICAL: fix escaped-context-ID identity mismatch in split_blob_into_slots
(model.py). Frontier wire keys are escaped (e.g. 'esc:ov_s:evil') while ov_*
sibling keys use the raw suffix ('ov_s:evil'). Without unescaping the frontier
before grouping, the two entries land in different slots — a compliant publisher
can still produce a split register for any context whose raw ID starts with a
reserved prefix. Old/new slot-coordinate mixtures across publication cycles then
reproduce the round-1 partial-reconstruction poison. Fix: derive group identity
via unescape_context_key(wire_key) for frontier keys. Add M9 mutant reverting to
escaped-key grouping; add test_escaped_context_slot_grouping regression (two
publication cycles, old/new slot-coordinate mixture, canonical re-pub in loop).
IMPORTANT: rewrite test_interleaved_delivery_grouping with correct oracle. Prior
version never delivered first_slot to final_a/final_b and never performed the
receive-rest → re-publish step (substituted source's full blob). Rewritten to
exactly: partial_obs receives first_slot → publishes transient_1 → receives
second_slot → publishes transient_2; three representative delivery orders for
third-party finals covering the toxic path and both orderings. Re-validated: M8
caught in clear-wins toxic branch (3 violations), zero false violations under
set-wins.
IMPORTANT: fix NOTE prose vs executable coverage.
- NOTE:178 'Both candidates converge under all tested delivery permutations'
rephrased as algebraic property with note that I2-I4/I6 are exercised for
Candidate B only.
- NOTE:615 'Both pass all merge invariants' scoped to Candidate B (I2-I8
exhaustively verified; A exercised only on I1/I7/I9).
- NOTE:656-658 distinguished abstract grouping model (modeled by
split_blob_into_slots, including unescape fix) from production TypeScript
splitter (not modeled).
- Added unescape-before-group rule and M9 to Multi-slot section and mutation
table; updated count 8→9.
IMPORTANT: delete docs/formal/nip-rs-unread/__pycache__/*.cpython-314.pyc
(107,366 bytes, embedded absolute worktree path). Add __pycache__/ and *.pyc
to .gitignore to prevent recurrence.
MINOR: collapse deep-history delivery shapes 3→1 (2,016→672 points). The
split_fwd/split_rev shapes became semantically identical to single once the
atomic-grouping rule made a single-context compliant split whole-register+empty;
removed _ancestor_split_ctx_dicts (now dead code). Update NOTE cube-size figure.
Fix M8 witness narrative: block comment said 'ov_s+ov_b' in one slot; actual
M8 puts frontier+ov_s in slot 0, ov_b+ov_c in slot 1.
Co-authored-by: Will Pfleger <pfleger.will@gmail.com>
Signed-off-by: Will Pfleger <pfleger.will@gmail.com>
wpfleger96
marked this pull request as ready for review
July 31, 2026 14:55
wpfleger96
added a commit
that referenced
this pull request
Jul 31, 2026
…nread model Resolves Thufir's final-pass NOT CLEAR findings on PR #1958: CRITICAL (transport atomicity): encode atomic slot-grouping rule. A context's frontier entry and all ov_s:/ov_c:/ov_b: sibling entries MUST travel in the same slot. Adds DeviceB.split_blob_into_slots (model.py) which round-robins per-context groups, not per-entry. Updates _ancestor_split_ctx_dicts and test_multi_slot_union to use grouped splits. Adds test_interleaved_delivery_grouping exercising both slot orders and delayed transient re-publication to a third observer (Thufir's exact witness). Adds mutant_m8 (M8_PerEntrySplit) which reverts to per-entry splitting and confirms the new test catches the false-clear counterexample. Documents the rule in NOTE.md under Multi-slot union with same normative weight as canonical publication. IMPORTANT (Candidate A coverage): NOTE.md invariant table marks I2, I3, I4, I6 as 'not exercised' for A instead of incorrect PASS. IMPORTANT (I5e cube-size wording): '300 points per tie policy' corrected to '156 clear-wins + 144 set-wins = 300 total'; 45,074 = 156^2 + 144^2 + 2 directed witnesses. MINOR (mutation section): count updated from 6 to 8; M7 and M8 added to table and narrative; M1-M6 subclass list updated to include M7,M8. Cosmetic MINOR: restore Candidate-comparison heading consumed by prior I5e insertion. Co-authored-by: Will Pfleger <pfleger.will@gmail.com> Signed-off-by: Will Pfleger <pfleger.will@gmail.com>
Member
Author
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.
Summary
Bounded exhaustive model comparing two candidate CRDT encodings for a manual mark-as-unread override layer within NIP-RS read state: lexicographic operation register (A) vs two grow-only counters + baseline (B).
RegB(0, max(S,C), 0)): a register that ever hadS>0orC>0is never fully deleted, blocking counter reuse; only virgin (never-set) registers compact toNoneov_*sibling entries must travel in the same slot. Grouping derives one logical identity for both key classes — frontier wire keys are unescaped viaunescape_context_key()before grouping — so a partial register is structurally impossible from a compliant publisher, including for opaque context IDs that collide with reserved prefixes (e.g. rawov_s:evil). Verified with interleaved receive → canonical re-publish → receive-rest → re-publish delivery tests and an old/new slot-coordinate mixture regressionov_/esc:escaping) so a pre-existing opaque NIP-RS context ID cannot be misparsed as override control state; verified with an adversarial round-trip testDeviceBsubclass injection with recorded counterexamples, including directed regressions for the tombstone-floor resurrection witness (M6), raw serialization without canonicalization (M7), per-entry slot splitting (M8), and escaped-key grouping (M9)>256-byte key drop hazard documentedNew files in
docs/formal/nip-rs-unread/:model.py,exhaustive.py,mutation.py,NOTE.md. Both scripts are deterministicpython3and exit 0. Also adds__pycache__/and*.pycto the repo.gitignore.