Correct store.rs and the cut9 header's no-second-writer prose
F7: store.rs claimed "no non-test code outside this crate touches a row directly." False: MindStore's supertrait CacheBackingStore and the public compare_and_swap_batch already let it. Rewrite the comment to say so, and name the re-export honestly -- two traits, CacheBackingStore and DatabaseEntry, plus DatabaseEntry's own derive macro riding along under the same name in a different namespace. Sealing the store so admission is its only write path stays a recorded follow-up, its own cut; nothing here seals it. The cut9 entries header rested the same false premise: "no behaviour this Body can reach" for assignments_of and resolutions_of's two weakenings assumed admission is the only write path. Corrected to "not yet reached," with the reason -- a row planted through the store port directly bypasses A5's instance check and the leaf's kind/id grammar alike. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
parent
56143c36ea
commit
7fc8ed3610
2 changed files with 35 additions and 16 deletions
|
|
@ -12,11 +12,19 @@ use cultcache_rs::CultCacheEnvelope;
|
|||
/// dependency entry, one rev, one place to move it.
|
||||
pub use cultcache_rs::OwnedRedbMessagePackBackingStore;
|
||||
|
||||
/// CultCache's own row traits, re-exported for the same reason and used for
|
||||
/// one thing: the daemon's store-integrity test reaches past this crate to
|
||||
/// break a store's rows, so that a read over the broken store raises the
|
||||
/// refusal its dispatch arm must carry. No non-test code outside this crate
|
||||
/// touches a row directly, and nothing here abstracts them.
|
||||
/// CultCache's own row traits, re-exported for the same reason: the crate
|
||||
/// that serves a mind reaches a store's rows through here rather than
|
||||
/// declaring `cultcache-rs` a second time. The daemon's store-integrity tests
|
||||
/// use it to break a row on purpose, over a real store, so a read over the
|
||||
/// broken store raises the refusal its dispatch arm must carry — but that is
|
||||
/// not the only door a row already has: `MindStore`'s own supertrait is
|
||||
/// `CacheBackingStore`, and its public `compare_and_swap_batch` already lets
|
||||
/// non-test code outside this crate write a row directly. Sealing the store
|
||||
/// so admission is its only write path is a follow-up, its own cut; this
|
||||
/// re-export does not widen anything that door does not already reach. It
|
||||
/// carries two traits, `CacheBackingStore` and `DatabaseEntry`, plus
|
||||
/// `DatabaseEntry`'s own derive macro, which shares its name in a different
|
||||
/// namespace and rides along unnamed.
|
||||
pub use cultcache_rs::{CacheBackingStore, DatabaseEntry};
|
||||
|
||||
/// A store a mind can be opened over. `Clone` shares ownership of the same
|
||||
|
|
|
|||
|
|
@ -15,21 +15,32 @@
|
|||
# breaks it for the views. V1L is H41's own edit, listed here as well as in
|
||||
# `eureka-cut8-mutations.psd1` -- one mutant, two suites, one owner.
|
||||
#
|
||||
# Two weakenings the spec names have no entry because they change no behaviour
|
||||
# this Body can reach, and a mutation that cannot fail is not a proof:
|
||||
# Two weakenings the spec names have no entry, not because they are
|
||||
# unreachable but because nothing on this Body's own public surface reaches
|
||||
# them today, which is a narrower claim than the one this header used to make.
|
||||
# "No behaviour this Body can reach" rested on admission being the only write
|
||||
# path, and that premise is false: `MindStore::compare_and_swap_batch` is
|
||||
# `pub`, and `store.rs`'s own re-export of `CacheBackingStore` already lets
|
||||
# code outside this crate push a row that skips A5 (and every other admission
|
||||
# rule) entirely, the same door the cut9 header's line 18-24 claim rested on.
|
||||
# Recorded as not yet reached, not as unreachable:
|
||||
#
|
||||
# - `assignments_of` comparing the repo and ignoring the instance. A5 refuses
|
||||
# a stewardship naming another instance, so every stewardship a mind holds
|
||||
# already names that mind, and every other caller is a sequence this mind
|
||||
# derives over its own scope.
|
||||
# a stewardship naming another instance for every row admission writes, so
|
||||
# every stewardship admission ever lands already names the mind that holds
|
||||
# it, and every caller reachable through admission is a sequence this mind
|
||||
# derives over its own scope. A row planted through the store port directly,
|
||||
# naming another instance, is not yet reached by anything in this suite.
|
||||
# - `resolutions_of` comparing a subject by `id` alone, which was `V10L` until
|
||||
# the leaf opened `PipelineRef::validate_ref` and `view` and `history` began
|
||||
# asking it. A ref that reaches the comparison now has a kind its id's kind
|
||||
# segment agrees with, and every stored subject was held to the same grammar
|
||||
# at admission, so on both sides the kind is a function of the id and
|
||||
# comparing the whole ref and comparing the id alone cannot differ. The rule
|
||||
# is still the rule; it is the reachable weakening that went, and what
|
||||
# defends it is `V24`/`V24L` at the doors instead.
|
||||
# asking it. A ref that reaches the comparison through admission has a kind
|
||||
# its id's kind segment agrees with, and every stored subject admission
|
||||
# writes was held to the same grammar, so on both sides the kind is a
|
||||
# function of the id and comparing the whole ref and comparing the id alone
|
||||
# cannot differ for anything admission wrote. The rule is still the rule; it
|
||||
# is the reachable weakening that went, and what defends it is `V24`/`V24L`
|
||||
# at the doors instead. A row planted through the store port directly, with
|
||||
# a subject whose kind disagrees with its id, is not yet reached either.
|
||||
#
|
||||
# The one listed beside them in the spec is failable and has an entry: the
|
||||
# `semantic` check below `Reader::new` changes the answer for a store the
|
||||
|
|
|
|||
Loading…
Reference in a new issue