Skip to content

Commit df1231c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
WIP vcl-ut PR-1: make VclTotal.* corpus type-check (Phase 2, 5/9 green)
Resurrects the never-compiled proof corpus so #20's in-situ L4 fix becomes machine-checkable. GREEN: ABI/Types, Core/{Grammar,Schema, Levels,Checker}. 0 proof-escapes; #20's MkNoRawUserInput preserved. Faithful fixes only (mutual blocks for forward refs, MkStatement pattern-match for totality, sound DecEq via injective tag, scoping hoists, relevant implicits) — each carries a ||| rationale. REMAINING (Phase 2): Composition proof tail (composeJoinFieldsSubset, elemAppendSplit), Epistemic parse error, ABI/{Foreign,Layout} paddingFor. Then Phase 3: ipkg + idris2 --check CI + refresh .machine_readable/badge. Refs hyperpolymath/standards#124. Not a PR yet — Phase 2 incomplete. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 89c64a1 commit df1231c

6 files changed

Lines changed: 555 additions & 417 deletions

File tree

‎src/core/Checker.idr‎

Lines changed: 76 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,18 @@ safetyLevelLabel EpistemicSafe = "L10:EpistemicSafe"
7676
-- Type Compatibility (decidable boolean check for Level 2)
7777
-- ═══════════════════════════════════════════════════════════════════════
7878

79+
||| Structural equality for Agent (ignoring payload for parameterised agents).
80+
||| Top-level so every `vqlTypeEq` clause can use it (a `where` binding is
81+
||| only in scope for the single clause it is attached to).
82+
public export
83+
agentEq : Agent -> Agent -> Bool
84+
agentEq AgEngine AgEngine = True
85+
agentEq (AgProver a) (AgProver b) = a == b
86+
agentEq AgValidator AgValidator = True
87+
agentEq (AgUser a) (AgUser b) = a == b
88+
agentEq AgFederation AgFederation = True
89+
agentEq _ _ = False
90+
7991
||| Decidable structural equality for VqlType.
8092
||| Returns True when two types are the same constructor with matching
8193
||| arguments — used by Level 2 to verify comparison operand types.
@@ -97,15 +109,6 @@ vqlTypeEq (TKnows a1 t1) (TKnows a2 t2) = agentEq a1 a2 && vqlTypeEq t1 t2
97109
vqlTypeEq (TBelieves a1 t1) (TBelieves a2 t2) = agentEq a1 a2 && vqlTypeEq t1 t2
98110
vqlTypeEq (TCommonKnowledge t1) (TCommonKnowledge t2) = vqlTypeEq t1 t2
99111
vqlTypeEq _ _ = False
100-
where
101-
||| Structural equality for Agent (ignoring payload for parameterised agents).
102-
agentEq : Agent -> Agent -> Bool
103-
agentEq AgEngine AgEngine = True
104-
agentEq (AgProver a) (AgProver b) = a == b
105-
agentEq AgValidator AgValidator = True
106-
agentEq (AgUser a) (AgUser b) = a == b
107-
agentEq AgFederation AgFederation = True
108-
agentEq _ _ = False
109112

110113
||| Check whether two VqlTypes are compatible for comparison.
111114
|||
@@ -134,46 +137,65 @@ typesCompatible a b =
134137
-- Field Reference Extraction
135138
-- ═══════════════════════════════════════════════════════════════════════
136139

137-
||| Recursively extract all FieldRef nodes from an expression tree.
138-
||| Traverses EField, ECompare, ELogic, EAggregate, and ESubquery nodes.
139-
public export
140-
extractFieldRefs : Expr -> List FieldRef
141-
extractFieldRefs (EField ref _) = [ref]
142-
extractFieldRefs (ELiteral _ _) = []
143-
extractFieldRefs (ECompare _ l r _) = extractFieldRefs l ++ extractFieldRefs r
144-
extractFieldRefs (ELogic _ l Nothing _) = extractFieldRefs l
145-
extractFieldRefs (ELogic _ l (Just r) _) = extractFieldRefs l ++ extractFieldRefs r
146-
extractFieldRefs (EAggregate _ e _) = extractFieldRefs e
147-
extractFieldRefs (EParam _ _) = []
148-
extractFieldRefs EStar = []
149-
extractFieldRefs (ESubquery sub) = statementFieldRefs sub
150-
extractFieldRefs (EEpistemic _ _ e _) = extractFieldRefs e
151-
extractFieldRefs (EAnnounce _ prop body _) =
152-
extractFieldRefs prop ++ extractFieldRefs body
153-
154-
||| Collect all field references from every clause of a statement.
155-
||| Delegates to extractFieldRefs for each expression-bearing clause.
156-
public export
157-
statementFieldRefs : Statement -> List FieldRef
158-
statementFieldRefs stmt =
159-
let selRefs : List FieldRef
160-
selRefs = concatMap selItemFieldRefs (selectItems stmt)
161-
whereRefs : List FieldRef
162-
whereRefs = maybe [] extractFieldRefs (whereClause stmt)
163-
groupRefs : List FieldRef
164-
groupRefs = groupBy stmt
165-
havingRefs : List FieldRef
166-
havingRefs = maybe [] extractFieldRefs (having stmt)
167-
orderRefs : List FieldRef
168-
orderRefs = map fst (orderBy stmt)
169-
in selRefs ++ whereRefs ++ groupRefs ++ havingRefs ++ orderRefs
170-
where
171-
||| Extract field references from a single SELECT item.
172-
selItemFieldRefs : SelectItem -> List FieldRef
173-
selItemFieldRefs (SelField ref) = [ref]
174-
selItemFieldRefs (SelModality _) = []
175-
selItemFieldRefs (SelAggregate _ e) = extractFieldRefs e
176-
selItemFieldRefs SelStar = []
140+
mutual
141+
||| Recursively extract all FieldRef nodes from an expression tree.
142+
||| Traverses EField, ECompare, ELogic, EAggregate, and ESubquery nodes.
143+
|||
144+
||| Mutually recursive with `statementFieldRefs` through `ESubquery`.
145+
||| All recursion is explicit structural descent (no `concatMap`/`maybe`/
146+
||| `map`) so the totality checker can see it terminates — every callee
147+
||| is applied to a strict sub-term of the constructor argument.
148+
public export
149+
extractFieldRefs : Expr -> List FieldRef
150+
extractFieldRefs (EField ref _) = [ref]
151+
extractFieldRefs (ELiteral _ _) = []
152+
extractFieldRefs (ECompare _ l r _) = extractFieldRefs l ++ extractFieldRefs r
153+
extractFieldRefs (ELogic _ l Nothing _) = extractFieldRefs l
154+
extractFieldRefs (ELogic _ l (Just r) _) = extractFieldRefs l ++ extractFieldRefs r
155+
extractFieldRefs (EAggregate _ e _) = extractFieldRefs e
156+
extractFieldRefs (EParam _ _) = []
157+
extractFieldRefs EStar = []
158+
extractFieldRefs (ESubquery sub) = statementFieldRefs sub
159+
extractFieldRefs (EEpistemic _ _ e _) = extractFieldRefs e
160+
extractFieldRefs (EAnnounce _ prop body _) =
161+
extractFieldRefs prop ++ extractFieldRefs body
162+
163+
||| Extract field references from a SELECT-item list (explicit recursion).
164+
public export
165+
selItemsFieldRefs : List SelectItem -> List FieldRef
166+
selItemsFieldRefs [] = []
167+
selItemsFieldRefs (SelField ref :: rest) = ref :: selItemsFieldRefs rest
168+
selItemsFieldRefs (SelModality _ :: rest) = selItemsFieldRefs rest
169+
selItemsFieldRefs (SelAggregate _ e :: rest) =
170+
extractFieldRefs e ++ selItemsFieldRefs rest
171+
selItemsFieldRefs (SelStar :: rest) = selItemsFieldRefs rest
172+
173+
||| Field refs of an optional clause expression (explicit, no `maybe`).
174+
public export
175+
optExprFieldRefs : Maybe Expr -> List FieldRef
176+
optExprFieldRefs Nothing = []
177+
optExprFieldRefs (Just e) = extractFieldRefs e
178+
179+
||| Projection of an ORDER BY list to its field refs (explicit, no `map`).
180+
public export
181+
orderByFieldRefs : List (FieldRef, Bool) -> List FieldRef
182+
orderByFieldRefs [] = []
183+
orderByFieldRefs ((f, _) :: xs) = f :: orderByFieldRefs xs
184+
185+
||| Collect all field references from every clause of a statement.
186+
||| Delegates to extractFieldRefs for each expression-bearing clause.
187+
||| Pattern-matches the `MkStatement` constructor rather than using field
188+
||| projections so the totality checker sees each clause as a strict
189+
||| sub-term of the statement (record projections defeat the size check
190+
||| across the `ESubquery` mutual edge).
191+
public export
192+
statementFieldRefs : Statement -> List FieldRef
193+
statementFieldRefs (MkStatement sel _ whr grp hav ord _ _ _ _ _ _ _ _) =
194+
selItemsFieldRefs sel
195+
++ optExprFieldRefs whr
196+
++ grp
197+
++ optExprFieldRefs hav
198+
++ orderByFieldRefs ord
177199

178200
-- ═══════════════════════════════════════════════════════════════════════
179201
-- Expression Scanning Helpers
@@ -617,11 +639,14 @@ runPipeline (lvl :: rest) stmt schema state =
617639
||| @schema The VeriSimDB octad schema to validate against.
618640
||| @return A CheckResult with the achieved safety level and diagnostics.
619641
public export
620-
checkQuery : Statement -> OctadSchema -> CheckResult
642+
checkQuery : Statement -> OctadSchema -> Checker.CheckResult
621643
checkQuery stmt schema =
622644
let initState : PipelineState
623645
initState = MkPipelineState ParseSafe [] []
624-
(finalState, mFailure) = runPipeline allLevels stmt schema initState
646+
res : (PipelineState, Maybe String)
647+
res = runPipeline allLevels stmt schema initState
648+
finalState : PipelineState
649+
finalState = fst res
625650
in case finalState.passed of
626651
[] =>
627652
-- Level 0 itself failed — should not happen (ParseSafe always passes)

‎src/core/Composition.idr‎

Lines changed: 21 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -41,14 +41,15 @@ import Data.List.Elem
4141
||| Appending an empty list on the right is a no-op.
4242
appendNilRight : (xs : List a) -> xs ++ [] = xs
4343
appendNilRight [] = Refl
44-
appendNilRight (_ :: xs) = cong (_ ::) (appendNilRight xs)
44+
appendNilRight (x :: xs) = cong (x ::) (appendNilRight xs)
4545

4646
||| map fst distributes over (++).
4747
mapFstAppend :
48+
{0 a, b : Type} ->
4849
(xs, ys : List (a, b)) ->
49-
map fst (xs ++ ys) = map fst xs ++ map fst ys
50+
map Builtin.fst (xs ++ ys) = map Builtin.fst xs ++ map Builtin.fst ys
5051
mapFstAppend [] _ = Refl
51-
mapFstAppend ((_ , _) :: xs) ys = cong (_ ::) (mapFstAppend xs ys)
52+
mapFstAppend ((k , _) :: xs) ys = cong (k ::) (mapFstAppend xs ys)
5253

5354
-- ── selectFieldRefs distributivity ──────────────────────────────────
5455

@@ -66,6 +67,16 @@ selectFieldRefsAppend (SelStar :: rest) items2 = selectFieldRefsAppend r
6667

6768
-- ── exprFieldRefs of the joined WHERE clause ─────────────────────────
6869

70+
||| Combine WHERE clauses with AND conjunction.
71+
||| Defined here (before its first use in the lemmas below) so the module
72+
||| type-checks top-down without a forward reference.
73+
export
74+
joinWhere : Maybe Expr -> Maybe Expr -> Maybe Expr
75+
joinWhere Nothing Nothing = Nothing
76+
joinWhere (Just w) Nothing = Just w
77+
joinWhere Nothing (Just w) = Just w
78+
joinWhere (Just w1) (Just w2) = Just (ELogic And w1 (Just w2) TBool)
79+
6980
||| When both WHERE clauses are Nothing, the join WHERE is Nothing.
7081
joinWhereNilNil : exprFieldRefs (joinWhere Nothing Nothing) = []
7182
joinWhereNilNil = Refl
@@ -82,7 +93,7 @@ joinWhereLNil :
8293
(w : Maybe Expr) ->
8394
exprFieldRefs (joinWhere w Nothing) = exprFieldRefs w
8495
joinWhereLNil Nothing = Refl
85-
joinWhereLNil (Just _) = appendNilRight _
96+
joinWhereLNil (Just _) = Refl
8697

8798
||| When both WHERE clauses are present, the join AND-conjoins them.
8899
||| Field refs of the AND expression are exactly the union of the two.
@@ -126,12 +137,17 @@ allFieldsBoundFromElem (ref :: refs) schema f =
126137

127138
||| AllFieldsBound respects list Subset (every element of xs appears in ys).
128139
||| Here Subset is: every member of xs is a member of ys.
140+
||| `xs` and `schema` are bound relevantly (not erased) because
141+
||| `allFieldsBoundFromElem` pattern-matches `refs := xs` and uses
142+
||| `schema` at the term level.
129143
allFieldsBoundSubset :
144+
{xs, ys : List FieldRef} ->
145+
{schema : OctadSchema} ->
130146
AllFieldsBound ys schema ->
131147
((ref : FieldRef) -> Elem ref xs -> Elem ref ys) ->
132148
AllFieldsBound xs schema
133149
allFieldsBoundSubset bound f =
134-
allFieldsBoundFromElem _ _ (\ref, prf => boundLookup bound (f ref prf))
150+
allFieldsBoundFromElem xs schema (\ref, prf => boundLookup bound (f ref prf))
135151

136152
-- ── Elem membership through (++) ────────────────────────────────────
137153

@@ -149,14 +165,6 @@ elemAppendRight (_ :: xs) e = There (elemAppendRight xs e)
149165
-- SECTION 2: Composition Operation
150166
-- ══════════════════════════════════════════════════════════════════════
151167

152-
||| Combine WHERE clauses with AND conjunction.
153-
export
154-
joinWhere : Maybe Expr -> Maybe Expr -> Maybe Expr
155-
joinWhere Nothing Nothing = Nothing
156-
joinWhere (Just w) Nothing = Just w
157-
joinWhere Nothing (Just w) = Just w
158-
joinWhere (Just w1) (Just w2) = Just (ELogic And w1 (Just w2) TBool)
159-
160168
||| Combine effect declarations: union of effects.
161169
joinEffects : Maybe EffectDecl -> Maybe EffectDecl -> Maybe EffectDecl
162170
joinEffects Nothing e = e

0 commit comments

Comments
 (0)