feat: prove cross-entity read-guards in composite verify - #420
Draft
rita-aga wants to merge 13 commits into
Draft
Conversation
Composite seed cover and plan scope now close over cross_entity_state guards, not only trigger edges, so a guard that only reads another entity is concrete in the joint model. INCOMPLETE fails the command. temper verify accepts repeated --specs-dir so two apps compose into one joint proof.
Keeps the production file under the 500-line ratchet after the multi-dir composite proof landed.
A default max_counter of 2 made CompleteResearch (min 3 directions) unsatisfiable. Scan MinCount/MaxCount/ListLengthMin and inhabit that universe so a machine the spec can run is a machine the checker can too.
Plan-build failure (unknown trigger target) was printed as "BFS budget exhausted" with 0 states. That hid the real finding: CurationDirection joins DesignLanguage, which is not in a curation-only --specs-dir. Print other_violations instead.
Axum's 2MiB default 413'd a synthesize trajectory (8.6MiB). Same class as blob ingest.
…e states Composite BFS was Incomplete on fat catalog types because the joint vector carried every local bool/counter/list and Stateright's target_state_count counted generated edges. Project each entity to the fields the join actually reads (status) and walk unique joint states. Katagami both-dirs: 342176 unique, VERIFIED, no dropped reactions.
Regression that the status-join composite is not vacuous: firing ReviewAgent.RecordVerdict from DesignLanguage.SubmitForReview while the reviewer is still SubmissionReceived must be VIOLATED.
…join Stateright eventually ignored `from`, so QueryEventuallyResolves was true at initial Idle even when ReadingQuery was a trap. Check that every reachable `from` status can still reach a target. never(Published) with Publish enabled was already caught; add the regression tests.
A join can fail AssignmentEventuallyResolved with zero drops. The exit line must say which property failed.
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
1 participant
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.
Why
temper verifytreated across_entity_stateguard as a free boolean unless a trigger connected the two entities. A guard that only reads another type (Katagami:CompleteSynthesisrequiresDesignLanguageUnderReview) never entered the joint model. INCOMPLETE also exited 0.Rita: the joint proof has to finish at spec-check time. Runtime 409 is not that proof.
What
cross_entity_stateguards as well as trigger edges.temper verify --specs-dir A --specs-dir Bunions both apps into one composite (curation + commons).[File, Workspace], 4 joint states, VERIFIED.Not in this PR
Instance multiplicity (N copies of one type in the joint BFS). That is not required for the Katagami actor experiment. Runtime already creates N directions.
Test plan
cargo test -p temper-verify --lib compositecargo test -p temper-cli