Repository navigation
Try making TLA operators opaque and use broadcast groups - #832
Open
Catoverflow wants to merge 6 commits into
Open
Catoverflow wants to merge 6 commits into
Catoverflow wants to merge 6 commits into
Conversation
Point verus_temporal_logic at a local ../verus-tla checkout whose temporal operators are opaque and whose rules are broadcast by default. - Replace execution-level reasoning in 21 functions (reveal of the temporal operators) with helper lemmas stated over state predicates. - Delete 752 TLA helper calls that the default rule group now applies automatically. - Use the renamed domain helpers (spec_entails_always_lift_state_forall_within_domain_equality, leads_to_always_lift_state_forall_pointwise_within_domain, tla_exists_lift_state_equality) and always_weaken in place of always_lift_state_weaken. - Add #[verifier::spinoff_prover] to two state-level lemmas whose proofs became unstable in the larger prover context. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Move the state-level preservation proof into lemma_vsts_guarantee_preserves_from_s_to_s_prime so that its query does not contain the temporal facts of the caller. With an extra broadcast axiom in that context (valid_always_equality, never instantiated) Z3 took a different search path and ran out of rlimit on every seed; the split module now verifies with 18M rlimit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
always_lift_state_weaken is now a default broadcast rule in verus-tla; all 61 always_weaken calls are redundant (936 verified, 0 errors). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
verus-tla no longer enables group_tla_rules by default, so every module that imports verus_temporal_logic now has a module-level `broadcast use verus_temporal_logic::rules::group_tla_rules;` (936 verified, 0 errors). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Temporarily depend on https://github.com/anvil-verifier/verus-tla (branch opaque-broadcast) instead of the local ../verus-tla patch, so CI verifies this branch. Revert to the default branch once that branch is merged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Keep the module-level broadcast use of group_tla_rules only in the 57 files whose proofs call verus-tla lemmas, plus vstatefulset_controller/proof/liveness/spec.rs, whose stability proofs rely on the rules after their explicit calls were removed. Spec-only modules and proof modules that do no temporal reasoning no longer use it (936 verified, 0 errors). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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.
No description provided.