Pass 11 audit follow-up: honest LayoutObjectId status + doc/test gaps
Independent audit ofb2f2e20/a7adbdc. The canonical, document-state byte layouts were already correct and golden-locked; this closes the one real spec-vs-code gap (in the non-canonical layout namespace) and the smaller doc/test gaps around it. LayoutObjectId (item 2.6): the spec normatively stated the id "is derived ... with MUSCLOID" and the ratification log / layout DECISIONS header called it "pinned" -- but no code uses MUSCLOID (stable_layout_id and manifestation_layout_id are untagged; synthesized_layout_id borrows MUSCCONF), and MUSCLOID cannot even be constructed: DomainTag::from_bytes accepts only built-ins or MUSCS-prefixed tags, so wiring it requires changing the frozen determinism crate (out of scope for a spec pass, and the spec itself says MUSCLOID is not a canonical system tag). Kept MUSCLOID as the pinned Track-A target and made every artifact honest that the v0 code is provisional: - spec: "is derived" -> "MUST be derived" (forward contract) + a note that the prototype mints provisional ids; changelog "pinned" -> "specified ... as the Track-A target". - records: ratification-log line 2.6 and layout DECISIONS header/body now state spec-pinned-but-code-provisional; stale "Pass 11 candidate 3" pointer now cites the ratified requirement. - provenance.rs comments name the MUSCLOID target and label the current derivation provisional. Other fixes: - epiphany-core/DECISIONS.md: the Tuplet bullet still claimed degenerate ratios are caught by runtime invariant 16 "since a Tuplet is a plain struct" -- stale after the construction-time TupletRatio change. Rewritten. - codec.rs: added degenerate_tuplet_ratio_is_rejected_on_decode, guarding the TupletRatio::dec re-validation branch that no test exercised (the constructor was tested, the decode path was not). - spec: integrity-anomaly snippet kind.canonical_bytes() -> to_canonical_bytes() (the actual method). - ids.rs / reduce.rs: clarifying comments (ManifestId's intentional, golden-locked document_id/generation duplication; compute_promotions bucketing by voice == (staff_instance, original_voice) via Invariant 5). Verification: cargo test --workspace (434 pass, +1), clippy --all-targets clean (0 warnings), fmt clean; spec rebuilds (lualatex, 0 undefined refs, 254pp). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
a7adbdc5a1
commit
0d8ec61a3c
|
|
@ -101,6 +101,11 @@ impl ManifestId {
|
|||
/// core_spec §"Manifest Encoding", Requirement `req:format:manifest-id`
|
||||
/// (`trunc128(BLAKE3("MUSCMNIF" || document_id || generation || body))`,
|
||||
/// body excluding `manifest_id`).
|
||||
///
|
||||
/// Note: `document_id` and `generation` are committed twice — explicitly
|
||||
/// here and again inside `body_preimage` (the canonical manifest body opens
|
||||
/// with them). This duplication is intentional and golden-locked, not an
|
||||
/// oversight: the preimage shape above is the ratified format.
|
||||
pub(crate) fn derive(document_id: DocumentId, generation: u64, body_preimage: &[u8]) -> Self {
|
||||
let mut p = Preimage::new(DomainTag::MANIFEST_ID);
|
||||
p.push_bytes(document_id.as_bytes());
|
||||
|
|
|
|||
|
|
@ -208,5 +208,8 @@ which is both faithful and removes the need for a runtime pass:
|
|||
- `TimeSignature::new` rejects beat groups that do not sum to the measure
|
||||
duration.
|
||||
- `EventOrderingDAG::try_new` rejects a cyclic aleatoric ordering.
|
||||
- `Tuplet` degenerate ratios (`0:n`/`n:0`) are caught by invariant 16
|
||||
(`check_invariants`), since a `Tuplet` is a plain struct.
|
||||
- `TupletRatio::new` rejects degenerate ratios (either term zero, or
|
||||
`actual == notated`); its fields are private, so a degenerate `TupletRatio`
|
||||
is never representable, and codec decode re-validates through the same
|
||||
constructor. (Pass 11 item 3.5 moved this from a runtime invariant-16
|
||||
sub-check to a construction-time MUST.)
|
||||
|
|
|
|||
|
|
@ -2065,6 +2065,30 @@ mod tests {
|
|||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn degenerate_tuplet_ratio_is_rejected_on_decode() {
|
||||
// Guards the TupletRatio::dec re-validation (Pass 11 item 3.5): a
|
||||
// hand-crafted byte stream must not be able to inject a degenerate ratio
|
||||
// that TupletRatio::new would reject at construction. Without the
|
||||
// `.ok_or(Reconstruct)` in dec, these would decode into an
|
||||
// unconstructible-by-API value.
|
||||
let decode = |actual: u32, notated: u32| {
|
||||
let mut bytes = Vec::new();
|
||||
actual.enc(&mut bytes);
|
||||
notated.enc(&mut bytes);
|
||||
TupletRatio::dec(&mut Reader::new(&bytes))
|
||||
};
|
||||
for (a, n) in [(0u32, 0u32), (2, 0), (0, 2), (4, 4)] {
|
||||
assert!(
|
||||
matches!(decode(a, n), Err(ScoreDecodeError::Reconstruct(_))),
|
||||
"degenerate ratio {a}:{n} must be rejected on decode"
|
||||
);
|
||||
}
|
||||
// A well-formed ratio still decodes.
|
||||
let ok = decode(3, 2).expect("non-degenerate ratio decodes");
|
||||
assert_eq!((ok.actual(), ok.notated()), (3, 2));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn exotic_event_and_pitch_variants_round_trip() {
|
||||
// Round-trip is structural, so this need not satisfy graph invariants —
|
||||
|
|
|
|||
|
|
@ -9,11 +9,15 @@ items batched."*).
|
|||
|
||||
> **RATIFIED (Pass 11, 2026-06-21).** layout P11-2 (`LayoutObjectId` derivation)
|
||||
> is ratified into `core_spec.tex` §"Provenance"
|
||||
> (`req:layoutir:object-id-derivation`): a `MUSCLOID`-tagged derivation keying
|
||||
> multiply-manifested objects on `(source, region)` and synthesized objects on
|
||||
> `(source, synthesis_kind, stable_semantic_instance_key)`. Layout ids are
|
||||
> non-canonical, so this is flagged for Track A (solver/renderer). layout P11-1
|
||||
> (layout→ops dependency) stays a crate-topology call for the G–K re-cut. See
|
||||
> (`req:layoutir:object-id-derivation`): the spec **pins** a `MUSCLOID`-tagged
|
||||
> derivation keying multiply-manifested objects on `(source, region)` and
|
||||
> synthesized objects on `(source, synthesis_kind, stable_semantic_instance_key)`.
|
||||
> Layout ids are non-canonical, so the `MUSCLOID` tag is **flagged for Track A
|
||||
> and not yet wired in code**: this crate still mints provisional ids (untagged;
|
||||
> synthesized borrows `MUSCCONF`) because the frozen determinism crate exposes no
|
||||
> `MUSCLOID` tag (see the `stable_layout_id` bullet below). Adopting the spec'd
|
||||
> derivation is Track A (solver/renderer) work. layout P11-1 (layout→ops
|
||||
> dependency) stays a crate-topology call for the G–K re-cut. See
|
||||
> `spec/PASS11_RATIFICATION_LOG.md`.
|
||||
|
||||
## Scope
|
||||
|
|
@ -88,7 +92,11 @@ object is covered); the provenance-preservation contract itself is unchanged.
|
|||
reordering of other objects (Chapter 7 §"Provenance"). It is not domain-
|
||||
separated, and the engraving-decision id borrows the `MUSCCONF` tag with a
|
||||
literal `engraving-decision` type prefix, because the frozen determinism crate
|
||||
(Agent A) defines no layout-object domain tag. See Pass 11 candidate 3.
|
||||
(Agent A) defines no layout-object domain tag. Pass 11 ratified the **target**
|
||||
derivation — a `MUSCLOID`-tagged hash (`req:layoutir:object-id-derivation`) —
|
||||
but adopting it is Track A work (the determinism crate must first expose the
|
||||
layout-namespace tag); these ids stay provisional until then. See the header
|
||||
note.
|
||||
|
||||
- **Repeated manifestations get per-`(source, region)` ids.** A score-graph
|
||||
object manifested within a region is laid out **per manifestation**: its stable
|
||||
|
|
|
|||
|
|
@ -136,8 +136,9 @@ impl Provenance {
|
|||
/// stable across re-layouts where the source is unchanged): inserting,
|
||||
/// removing, or reordering other objects cannot change any object's stable id,
|
||||
/// because each depends solely on its own source's canonical bytes. v0 derives
|
||||
/// it as `trunc128(BLAKE3(source.canonical_bytes()))`; see `DECISIONS.md` for
|
||||
/// why this is not (yet) domain-separated.
|
||||
/// it as `trunc128(BLAKE3(source.canonical_bytes()))` — a provisional, untagged
|
||||
/// stand-in. The spec (`req:layoutir:object-id-derivation`) pins a
|
||||
/// `MUSCLOID`-tagged derivation as the Track A target; see `DECISIONS.md`.
|
||||
pub fn stable_layout_id(source: &TypedObjectId) -> LayoutObjectId {
|
||||
LayoutObjectId(trunc128(&blake3_256(&source.canonical_bytes())))
|
||||
}
|
||||
|
|
@ -155,9 +156,11 @@ pub fn manifestation_layout_id(source: &TypedObjectId, region: RegionId) -> Layo
|
|||
|
||||
/// Derives the stable layout id of an **engraver-synthesized** object from its
|
||||
/// `source` and its [`SynthesisKind`], so distinct synthesis kinds from one
|
||||
/// source do not collide (Chapter 7 §"Provenance"). Domain-tagged via the
|
||||
/// borrowed `MUSCCONF` tag with a `synthesized` discriminator prefix (the
|
||||
/// determinism crate defines no layout tag — see `DECISIONS.md`).
|
||||
/// source do not collide (Chapter 7 §"Provenance"). Provisionally domain-tagged
|
||||
/// via the borrowed `MUSCCONF` tag with a `synthesized` discriminator prefix; the
|
||||
/// determinism crate defines no `MUSCLOID` layout tag yet, and the spec'd
|
||||
/// `MUSCLOID` derivation (`req:layoutir:object-id-derivation`) is the Track A
|
||||
/// target — see `DECISIONS.md`.
|
||||
pub fn synthesized_layout_id(
|
||||
source: &TypedObjectId,
|
||||
kind: SynthesisKind,
|
||||
|
|
|
|||
|
|
@ -731,8 +731,11 @@ impl<'a> Reducer<'a> {
|
|||
// --- Voice promotion pre-pass (Chapter 6 §6.10 InsertEvent). ------------
|
||||
|
||||
fn compute_promotions(&mut self, active: &[&OperationEnvelope]) {
|
||||
// Bucket inserts by target voice. Promotion applies only to concurrent
|
||||
// operations whose half-open duration intervals overlap.
|
||||
// Bucket inserts by target voice. Bucketing by `op.voice` alone realizes
|
||||
// the spec's `(staff_instance, original_voice)` key: a VoiceId is
|
||||
// globally unique and (Invariant 5) belongs to exactly one staff
|
||||
// instance, so the voice id alone determines the pair. Promotion applies
|
||||
// only to concurrent operations whose half-open duration intervals overlap.
|
||||
let mut buckets: BTreeMap<VoiceId, Vec<&OperationEnvelope>> = BTreeMap::new();
|
||||
for env in active {
|
||||
if let OperationPayload::Primitive(OperationKind::InsertEvent(op)) = &env.payload {
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ unchanged. The full worklist is `PASS11_WORKLIST.md`.
|
|||
| 2.3 `>2`-way promotion | P11-C4 | **adopt + lifted to normative** — order-independent pre-pass: bucket by voice, walk by OperationId, retain a non-overlapping set, promote each overlapping loser (lowest-id retained survivor wins); applies to **partial** interval overlaps, not just identical onsets | §"System-Promoted Voices", `req:graph:promotion-generalization` | `reduce.rs::compute_promotions` |
|
||||
| 2.4 Open-vocab enums | P11-C9 | **decided: pinned core sets, kept `Registered`** — `TransactionCategory ∈ {NoteEntry, Structural, Layout, Import, Registered}`; `ObjectKind ∈ {Voice, Pitch, Registered}` (narrower than the 28 object kinds: only kinds minted into the system namespace) | `req:semops:transaction-category`, `req:graph:object-kind-vocab` | `payload.rs`, `support.rs` |
|
||||
| 2.5 `ResolveConflict` Dismissed | P11-C10 | **decided: added `ResolutionAction::Dismiss`** (code + spec) — closes the half-unreachable state machine; the Dismiss action selects the `Dismissed` state, every other action selects `Resolved` | §"Conflict Resolution Operations" | `conflict.rs`, `reduce.rs::resolve_conflict`, `resolve_conflict_with_dismiss_reaches_dismissed_state` |
|
||||
| 2.6 Layout-object id | layout P11-2 | **decided + registered tag (Track A)** — `MUSCLOID`-tagged derivation; keys multiply-manifested objects on `(source, region)`, synthesized objects on `(source, synthesis_kind, stable_semantic_instance_key)`. Non-canonical (not document state); consumed by the solver/renderer | §"Provenance", `req:layoutir:object-id-derivation` | `layout-ir` provenance |
|
||||
| 2.6 Layout-object id | layout P11-2 | **decided: spec pins `MUSCLOID` tag; code adoption is Track A** — the spec specifies a `MUSCLOID`-tagged derivation keying multiply-manifested objects on `(source, region)`, synthesized objects on `(source, synthesis_kind, stable_semantic_instance_key)`. Non-canonical (not document state). The v0 `layout-ir` crate still mints **provisional** ids (untagged; synthesized borrows `MUSCCONF`) because the frozen determinism crate exposes no `MUSCLOID` tag — realizing the spec'd derivation is Track A work, not done in this pass | §"Provenance", `req:layoutir:object-id-derivation` | `layout-ir` provenance (provisional) |
|
||||
|
||||
## Bucket 3 — Fixes (spec was contradictory or silent)
|
||||
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -3690,7 +3690,7 @@ pub enum ObjectKind {
|
|||
Section~\ref{sec:graph:system-derived} with the reserved domain tag
|
||||
\texttt{"MUSCSANM"} over the anomaly kind's canonical bytes:
|
||||
\texttt{derive\_system\_id::<IntegrityAnomalyId>(b"MUSCSANM",
|
||||
\&kind.canonical\_bytes())}. Because the identity is content-derived
|
||||
\&kind.to\_canonical\_bytes())}. Because the identity is content-derived
|
||||
from the kind, two replicas observing the same structural failure
|
||||
derive the same anomaly identifier and therefore agree on anomaly
|
||||
identity across the network.
|
||||
|
|
@ -7898,9 +7898,9 @@ pub struct LayoutObjectId(pub u128);
|
|||
\begin{requirement}
|
||||
\label{req:layoutir:object-id-derivation}
|
||||
A \texttt{LayoutObjectId} \MUST{} be stable across re-layouts whose
|
||||
underlying source is unchanged. It is derived by domain-separated
|
||||
BLAKE3 truncation with the reserved layout domain tag
|
||||
\texttt{"MUSCLOID"} over a key that depends on how the object is
|
||||
underlying source is unchanged. It \MUST{} be derived by
|
||||
domain-separated BLAKE3 truncation with the reserved layout domain
|
||||
tag \texttt{"MUSCLOID"} over a key that depends on how the object is
|
||||
manifested:
|
||||
|
||||
\begin{itemize}
|
||||
|
|
@ -7928,7 +7928,13 @@ pub struct LayoutObjectId(pub u128);
|
|||
Section~\ref{sec:graph:system-derived}. The fixed derivation is
|
||||
pinned for incremental-relayout correctness and provenance
|
||||
back-reference stability; its consumers are the solver and renderer
|
||||
(Track~A), not the interchange track.
|
||||
(Track~A), not the interchange track. Because these ids never enter
|
||||
document state, no stored or interchanged artifact depends on this
|
||||
derivation; the v0 reference crate accordingly mints layout ids with
|
||||
a provisional, untagged stand-in (synthesized objects borrowing the
|
||||
\texttt{"MUSCCONF"} tag), and wiring the \texttt{"MUSCLOID"}
|
||||
derivation above is Track~A work rather than a property the prototype
|
||||
yet realizes.
|
||||
\end{requirement}
|
||||
|
||||
\section{The Stage Pipeline}
|
||||
|
|
@ -13991,8 +13997,10 @@ state.
|
|||
pinned the \texttt{TransactionCategory} and \texttt{ObjectKind} core
|
||||
vocabularies; added \texttt{ResolutionAction::Dismiss} so the
|
||||
\texttt{Dismissed} resolution state is reachable by an authored
|
||||
operation; and pinned the (non-canonical) \texttt{LayoutObjectId}
|
||||
derivation with a \texttt{MUSCLOID} tag. \emph{Fixes:} blob hashing
|
||||
operation; and specified the (non-canonical) \texttt{LayoutObjectId}
|
||||
derivation with a \texttt{MUSCLOID} tag as the Track~A target (the v0
|
||||
prototype still mints provisional layout ids; wiring \texttt{MUSCLOID}
|
||||
is Track~A work). \emph{Fixes:} blob hashing
|
||||
is the bare \texttt{"MUSCBLOB" || payload} (deleted the
|
||||
contradictory ``identically to chunks'' phrasing); added the
|
||||
equal-generation superblock rule (\texttt{DivergentSameGeneration}
|
||||
|
|
|
|||
Loading…
Reference in New Issue