Freeze closed typed R3 semantic review implementation contract
This commit is contained in:
@@ -0,0 +1,187 @@
|
||||
# R3 semantic review implementation freeze — schema/source 5
|
||||
|
||||
Status: production implementation authorized; not accepted or complete. Isolated
|
||||
worktree `D:/CodexBuilds/Capella2-semantic-review`, branch `codex/semantic-review`,
|
||||
base `ab661f2d332f540673ee0e2003b454c1765332bc`; dedicated target
|
||||
`D:/CodexBuilds/Capella2-semantic-target`. R6 native work remains root-owned in DATA.
|
||||
|
||||
## Decision and evidence
|
||||
|
||||
Adopt C: a closed, typed, self-tagged review value per semantic facet. The
|
||||
throwaway C proof is `b2ab2b1feb9b0ada03cd9d0974749bd7fd28c7f8` in the separate
|
||||
transition-probe worktree. Its 11 passing tests comprise three B1 comparison
|
||||
cases and eight C cases, including an independent adversarial review's concrete
|
||||
counterexamples. Additional type/adapter code is accepted for fewer persisted
|
||||
state invariants; this is not a claim that C uses fewer lines.
|
||||
|
||||
This supersedes the recursive `SemanticValue`/string-path recommendation in
|
||||
release-transition-contract.md and the interim typed-carrier/mask/order-shadow
|
||||
recommendation. Keep its engineering requirements: partial deliberate review,
|
||||
explicit mapping, target-only preservation, honest unreviewed state, source/JSON
|
||||
parity, and one stale-checked validated transaction. No generic metamodel, graph
|
||||
synchronization service, runtime value tree, or second mutation engine is added.
|
||||
|
||||
## Persisted shape and granularity
|
||||
|
||||
`TraceBaseline` retains existing `oa`/`sa: TracedProperties` and adds
|
||||
`#[serde(default)] semantic: Option<SemanticBaseline>`. Old absence is Unreviewed;
|
||||
never synthesize historical semantic values from today's project. Baseline and
|
||||
Trace use PartialEq, because typed semantic values include finite f64.
|
||||
|
||||
`SemanticBaseline { facets: Vec<FacetReview> }` stores only independently reviewed
|
||||
facts. `FacetReview` is a closed self-tagged enum, nested by actual model family;
|
||||
each leaf carries `Reviewed<T> { oa: Observed<T>, sa: Observed<T> }`.
|
||||
`Observed<T>` is `NotApplicable | Value(T)`. T is fixed by the enum variant, reusing
|
||||
existing model types (DataValue, TypeRef, MessageValue, LifelineBinding, port/state
|
||||
enums and artifact metadata). No entry means Unreviewed. `Value(None)` is a real
|
||||
absent optional value, distinct from a missing constructor branch. Reject leaves
|
||||
inapplicable on both sides and selectors outside the compared record family.
|
||||
|
||||
Historical keys use `KeyPair<K> { oa: Option<K>, sa: Option<K> }` in canonical
|
||||
OA/SA coordinates. Annotation keys are the entire `(path, field)`; binding keys
|
||||
are the referenced lifeline. An annotation or binding is one atomic optional row;
|
||||
retargeting its key is explicit removal/addition, with no heuristic rename.
|
||||
Other rows remain independently reviewable. Scalar field defaults are one atomic
|
||||
optional vector because their repeated values have no stable identity.
|
||||
|
||||
Reference collection members and enum literals are individually reviewed facts.
|
||||
Enum keys are exact case-sensitive strings, not list indexes. Source collection
|
||||
Take applies additions/removals, preserving independently added target members.
|
||||
Ordering is its own typed Vec<Id> fact; membership acknowledgement never refreshes
|
||||
it. InterfaceItemAllocation order/protocols remain fields of the identified
|
||||
relation, not a second writable Interface.items list.
|
||||
|
||||
Constructor groups are explicit, narrow semantic scopes. Data definition owns
|
||||
its variant fields and coupled default; PortContract owns contract plus Legacy
|
||||
payload; Event owns its variant payload; Occurrence owns its variant payload but
|
||||
not common pre/postconditions. Nested MessageKind/Timer changes expose dependent
|
||||
exchange/reply/value changes. StateKind is a semantic structural choice even
|
||||
though it changes Element::kind(). Accept a discriminator switch and its whole
|
||||
introduced/removed group atomically, retiring obsolete branch facts. Unchanged
|
||||
kind cannot acknowledge unrelated bound/default drift by a Keep shortcut. An
|
||||
explicit actual target switch may reconsider an earlier deliberate Keep.
|
||||
|
||||
Artifact reviews are attached facts of the owning semantic trace; they do not
|
||||
widen ordinary Trace endpoint compatibility. Cover artifact membership and
|
||||
name/description/owner/relation/URI/revision/fragment, preserving target-only links.
|
||||
Do not fetch artifact content. Historical UUIDs remain after ordinary deletion,
|
||||
and explicit identity remapping visits keys and typed values without treating
|
||||
them as live graph edges.
|
||||
|
||||
## Complete field catalog
|
||||
|
||||
- Headers: existing name/description review; element parent. Identity, alias,
|
||||
layer and placements are not incidental semantic edits.
|
||||
- OA/SA primitive bodies have no payload; Process/FunctionalChain have step
|
||||
membership/order. Shared Machine/Region have no own payload.
|
||||
- ExchangeItem nature/mechanism/supertype; Interface supertype and independently
|
||||
identified allocation relations.
|
||||
- DataType constructor, integer/real bounds, string lengths, enum members,
|
||||
Record supertype, default and unit. DataField TypeRef, multiplicity bounds,
|
||||
unit, direction, storage and optional default vector.
|
||||
- Port constructor, function input/output item membership, component
|
||||
kind/orientation and Legacy direction/interface. Existing typed port generation,
|
||||
explicit resolution/split and unsupported OA mappings remain authoritative.
|
||||
- Scenario viewpoint/context/pre/postconditions/steps; Lifeline represented ref.
|
||||
- Occurrence constructor/common pre/postconditions; Exchange endpoints/reference,
|
||||
message kind/Timer expression, reply correlation and qualified annotations;
|
||||
Action refs; Control kind; SequenceReference; ScenarioUse ref/bindings; State
|
||||
refs; Fragment operator/branches; Branch guard/ordered occurrences.
|
||||
- Event Signal item membership, Time kind/expression, Change expression; State
|
||||
kind and entry/exit/do prose.
|
||||
- All relation source/target endpoints; interface allocation order/protocols;
|
||||
association roles/multiplicities/navigation; exchange item sets/ports/orientation;
|
||||
capability-extend condition; sequence guard; state-transition kind, trigger/effect
|
||||
sets and separate prose; StateAction phase. Other relation variants are endpoint-only.
|
||||
- Direct owned-child membership, incident relation identity with endpoint role,
|
||||
and attached artifact membership/properties. Rollups distinguish own drift from
|
||||
linked impact; shared referenced definitions are not copied into every baseline.
|
||||
|
||||
## Review and command boundary
|
||||
|
||||
Use the existing transition selection/dependency/mapping planner and ordinary
|
||||
Command preparation. Keep the prose request/API compatible; add sibling typed
|
||||
semantic request/preview/apply helpers. Whole existing typed records may appear
|
||||
as transient candidates or impact snapshots, never as persisted baseline carriers.
|
||||
|
||||
Freeze mappings before proposals. Resolve all live and historical reference
|
||||
members through explicit correspondence; no display-name matching. Many sources
|
||||
may affect a target only when resolved deltas agree for each canonical target
|
||||
slot. A source/key-pair collision or contradictory target delta is a conflict,
|
||||
independent of request order. Mapping changes require explicit invalidation/reset
|
||||
of affected old reviews; never silently replace or accumulate overlapping pairs.
|
||||
|
||||
Compare each side against its own reviewed value, retaining intentionally unequal
|
||||
pairs. Keep acknowledges only the selected current source/retained target fact.
|
||||
Take or a typed candidate acknowledges only the selected resulting fact. Untouched
|
||||
changes remain drift. Preview unreviewed differences rather than falsely claiming
|
||||
unchanged semantics. A selected constructor group names every fact it acknowledges.
|
||||
|
||||
Preserve target-only members and records. Removing source membership proposes
|
||||
unlinking, not deletion of target semantic objects. Ordered insertion is automatic
|
||||
only with a unique unchanged mapped anchor; ambiguous insertion/reorder requires
|
||||
an explicit final target order containing every surviving member once. Parent and
|
||||
relation endpoint edits remain explicit canonical operations, with aggregate
|
||||
membership effects linked to those same operations rather than competing commands.
|
||||
|
||||
Prepare one complete candidate, then compare the actual prepared project against
|
||||
the explicitly reviewed result. Existing cleanup (including inherited annotation
|
||||
pruning) can cause additional changes: expose their exact typed before/after
|
||||
impact and require explicit review. Cancellation, stale fingerprint/ETag, missing
|
||||
resolution or invalid candidate leaves model, baseline, revision/history and disk
|
||||
unchanged. Baseline updates join the same ordinary atomic transaction. Repeated
|
||||
application is idempotent. The plan is still a client candidate, not a security
|
||||
receipt; ordinary validation is never bypassed.
|
||||
|
||||
## Source/schema handoff and ownership
|
||||
|
||||
Core owns model/types, the closed semantic catalog/helpers, transition integration,
|
||||
reference/remap/admission validation, lib registration and semantic core tests.
|
||||
Source worker owns persistence.rs version dispatch, language/source_project/source
|
||||
files, V4 compatibility migration and source/migration tests. Desktop/server are
|
||||
later separate integrations. Communicate compiled public types before dependent
|
||||
source edits. Coordinate the dedicated target; no concurrent Cargo mutations.
|
||||
|
||||
Agreed internal helper, rooted at SemanticBaseline's serde tree:
|
||||
|
||||
```rust
|
||||
pub(crate) enum HistoricalSourceKind { Reference, Enum }
|
||||
pub(crate) fn historical_source_slots(
|
||||
baseline: &SemanticBaseline,
|
||||
) -> Vec<(Vec<String>, HistoricalSourceKind)>;
|
||||
```
|
||||
|
||||
Paths are internal field names/list indexes, never persisted or public SemanticPath.
|
||||
Core derives slots from the same finite typed leaf catalog, including nested Id,
|
||||
model enums, Option/Vec, annotations/bindings and NotApplicable observations.
|
||||
Source can normalize historical AST leaves to temporary JSON, deserialize the
|
||||
existing typed SemanticBaseline, then check original token classes with this map.
|
||||
References require an explicit historical `uuid "..."`; enum leaves require bare
|
||||
words; other string leaves require quotes. Historical @alias is rejected. This
|
||||
handles Reviewed oa/sa text fields without weakening existing live @alias rules.
|
||||
Formatting and token/comment identity use the same slot metadata.
|
||||
|
||||
Schema/source5 is explicit. V4 migration freezes only changed Trace/TraceBaseline
|
||||
shapes plus the closed old constructor catalog, reusing unchanged typed model
|
||||
records; retain V1/V2/V3 adapters and real compatibility fixtures. No public
|
||||
intermediate5 acceptance before full catalog, baseline roundtrip, source/JSON/API
|
||||
agreement and coupled persistence are verified. Earlier source/data4 remains real
|
||||
compatibility input, not a silently mutable contract.
|
||||
|
||||
## Verification gates
|
||||
|
||||
First close pure types/catalog/drift and typed source admission, then mapped review
|
||||
and complete atomic preparation. Cover every listed field family with observed
|
||||
mutations, including both directions and same-kind counterparts. Required focused
|
||||
cases: partial Keep/Take; constructors/defaults/units; row identity and changed old
|
||||
deleted references; target-only fields/triggers/literals/bindings/artifacts; order
|
||||
ambiguity; mapping reset and agreeing/conflicting many-to-one slots; wrong-family
|
||||
and both-side-NA admission; old semantic absence; prepared cleanup impacts; stale
|
||||
plan; duplicate decisions; no-op acknowledgement; repeat apply; undo/redo and invalid
|
||||
rollback. Test finite bounds and bounded nested/historical reference work.
|
||||
|
||||
Then source/JSON historical UUID and mixed-constructor roundtrip, explicit migration,
|
||||
comment/identity preservation, actual REST ETag/disk/restart, native compact/normal
|
||||
review UI, independent semantics/correctness review and Windows/Linux verification.
|
||||
Do not quietly reduce this to scalar-only reconciliation. Incremental commits are
|
||||
implementation checkpoints, not release acceptance.
|
||||
Reference in New Issue
Block a user