Master doc: docs/shaping/normative-ir-slices.md — authoritative for scope, slice order, and per-slice affordances. docs/shaping/normative-ir-shaping.md is authoritative for requirements, Shape E, the fit check, and the breadboard.
Outcome: ACS's normative prose becomes a machine-checked requirement catalog. Opaque stable anchors on each atomic provision, a generated manifest joined to an authored semantic layer, and typed predicates compiled to two independently executed engines held equivalent by differential CI — so the chain normative prose ↕ requirement ID ↕ formal predicate ↕ executable verifier ↕ conformance test holds end to end, and a definition change can invalidate an unchanged MUST.
Stops at: IR V8, upstream markers merged. The TLA+ model and the Lean faithfulness proof stay parked.
Slice IDs are IR Vn here because #1 already owns Vn; each maps 1:1 to §Vn in the master doc. Sibling to #1 — different work stream, same repo, no shared code (R8.2).
Master doc:
docs/shaping/normative-ir-slices.md— authoritative for scope, slice order, and per-slice affordances.docs/shaping/normative-ir-shaping.mdis authoritative for requirements, Shape E, the fit check, and the breadboard.Outcome: ACS's normative prose becomes a machine-checked requirement catalog. Opaque stable anchors on each atomic provision, a generated manifest joined to an authored semantic layer, and typed predicates compiled to two independently executed engines held equivalent by differential CI — so the chain
normative prose ↕ requirement ID ↕ formal predicate ↕ executable verifier ↕ conformance testholds end to end, and a definition change can invalidate an unchangedMUST.Stops at: IR V8, upstream markers merged. The TLA+ model and the Lean faithfulness proof stay parked.
Slice IDs are
IR Vnhere because #1 already ownsVn; each maps 1:1 to§Vnin the master doc. Sibling to #1 — different work stream, same repo, no shared code (R8.2).