refactor(seed): finalize minimal semantic core - #32
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR completes the semantic cleanup and minimization of ASET Seed.
It removes remaining legacy distinctions that were no longer represented by the normative wire model, sharpens the boundary between Seed-owned state and environment observations, makes the machine-readable operation model match the actual state-transition semantics, and further reduces the reachable formal state space without weakening Seed safety guarantees.
Main changes
Unified Authority recognition
The previous formal distinction between:
RequestAuthorityBindingsTerminalAuthorityBindingsis removed.
Seed now consumes a single exact-binding recognition relation:
RecognizedAuthorityBindingsThe same recognized
(authority, binding)relation is used for both request registration and terminal submission.This aligns the formal model with the normative wire representation and executable oracle, which already use one
ResolutionAuthorityBindingconcept.Concrete signatures, delegation chains, certificates, and recognition mechanisms remain outside the Seed semantic kernel.
Conflict observation constrained to valid terminal state
Environment conflicts can now be observed only for resolution identifiers that already have accepted terminal state.
This removes unreachable formal states such as:
The formal invariant now explicitly requires:
Conflict remains environment state and does not mutate Seed-owned state.
Accepted terminal uniqueness clarified
The previous broad
TerminalUniqueterminology is replaced by semantics that distinguish:This removes ambiguity between accepted canonical state and externally observed conflicting material.
Operations separated from state transitions
The machine-readable canon now models three Seed operations:
REGISTER_REQUEST— state transitionSUBMIT_RESOLUTION— state transitionEVALUATE_RESOLUTION— observerEVALUATE_RESOLUTIONis no longer structurally presented as a state transition.This aligns the machine-readable canon, documentation, executable semantics, and TLA model.
Machine canon schema cleanup
The active machine-readable schema is updated to the new operation-oriented representation.
Legacy
SEED-TX-*transition identifiers are replaced bySEED-OP-*operation identifiers where appropriate.The generated canon-to-TLA projection is updated to projection profile V5.
Standalone canon-to-TLA refinement preserved
SeedCanonProjection.tlaremains a standalone generated projection and does not depend on the handwrittenSeedResolutionmodule.The refinement proof explicitly relates the standalone machine-canon projection to the handwritten formal model.
Documentation and assurance cleanup
This PR also removes remaining active documentation inherited from earlier RC11/RC12 runtime-era architecture.
Notably:
Historical frozen evidence remains preserved.
Resulting semantic architecture
Formal state-space reduction
Before this final cleanup:
After constraining conflict observation and unifying Authority recognition:
The reduction comes from removing formally representable states that were not possible under the normative wire semantics.
Assurance
Executable bounded model:
Semantic mutations:
Python test suite:
TLC:
TLAPS:
Canon-to-TLA refinement:
Additional assurance:
Scope
This PR deliberately does not add higher-level mechanisms to Seed.
The following remain outside the minimal semantic kernel:
Seed consumes recognized boundary facts without prescribing how those facts are established.
Result
After this cleanup, the active Seed specification has:
This PR is intended to establish the minimal semantic baseline for the next Seed freeze rather than introduce new capabilities.