- 1. Overview
- 2. Notation
- 3. Syntax (Abstract)
- 4. Type System (Static Semantics)
- 5. Operational Semantics (Dynamic Semantics)
- 6. Proof Obligations (Dependent-Type Path)
- 7. Soundness Theorem
- 8. Semantic Equivalence
- 9. Drift Semantics
- 10. Denotational Semantics (Alternative View)
- 11. Future Extensions
- 12. References
This document specifies the formal operational semantics and static type system for VeriSim Query Language (VQL). VQL has two execution paths with different semantic guarantees:
-
Dependent-Type Path - Queries with
PROOFclause, formally verified via ZKP -
Slipstream Path - Queries without
PROOFclause, fast but unverified
We use standard mathematical notation for formal semantics:
| Notation | Meaning |
|---|---|
\(\Gamma\) |
Type environment (context) |
\(\Gamma \vdash e : \tau\) |
Expression |
\(e \Rightarrow v\) |
Expression |
\(e \rightarrow e'\) |
Expression |
\(\llbracket e \rrbracket_{\rho}\) |
Denotational semantics of |
\(\pi : \phi\) |
Proof term \(\pi\) for proposition \(\phi\) |
\(\{x : \tau \mid \phi(x)\}\) |
Refinement type: values of type \(\tau\) satisfying predicate \(\phi\) |
We define the abstract syntax of VQL (concrete syntax in vql-grammar.ebnf):
Query ::= SELECT Modalities FROM Source [WHERE Condition]
[PROOF ProofSpec] [LIMIT Int] [OFFSET Int]
Modalities ::= * | Modality, ...
Modality ::= GRAPH | VECTOR | TENSOR | SEMANTIC | DOCUMENT | TEMPORAL
Source ::= HEXAD UUID
| FEDERATION Pattern [WITH DRIFT DriftMode]
| STORE ID
Condition ::= SimpleCond | CompoundCond | (Condition)
SimpleCond ::= GraphCond | VectorCond | TensorCond | ...
CompoundCond::= Condition AND Condition
| Condition OR Condition
| NOT Condition
ProofSpec ::= ProofType(Contract) [WITH Params]
ProofType ::= EXISTENCE | CITATION | ACCESS | INTEGRITY | PROVENANCE | CUSTOM
VQL has the following base types:
τ ::= UUID -- 128-bit identifier
| String -- UTF-8 string
| Int -- Integer
| Float -- IEEE 754 double
| Bool -- Boolean
| Vector[n] -- n-dimensional vector
| Tensor[d₁, ..., dₙ] -- n-dimensional tensor
| Timestamp -- ISO 8601 datetime
| RDFTriple -- (subject, predicate, object)
| OctadRef -- Reference to a Octad
| Modality -- GRAPH | VECTOR | TENSOR | ...
| Proof[φ] -- Proof of proposition φ
Each modality has an associated type projection:
A Octad is a dependent product over modalities:
Where \(\text{Valid}(h, m)\) asserts that octad h has a valid representation in modality m.
A query result has a refinement type that depends on the modalities selected:
Where \(\mathcal{M} \subseteq \{\text{GRAPH}, \text{VECTOR}, \ldots\}\) and:
For queries with PROOF clause, the result type includes a proof term:
Where \(\phi\) is the proposition specified by the PROOF clause.
Interpretation: A slipstream query returns a list of octads with selected modalities, without proof guarantees.
Interpretation: A dependent-type query returns results with proof that the contract \(\phi_{\text{proof-spec}}\) holds.
We define two evaluation environments:
-
Store Environment \(\Sigma\): Maps UUIDs to Octad data
-
Proof Environment \(\Pi\): Maps contracts to proof functions
Interpretation: 1. Retrieve candidate octads from source 2. Filter by condition 3. Project to selected modalities 4. No proof generation
Interpretation: 1. Same filtering as slipstream path 2. Generate proof \(\pi\) that contract holds 3. Return results with proof term
Where \(\pi_{\exists}\) is a ZKP proving existence without revealing data.
For federated queries with drift, we model evaluation as a state machine:
For each proof type, we specify the proposition \(\phi\) that must be proven:
Informal: The octad exists in at least one store and is accessible to the querier.
Informal: All citations are valid and cited octads exist.
Informal: User u has read permission for octad h.
Informal: Data has not been tampered with since commitment.
For dependent-type queries, VQL delegates to proven-library (external ZKP framework):
Where:
- \(\phi_{\text{proof-spec}}\) is the proposition from the contract
- R is the query result (public input)
- witness is private data used for proof construction
Theorem (Slipstream Correctness):
If \(\Gamma \vdash Q : \text{QueryResult}[\mathcal{M}\)] and \(\llbracket Q \rrbracket_\Sigma = R\), then:
Informal: All results are valid projections from the store (but no additional guarantees).
Theorem (Dependent-Type Soundness):
If \(\Gamma \vdash Q : \text{ProvedResult}[\mathcal{M}, \phi\)] and \(\llbracket Q \rrbracket_{\Sigma,\Pi} = (R, \pi)\), then:
Informal: The proof term \(\pi\) is a valid proof of proposition \(\phi\) applied to results R, and it verifies correctly.
Proof sketch: By induction on the derivation of \(\Gamma \vdash Q : \text{ProvedResult}[\mathcal{M}, \phi\)]. The critical step uses the soundness of the underlying ZKP system (proven-library).
Two queries \(Q_1\) and \(Q_2\) are semantically equivalent (\(Q_1 \equiv Q_2\)) if:
Example equivalences:
-
Commutativity of AND:
\[\texttt{WHERE } C_1 \texttt{ AND } C_2 \equiv \texttt{WHERE } C_2 \texttt{ AND } C_1\] -
Idempotence of modality selection:
\[\texttt{SELECT GRAPH, GRAPH} \equiv \texttt{SELECT GRAPH}\] -
Filter distribution:
\[\texttt{WHERE } C_1 \texttt{ AND } (C_2 \texttt{ OR } C_3) \equiv (\texttt{WHERE } C_1 \texttt{ AND } C_2) \texttt{ OR } (\texttt{WHERE } C_1 \texttt{ AND } C_3)\]
We define a consistency lattice for federated queries:
Where \(A \sqsubset B\) means "A provides stronger guarantees than B".
For federated queries with drift mode \(D\):
Where \(\text{merge}_D\) implements the drift policy:
We can also give a denotational semantics by interpreting queries as functions on stores:
Where \(\mathcal{P}(\text{Octad})\) is the powerset of octads.
Conditions compose via logical operators:
Future versions may support refinement predicates in query syntax:
SELECT GRAPH, VECTOR
FROM verisim:semantic
WHERE octad : {h : Octad | citationCount(h) > 10}
LIMIT 100;Formal type:
-
Pierce, B. C. (2002). Types and Programming Languages. MIT Press.
-
Chlipala, A. (2013). Certified Programming with Dependent Types. MIT Press.
-
Boneh & Shoup. A Graduate Course in Applied Cryptography (ZKP foundations)