Skip to content

Detect changes fused with join/act - #9

Merged
plaidfinch merged 4 commits into
mainfrom
changed-flag-152
Jul 30, 2026
Merged

Detect changes fused with join/act#9
plaidfinch merged 4 commits into
mainfrom
changed-flag-152

Conversation

@plaidfinch

Copy link
Copy Markdown
Collaborator

No description provided.

A test-only, per-thread counter at Tree::hash, with a liveness pin (one
snapshot hash moves it by one) and two commit-path pins: a batch commit
reads the root hash twice inside its watch critical section, and a
gossip session twice per side, both to answer "did the tree change?"
by before/after hash comparison. The post-mutation read hashes the
freshly rebuilt copy-on-write spine while the lock is held; these pins
are the enforced baseline that cost is measured against.
act's effectual-action observer already knows whether any leaf was
inserted, replaced, or removed: no observation means no ceiling
movement and a byte-identical root hash, so act now returns that bit.
join threads one bit through its recursion, decided exactly and without
hashing: a gain is a subtree of the counterparty surviving the deletion
filter where we held nothing, and a drop moves a node's exact memoized
leaf count; gains and drops live at distinct content-addressed paths
and are monotone per path, so they cannot cancel.

Contracts at both definitions: false is exact (hash byte-identical;
watchers skipped on false miss nothing). For join, true is exact too,
and deliberately excludes ceiling-only advancement. For act, true is
conservative in exactly one constructible case: a store poisoned by an
escaped version (leaf above the ceiling, the shape session ingestion
rejects) silently skips a causally-prior forget while the observer
fires - one spurious wakeup, never a missed one; unreachable for
honestly built trees, whose ceilings bound every leaf.

Pins: act/join changed-flag-tracks-the-root-hash proptests (the
biconditional over honest trees and divergent pairs), a ceiling-only
join reporting unchanged, and the poisoned-store false positive
constructed.
The batch commit and the gossip write-back each decided their watch
notification by reading the root hash before and after the mutation,
forcing a hash over the freshly rebuilt memo-less spine inside the
watch critical section. Both now take the answer from the changed flag
act and join return, and the commit-path meter pins tighten from two
root-hash reads per batch commit (four per gossip session) to zero.
Watch semantics on the true-change path are unchanged: the flag's
false direction is exact, so observers wake exactly when they did.
Prose only: each long first paragraph becomes a short summary sentence
with the detail below the fold, as the doclint gate requires.
@plaidfinch
plaidfinch merged commit 491272d into main Jul 30, 2026
1 check passed
@plaidfinch
plaidfinch deleted the changed-flag-152 branch July 30, 2026 22:38
plaidfinch added a commit that referenced this pull request Aug 7, 2026
Owner counterweight (dissolve/link/mint, per term — binding ruling
applied retroactively to the T2 lexicon):
- min-into-max: DISSOLVED — every site now names suanpan's
  merge_into_wider plainly (the narrower buffer folds into the wider),
  linked once at the close bullet.
- range/frame: resolved by DELETING "frame" from watermark.rs — the
  web's word is now "range" everywhere (prose, field docs, assert
  messages); "range" keeps its one definition (the client's bracket,
  never interpreted by the web). fill.rs's one "watermark frame" phrase
  re-denominated.
- plateau: LINKED — overlay.rs's tiling vocabulary keeps the one mint;
  skyline.rs carries a plain gloss naming overlay as the minting site
  (a public->private intra-doc link cannot resolve on the public build).
- "both width currencies": DISSOLVED into "both the touch and limb
  counters".
- B/P/L and F/L component names: LINKED — named plainly in query.rs
  with the pointer to integral.rs's existing mints, no re-mint.
- priced/paid-by, left-full site, settled (filter.rs),
  liveness-floor/improvement-tripwire: MINTED (each spent widely enough
  that per-use restatement costs more; the first two per the owner's
  own examples).
- full child: LINKED to IdNode::Full (the API's own name).

Polish implemented (by synthesis numbering):
- foundations #5 (walk.rs/overlay.rs internal Panics sections adopt the
  precise truncation/malformation-vs-silent contract, pointing at
  causal_cmp's canonical statement), #7 (Extremum reset-policy
  comparison + provenance contract, grounded in the pool's
  clear-on-retire), #8 (CursorSet absent-slot lemma written out;
  priority's commutative-sums freedom stated), #9 (GAMMA_SMALL_MAG_BOUND
  named with its derivation, both twins), #10 (root-doc micro-frictions:
  first sentence, zigzag letter d vs code-shape k, gamma-covers-zero
  clause, codec-cursor reference), #11 (Step vs Signed distinction),
  #12 (block-scan honesty leads the skip docs), #13 (overlay layer-map
  sentence split), #14 (numeric flip<=depth restatement), #15
  (IdLeafCursor pop-flip survival comment + idbits packed-coding
  pointer), #16 (advance's unexhausted precondition), #17 (sweep
  early-exit Break-carries-V reworded); delta latent items: the
  advance dual-channel why (callback = order, return = crossings),
  masked.rs Directions::relation link.
- verdicts #6 (admit.rs "placement walk's idiom" misattribution dropped
  at both sites — restated-not-reused, fallibility argument kept), #7
  (masked height integrators fold plainly via fold_signed_int; the
  Side::A polarity pun and its rescue comments gone), #9 (settled
  minted at Pair::live), #11 (end-first arbitrariness stated), #12
  (trichotomy glossed as the comparison trichotomy), #13 (/* negative:
  */ argument comments at the literal seeding sites, uniformly), #14
  (validate.rs first-leaf zero_delta defense), #15 (admit.rs rewrap),
  #16 (subsumption's pointwise no-block-skipping premise), #17
  (filter.rs Cost names the per-interval bookkeeping scans); delta:
  Demand::After/Before inclusivity reminders at both downstream
  re-check sites.
- streams F5 (grow Phase 2 absolute-code case), F6 (emit sticky-tie
  seed comments + placeholder note), F7 (build absorb-pop lens
  comment), P1 (re-anchor gloss), P2 (delta_code takes Option<&Step>),
  P3 (merge per-step comments).
- integral P1 (one's why-a-field), P3 (pair_fold unwrap_or(1) declared
  unreachable-but-total), P4 (feeds garden path resolved in the Cost
  list), P5 (rank Cost paragraph as a charge list + the four-structure
  map sentence), F7 (top-index domination appositive), F8 (forward/
  reverse dual names dropped for plain statements), F11 (jump-pair
  family named at the jump-comb parenthetical), F12 (carry-cliff and
  comb-teeth glosses), F13 (resolve_latent's caller obligation stated
  abstractly).
- tick F6 (one-web-range-per-Frames-entry comment at the single close),
  F7 (FillWalk/PreScan field stack -> web, matching query/web.rs), F8
  (Relation::Min <-> REL_FOLLOWER invariant on the type), F9
  (FOLLOWER_SLOTS pub(super) + const assert binding the slot roster
  across files), F14 covered by the propagate doc's existing narration
  (loop-invariant comment deferred: see report), F15 (level-vs-depth
  caution at the twin declaration), F16 (level-0 keeper exemption), F17
  (recorder invariant block), F18 (replay_max why-not-park), F19 (the
  twelve-line measurement roster reduced to claim + pointer), F20
  (close() doc: fill discards the outcome entirely; min-ticks
  dispatches all four arms) [in close()'s payload sentence], F21
  (emit_offset's constant-true note_match as a debug-asserted match),
  F22 (Out::leaf # Panics heading), F23 (copy_subtree regime map), F24
  (compact()'s two-digits-cover-a-u64 derivation); tick polish: the
  two precondition-shaped assert messages restated as invariants,
  materialize's sign() collapse idiom matched to the explained
  spelling, walk()'s derived-depth comment, emit_step's deliberately-
  unread step comment, RouteProbe's Cost::MAX-as-don't-care and
  id_span fallback notes, the watermark representation paragraph as a
  list with the derivation sentence standing alone (relay-8 guard
  honored), the undercut bullet as sub-bullets, the cost essay's
  first-read gate, new()/compacting() pointing at their committed
  families, ascend-cliff floor's created/penetrated split, both
  derived floors scoped to their mechanism with the floor-premise
  escape stated.

Zero meter movement: full suite 775 green, board 2014/2014 green,
worst-case pin clean (172 rows, both scales), clippy clean on default
and --all-features. validate_bits gated to test/meter (its production
consumer is gone), keeping the default build warning-free.
plaidfinch added a commit that referenced this pull request Aug 7, 2026
Detect changes fused with join/act
plaidfinch added a commit that referenced this pull request Aug 7, 2026
Owner counterweight (dissolve/link/mint, per term — binding ruling
applied retroactively to the T2 lexicon):
- min-into-max: DISSOLVED — every site now names suanpan's
  merge_into_wider plainly (the narrower buffer folds into the wider),
  linked once at the close bullet.
- range/frame: resolved by DELETING "frame" from watermark.rs — the
  web's word is now "range" everywhere (prose, field docs, assert
  messages); "range" keeps its one definition (the client's bracket,
  never interpreted by the web). fill.rs's one "watermark frame" phrase
  re-denominated.
- plateau: LINKED — overlay.rs's tiling vocabulary keeps the one mint;
  skyline.rs carries a plain gloss naming overlay as the minting site
  (a public->private intra-doc link cannot resolve on the public build).
- "both width currencies": DISSOLVED into "both the touch and limb
  counters".
- B/P/L and F/L component names: LINKED — named plainly in query.rs
  with the pointer to integral.rs's existing mints, no re-mint.
- priced/paid-by, left-full site, settled (filter.rs),
  liveness-floor/improvement-tripwire: MINTED (each spent widely enough
  that per-use restatement costs more; the first two per the owner's
  own examples).
- full child: LINKED to IdNode::Full (the API's own name).

Polish implemented (by synthesis numbering):
- foundations #5 (walk.rs/overlay.rs internal Panics sections adopt the
  precise truncation/malformation-vs-silent contract, pointing at
  causal_cmp's canonical statement), #7 (Extremum reset-policy
  comparison + provenance contract, grounded in the pool's
  clear-on-retire), #8 (CursorSet absent-slot lemma written out;
  priority's commutative-sums freedom stated), #9 (GAMMA_SMALL_MAG_BOUND
  named with its derivation, both twins), #10 (root-doc micro-frictions:
  first sentence, zigzag letter d vs code-shape k, gamma-covers-zero
  clause, codec-cursor reference), #11 (Step vs Signed distinction),
  #12 (block-scan honesty leads the skip docs), #13 (overlay layer-map
  sentence split), #14 (numeric flip<=depth restatement), #15
  (IdLeafCursor pop-flip survival comment + idbits packed-coding
  pointer), #16 (advance's unexhausted precondition), #17 (sweep
  early-exit Break-carries-V reworded); delta latent items: the
  advance dual-channel why (callback = order, return = crossings),
  masked.rs Directions::relation link.
- verdicts #6 (admit.rs "placement walk's idiom" misattribution dropped
  at both sites — restated-not-reused, fallibility argument kept), #7
  (masked height integrators fold plainly via fold_signed_int; the
  Side::A polarity pun and its rescue comments gone), #9 (settled
  minted at Pair::live), #11 (end-first arbitrariness stated), #12
  (trichotomy glossed as the comparison trichotomy), #13 (/* negative:
  */ argument comments at the literal seeding sites, uniformly), #14
  (validate.rs first-leaf zero_delta defense), #15 (admit.rs rewrap),
  #16 (subsumption's pointwise no-block-skipping premise), #17
  (filter.rs Cost names the per-interval bookkeeping scans); delta:
  Demand::After/Before inclusivity reminders at both downstream
  re-check sites.
- streams F5 (grow Phase 2 absolute-code case), F6 (emit sticky-tie
  seed comments + placeholder note), F7 (build absorb-pop lens
  comment), P1 (re-anchor gloss), P2 (delta_code takes Option<&Step>),
  P3 (merge per-step comments).
- integral P1 (one's why-a-field), P3 (pair_fold unwrap_or(1) declared
  unreachable-but-total), P4 (feeds garden path resolved in the Cost
  list), P5 (rank Cost paragraph as a charge list + the four-structure
  map sentence), F7 (top-index domination appositive), F8 (forward/
  reverse dual names dropped for plain statements), F11 (jump-pair
  family named at the jump-comb parenthetical), F12 (carry-cliff and
  comb-teeth glosses), F13 (resolve_latent's caller obligation stated
  abstractly).
- tick F6 (one-web-range-per-Frames-entry comment at the single close),
  F7 (FillWalk/PreScan field stack -> web, matching query/web.rs), F8
  (Relation::Min <-> REL_FOLLOWER invariant on the type), F9
  (FOLLOWER_SLOTS pub(super) + const assert binding the slot roster
  across files), F14 covered by the propagate doc's existing narration
  (loop-invariant comment deferred: see report), F15 (level-vs-depth
  caution at the twin declaration), F16 (level-0 keeper exemption), F17
  (recorder invariant block), F18 (replay_max why-not-park), F19 (the
  twelve-line measurement roster reduced to claim + pointer), F20
  (close() doc: fill discards the outcome entirely; min-ticks
  dispatches all four arms) [in close()'s payload sentence], F21
  (emit_offset's constant-true note_match as a debug-asserted match),
  F22 (Out::leaf # Panics heading), F23 (copy_subtree regime map), F24
  (compact()'s two-digits-cover-a-u64 derivation); tick polish: the
  two precondition-shaped assert messages restated as invariants,
  materialize's sign() collapse idiom matched to the explained
  spelling, walk()'s derived-depth comment, emit_step's deliberately-
  unread step comment, RouteProbe's Cost::MAX-as-don't-care and
  id_span fallback notes, the watermark representation paragraph as a
  list with the derivation sentence standing alone (relay-8 guard
  honored), the undercut bullet as sub-bullets, the cost essay's
  first-read gate, new()/compacting() pointing at their committed
  families, ascend-cliff floor's created/penetrated split, both
  derived floors scoped to their mechanism with the floor-premise
  escape stated.

Zero meter movement: full suite 775 green, board 2014/2014 green,
worst-case pin clean (172 rows, both scales), clippy clean on default
and --all-features. validate_bits gated to test/meter (its production
consumer is gone), keeping the default build warning-free.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant