diff --git a/src/core/Checker.idr b/src/core/Checker.idr index c87ddae..909b161 100644 --- a/src/core/Checker.idr +++ b/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 diff --git a/src/core/Composition.idr b/src/core/Composition.idr index 4fae58c..0e0d585 100644 --- a/src/core/Composition.idr +++ b/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 diff --git a/src/core/Grammar.idr b/src/core/Grammar.idr index 97a23e1..17afa7c 100644 --- a/src/core/Grammar.idr +++ b/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 diff --git a/src/interface/WireConformance.idr b/src/interface/WireConformance.idr index 9d23abb..25f211a 100644 --- a/src/interface/WireConformance.idr +++ b/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 diff --git a/src/interface/WireDecode.idr b/src/interface/WireDecode.idr index a649318..384848f 100644 --- a/src/interface/WireDecode.idr +++ b/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 diff --git a/src/interface/parse/src/ast.rs b/src/interface/parse/src/ast.rs index d90964d..e21e616 100644 --- a/src/interface/parse/src/ast.rs +++ b/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, pub epistemic_clause: Option, pub requested_level: SafetyLevel, + /// VCL consonance verb (S1) — mirrors `Grammar.idr`'s additive `verb`. + pub verb: Verb, } diff --git a/src/interface/parse/src/parser.rs b/src/interface/parse/src/parser.rs index a711822..0b70dfe 100644 --- a/src/interface/parse/src/parser.rs +++ b/src/interface/parse/src/parser.rs @@ -110,12 +110,30 @@ pub fn parse(input: &str) -> Result { } fn parse_statement(p: &mut P) -> Result { - // 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 { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::ParseSafe, + verb, }; stmt.requested_level = infer_requested_level(&stmt); Ok(stmt) diff --git a/src/interface/parse/src/wire.rs b/src/interface/parse/src/wire.rs index c93cb08..675cb1d 100644 --- a/src/interface/parse/src/wire.rs +++ b/src/interface/parse/src/wire.rs @@ -845,6 +845,9 @@ fn dec_stmt(d: &mut D) -> Result { 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, }) } diff --git a/src/interface/parse/tests/conformance_emit.rs b/src/interface/parse/tests/conformance_emit.rs index 8f6871c..801568f 100644 --- a/src/interface/parse/tests/conformance_emit.rs +++ b/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, } } diff --git a/src/interface/parse/tests/gate.rs b/src/interface/parse/tests/gate.rs index 95a3d65..b9f9874 100644 --- a/src/interface/parse/tests/gate.rs +++ b/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) -> 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)" + ); + } +} diff --git a/src/interface/parse/tests/wire.rs b/src/interface/parse/tests/wire.rs index 3b2af09..da4619f 100644 --- a/src/interface/parse/tests/wire.rs +++ b/src/interface/parse/tests/wire.rs @@ -129,6 +129,7 @@ fn leaf_stmt() -> impl Strategy { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::ParseSafe, + verb: Verb::Select, }) } @@ -254,6 +255,7 @@ fn statement() -> impl Strategy { linear_annot: e.3, epistemic_clause: e.4, requested_level: e.5, + verb: Verb::Select, }) } @@ -307,6 +309,7 @@ fn golden_minimal() { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::SchemaBound, + verb: Verb::Select, }; let b = to_wire(&s); assert_eq!(&b[0..4], b"VCLW"); @@ -348,5 +351,6 @@ fn mk_float_stmt(f: f64) -> Statement { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::ParseSafe, + verb: Verb::Select, } }