feat(abi): S1 additive Verb discriminant — promote ASSERT/DECLARE/RETRACT#60
Merged
Conversation
…RACT Add `data Verb = VSelect|VInspect|VVerify|VAssert|VDeclare|VRetract` and an additive `verb` field to both `Grammar.idr record Statement` (proof corpus) and the Rust `ast.rs` mirror. The parser promotes ASSERT/DECLARE/RETRACT as verb tags over the existing relational body; INSPECT/VERIFY already aliased SELECT; MERGE/SPLIT/NORMALISE stay fail-closed (S2 — multi-subject / result-less semantics). Additive-extension property demonstrated: ZERO proof edits. All L0..L10 soundness proofs and the WireConformance Refls stay green (the predicates access Statement by name and ignore `verb`); only the 9 construction/pattern sites needed the extra arg. `verb` is not carried on the wire — it defaults to VSelect on decode and in the conformance fixtures, so the byte format and the Refls are unchanged. Also closes the gate.rs silent ASSERT->INSPECT rewrite: the admitted fixture now parses the contract's actual ASSERT example (vclt-gate-contract.adoc:86) and asserts verb==Assert; adds s1_verb_tags_and_fail_closed. Verified: idris2 --build vclut-core.ipkg exit 0; cargo test 7/7 suites; honesty-guard Clean. Co-Authored-By: Claude Opus 4.8 (1M context) <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
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.
S1 — additive
Verbdiscriminant (hybrid/staged language path)Promotes the consonance verbs onto the proven relational core, per the hybrid language decision.
data Verb = VSelect | VInspect | VVerify | VAssert | VDeclare | VRetract+ an additiveverbfield to bothGrammar.idr record Statement(proof corpus) and the Rustast.rsmirror.ASSERT/DECLARE/RETRACTas verb tags over the same relational body;INSPECT/VERIFYalready aliasedSELECT;MERGE/SPLIT/NORMALISEfail-closed (S2 — multi-subject / result-less, need new semantics).gate.rssilentASSERT→INSPECTrewrite: the admitted fixture now parses the contract's realASSERTexample (vclt-gate-contract.adoc:86) and assertsverb == Assert; addss1_verb_tags_and_fail_closed.Additive-extension property — zero proof edits
The L0–L10 soundness proofs and the
WireConformanceRefls stay green untouched: the predicates accessStatementby name and ignoreverb, so only the 9 construction/pattern sites needed the extra arg.verbis not serialized (defaultsVSelecton decode and in the conformance fixtures), so the byte format and the Refls are stable.Verified locally
idris2 --build verification/proofs/vclut-core.ipkg→ exit 0 ·cargo test(parse crate) → 7/7 suites green ·honesty-guard.sh→ Clean.Next: S2 = genuine safety semantics for
MERGE/SPLIT/NORMALISE(multi-subject source / repair-only).🤖 Generated with Claude Code