feat(abi): S1 additive Verb discriminant — promote ASSERT/DECLARE/RETRACT

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>

Author: hyperpolymath

src/core/Checker.idr

@@ -172,7 +172,7 @@ mutual
   ||| payload — itself smaller than the enclosing `Expr`).
   public export
   statementFieldRefs : Statement -> List FieldRef
-  statementFieldRefs (MkStatement sel _ whr grp hav ord _ _ _ _ _ _ _ _) =
+  statementFieldRefs (MkStatement sel _ whr grp hav ord _ _ _ _ _ _ _ _ _) =
     let selRefs    : List FieldRef
         selRefs    = selItemsFieldRefs sel
         whereRefs  : List FieldRef

src/core/Composition.idr

@@ -187,6 +187,7 @@ composeJoin q1 q2 = MkStatement
   (joinLinear (linearAnnot q1) (linearAnnot q2))
   (joinEpistemic (epistemicClause q1) (epistemicClause q2))
   (requestedLevel q1)
+  (verb q1)                                      -- join inherits the left verb
 
 ||| Two queries are composable if they target the same source octad.
 public export

src/core/Grammar.idr

@@ -298,6 +298,13 @@ mutual
   -- Statement (top-level query)
   -- ═══════════════════════════════════════════════════════════════════════
 
+  ||| The VCL statement verb (consonance surface, S1). The read verbs
+  ||| (VSelect/VInspect/VVerify) carry the existing relational semantics;
+  ||| the mutating verbs (VAssert/VDeclare/VRetract) are parsed as tags over
+  ||| the same body. MERGE/SPLIT/NORMALISE stay unmodelled (fail-closed).
+  public export
+  data Verb = VSelect | VInspect | VVerify | VAssert | VDeclare | VRetract
+
   ||| A complete VCL-total query statement.
   public export
   record Statement where
@@ -319,6 +326,9 @@ mutual
     epistemicClause : Maybe EpistemicClause  -- Level 10: epistemic safety
     -- Metadata
     requestedLevel : SafetyLevel
+    -- VCL consonance verb (S1). Every L0..L10 predicate accesses Statement
+    -- by named field and ignores `verb`, so adding it is proof-preserving.
+    verb            : Verb
 
 -- ═══════════════════════════════════════════════════════════════════════
 -- Injection-safety primitive (canonical single source of truth)
@@ -364,9 +374,9 @@ data HasSelectItems : Statement -> Type where
 ||| Proof that a statement has a valid source.
 public export
 data HasSource : Statement -> Type where
-  OctadSource : HasSource (MkStatement _ (SrcOctad _) _ _ _ _ _ _ _ _ _ _ _ _)
-  FederationSource : HasSource (MkStatement _ (SrcFederation _) _ _ _ _ _ _ _ _ _ _ _ _)
-  StoreSource : HasSource (MkStatement _ (SrcStore _) _ _ _ _ _ _ _ _ _ _ _ _)
+  OctadSource : HasSource (MkStatement _ (SrcOctad _) _ _ _ _ _ _ _ _ _ _ _ _ _)
+  FederationSource : HasSource (MkStatement _ (SrcFederation _) _ _ _ _ _ _ _ _ _ _ _ _ _)
+  StoreSource : HasSource (MkStatement _ (SrcStore _) _ _ _ _ _ _ _ _ _ _ _ _ _)
 
 ||| Proof that a statement requesting Level 6+ has a LIMIT clause.
 public export

src/interface/WireConformance.idr

@@ -50,7 +50,7 @@ expected1 =
   MkStatement [SelStar] (SrcStore "main")
     Nothing [] Nothing [] Nothing Nothing
     Nothing Nothing Nothing Nothing Nothing
-    SchemaBound
+    SchemaBound VSelect
 
 conform1 : fromWire WireConformance.golden1 = Right WireConformance.expected1
 conform1 = Refl
@@ -82,7 +82,7 @@ expected2 =
     (Just (EpClause
              [AgEngine, AgProver "lean4"]
              [EpReqKnows AgEngine (ELiteral (LitBool True) TAny)]))
-    EpistemicSafe
+    EpistemicSafe VSelect
 
 conform2 : fromWire WireConformance.golden2 = Right WireConformance.expected2
 conform2 = Refl
@@ -98,7 +98,7 @@ expected3 =
     (Just (ELiteral (LitFloat 2.5) TAny))
     [] Nothing [] Nothing Nothing
     Nothing Nothing Nothing Nothing Nothing
-    ParseSafe
+    ParseSafe VSelect
 
 conform3 : fromWire WireConformance.golden3 = Right WireConformance.expected3
 conform3 = Refl

src/interface/WireDecode.idr

@@ -618,7 +618,9 @@ mutual
     (la,  r12) <- decOpt (\x => decLinear x) r11
     (ep,  r13) <- decOpt (decEpiClause k) r12
     (lvl, r14) <- decSafety r13
-    Right (MkStatement sel src wc gb hav ob lim off pf ef vc la ep lvl, r14)
+    -- `verb` is not carried on the wire (S1): decode defaults to VSelect, the
+    -- read sense, keeping the byte format and the WireConformance Refls stable.
+    Right (MkStatement sel src wc gb hav ob lim off pf ef vc la ep lvl VSelect, r14)
 
 -- ═══════════════════════════════════════════════════════════════════════
 -- Header + entry point

src/interface/parse/src/ast.rs

@@ -207,6 +207,20 @@ pub enum SafetyLevel {
     EpistemicSafe = 10,
 }
 
+/// `Grammar.idr`: `data Verb`. Read verbs (`Select`/`Inspect`/`Verify`) carry
+/// the existing relational semantics; the mutating verbs (`Assert`/`Declare`/
+/// `Retract`) are parsed as tags over the same body (S1). `Merge`/`Split`/
+/// `Normalise` stay unmodelled (fail-closed in the parser).
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Verb {
+    Select,
+    Inspect,
+    Verify,
+    Assert,
+    Declare,
+    Retract,
+}
+
 /// `Grammar.idr`: `record Statement` (`orderBy` is `(field, ascending?)`;
 /// Idris `Nat` limit/offset -> `u64`).
 #[derive(Debug, Clone, PartialEq)]
@@ -225,4 +239,6 @@ pub struct Statement {
     pub linear_annot: Option<LinearAnnotation>,
     pub epistemic_clause: Option<EpistemicClause>,
     pub requested_level: SafetyLevel,
+    /// VCL consonance verb (S1) — mirrors `Grammar.idr`'s additive `verb`.
+    pub verb: Verb,
 }

src/interface/parse/src/parser.rs

@@ -110,12 +110,30 @@ pub fn parse(input: &str) -> Result<Statement, ParseError> {
 }
 
 fn parse_statement(p: &mut P) -> Result<Statement, ParseError> {
-    // Accept SELECT (legacy) and INSPECT (VCL epistemic read request) interchangeably.
-    if p.is_kw("INSPECT") || p.is_kw("VERIFY") {
+    // VCL consonance verb (S1). The read verbs (SELECT legacy / INSPECT /
+    // VERIFY) and the promoted mutating verbs (ASSERT / DECLARE / RETRACT) all
+    // parse as a tag over the same relational body. MERGE / SPLIT / NORMALISE
+    // are deliberately NOT accepted, so they fail-closed (their semantics are
+    // S2, multi-subject / result-less).
+    let verb = if p.is_kw("INSPECT") {
         p.bump();
+        Verb::Inspect
+    } else if p.is_kw("VERIFY") {
+        p.bump();
+        Verb::Verify
+    } else if p.is_kw("ASSERT") {
+        p.bump();
+        Verb::Assert
+    } else if p.is_kw("DECLARE") {
+        p.bump();
+        Verb::Declare
+    } else if p.is_kw("RETRACT") {
+        p.bump();
+        Verb::Retract
     } else {
         p.eat_kw("SELECT")?;
-    }
+        Verb::Select
+    };
     let select_items = parse_select_items(p)?;
     p.eat_kw("FROM")?;
     let source = parse_source(p)?;
@@ -179,6 +197,7 @@ fn parse_statement(p: &mut P) -> Result<Statement, ParseError> {
         linear_annot: None,
         epistemic_clause: None,
         requested_level: SafetyLevel::ParseSafe,
+        verb,
     };
     stmt.requested_level = infer_requested_level(&stmt);
     Ok(stmt)

src/interface/parse/src/wire.rs

@@ -845,6 +845,9 @@ fn dec_stmt(d: &mut D) -> Result<Statement, WireError> {
         linear_annot,
         epistemic_clause,
         requested_level,
+        // `verb` is not carried on the wire (S1): default to the read sense,
+        // matching `WireDecode.idr`, so the byte format stays stable.
+        verb: Verb::Select,
     })
 }
 

src/interface/parse/tests/conformance_emit.rs

@@ -94,6 +94,7 @@ fn f1() -> Statement {
         linear_annot: None,
         epistemic_clause: None,
         requested_level: SafetyLevel::SchemaBound,
+        verb: Verb::Select,
     }
 }
 
@@ -138,6 +139,7 @@ fn f2() -> Statement {
             )],
         }),
         requested_level: SafetyLevel::EpistemicSafe,
+        verb: Verb::Select,
     }
 }
 
@@ -157,6 +159,7 @@ fn f3() -> Statement {
         linear_annot: None,
         epistemic_clause: None,
         requested_level: SafetyLevel::ParseSafe,
+        verb: Verb::Select,
     }
 }
 

src/interface/parse/tests/gate.rs

@@ -16,7 +16,7 @@
 )]
 
 use vcltotal_parse::{
-    ast::Modality,
+    ast::{Modality, Verb},
     certified_level, parse,
     schema::{FieldDef, ModalitySchema, OctadSchema, VqlType},
 };
@@ -49,13 +49,13 @@ fn schema_with_graph_fields(fields: Vec<FieldDef>) -> OctadSchema {
 
 // ── Fixture 1: Admitted ────────────────────────────────────────────────────
 //
-// Contract §"Worked examples" — Admitted:
-//   INSPECT GRAPH.knows FROM HEXAD 'e-1' WHERE depth < 3 LIMIT 10
+// Contract §"Worked examples" — Admitted (vclt-gate-contract.adoc:86):
+//   ASSERT GRAPH.knows FROM HEXAD 'e-1' WHERE depth < 3 LIMIT 10
 //   schema: graph.depth TInt non-null, graph.knows TOctad non-null
 //   expected: admissible=true, certified_level=6, levels 1-6 all pass, exit 0.
 
 #[test]
-fn fixture_admitted_inspect_with_limit() {
+fn fixture_admitted_assert_with_limit() {
     let schema = schema_with_graph_fields(vec![
         FieldDef {
             name: "depth".to_string(),
@@ -70,10 +70,14 @@ fn fixture_admitted_inspect_with_limit() {
             indexed: true,
         },
     ]);
-    // P5a parser uses SELECT/INSPECT; field refs need MODALITY.name qualification;
-    // bare `depth` is parsed as Expr::Param (schema-unresolved) — passes L1 vacuously.
-    let stmt = parse("INSPECT GRAPH.knows FROM HEXAD 'e-1' WHERE depth < 3 LIMIT 10")
+    // S1: the contract's worked example uses the ASSERT consonance verb, which
+    // now parses as a verb tag over the relational body (previously this fixture
+    // had to rewrite ASSERT->INSPECT because the parser could not parse ASSERT).
+    // Field refs need MODALITY.name qualification; bare `depth` parses as
+    // Expr::Param (schema-unresolved) — passes L1 vacuously.
+    let stmt = parse("ASSERT GRAPH.knows FROM HEXAD 'e-1' WHERE depth < 3 LIMIT 10")
         .expect("fixture 1 must parse");
+    assert_eq!(stmt.verb, Verb::Assert, "the ASSERT verb tag must be captured");
     let cert = certified_level(&stmt, &schema);
     assert_eq!(
         cert, 6,
@@ -160,3 +164,30 @@ fn parse_error_on_empty_input() {
 fn parse_error_on_garbage() {
     assert!(parse("'); DROP TABLE --").is_err());
 }
+
+// ── S1: consonance-verb discriminant ────────────────────────────────────────
+// The read verbs (SELECT/INSPECT/VERIFY) and the promoted mutating verbs
+// (ASSERT/DECLARE/RETRACT) parse as a verb tag over the same relational body;
+// MERGE/SPLIT/NORMALISE are deliberately fail-closed until their semantics (S2).
+#[test]
+fn s1_verb_tags_and_fail_closed() {
+    let body = "GRAPH.knows FROM STORE main";
+    for (kw, want) in [
+        ("SELECT", Verb::Select),
+        ("INSPECT", Verb::Inspect),
+        ("VERIFY", Verb::Verify),
+        ("ASSERT", Verb::Assert),
+        ("DECLARE", Verb::Declare),
+        ("RETRACT", Verb::Retract),
+    ] {
+        let stmt = parse(&format!("{kw} {body}"))
+            .unwrap_or_else(|e| panic!("{kw} should parse: {e:?}"));
+        assert_eq!(stmt.verb, want, "{kw} must carry the {want:?} tag");
+    }
+    for kw in ["MERGE", "SPLIT", "NORMALISE"] {
+        assert!(
+            parse(&format!("{kw} {body}")).is_err(),
+            "{kw} must fail-closed (S2, multi-subject / result-less semantics)"
+        );
+    }
+}