diff options
Diffstat (limited to 'proof')
| -rw-r--r-- | proof/.gitignore | 11 | ||||
| -rw-r--r-- | proof/Drl.v | 67 | ||||
| -rw-r--r-- | proof/Extraction.v | 17 | ||||
| -rw-r--r-- | proof/Makefile | 14 | ||||
| -rw-r--r-- | proof/Relation.v | 26 | ||||
| -rw-r--r-- | proof/Schema.v | 5 | ||||
| -rw-r--r-- | proof/_CoqProject | 6 | ||||
| -rw-r--r-- | proof/drl_verified.ml | 410 |
8 files changed, 556 insertions, 0 deletions
diff --git a/proof/.gitignore b/proof/.gitignore new file mode 100644 index 0000000..5ff7fe7 --- /dev/null +++ b/proof/.gitignore @@ -0,0 +1,11 @@ +# Coq build artifacts +*.vo +*.vos +*.vok +*.glob +*.aux +.*.aux +Makefile.coq +Makefile.coq.conf +.Makefile.coq.d +.coqdeps.d diff --git a/proof/Drl.v b/proof/Drl.v new file mode 100644 index 0000000..fd179a1 --- /dev/null +++ b/proof/Drl.v @@ -0,0 +1,67 @@ +(** * DRL: Data Retrieval Language — Finiteness Gate + + This file defines: + - The DRL query AST (mirroring [lib/drl/ast.ml]) + - [predicted_finite]: statically decides whether a query can + produce an infinite result based on the cardinality flags of + the relations it references. + + [predicted_finite] is extracted to OCaml and called by + [lib/drl/gate.ml] before every query execution. Queries whose + result cannot be statically proven finite are rejected unless + wrapped in a [Take]. *) + +From Stdlib Require Import List. +From Stdlib Require Import String. +From Stdlib Require Import Bool. +Require Import Schema. +Require Import Relation. +Import ListNotations. + +(* ================================================================== *) +(** ** AST *) +(* ================================================================== *) + +Inductive literal := + | LitInt : nat -> literal + | LitStr : string -> literal + | LitBool : bool -> literal. + +Inductive query : Type := + | Base : string -> query + | Const : list (attr_name * literal) -> query + | Select : query -> query -> query + | Join : list attr_name -> query -> query -> query + | Cartesian : query -> query -> query + | Project : list attr_name -> query -> query + | Rename : list (attr_name * attr_name) -> query -> query + | Union : query -> query -> query + | Diff : query -> query -> query + | Take : nat -> query -> query. + +(* ================================================================== *) +(** ** Finiteness Prediction *) +(* ================================================================== *) + +(** Conservatively predict whether a query produces a finite result. + Returns [Some true] if guaranteed finite, [Some false] if not, + [None] if a referenced relation is not found in the database. *) +Fixpoint predicted_finite (db : database) (q : query) : option bool := + match q with + | Base name => + match db_lookup name db with + | Some r => Some (rel_finite r) + | None => None + end + | Const _ => Some true + | Take _ _ => Some true + | Select _ source => + predicted_finite db source + | Join _ q1 q2 | Cartesian q1 q2 | Union q1 q2 => + match predicted_finite db q1, predicted_finite db q2 with + | Some f1, Some f2 => Some (f1 && f2) + | _, _ => None + end + | Diff q1 _ => predicted_finite db q1 + | Project _ q' | Rename _ q' => predicted_finite db q' + end. diff --git a/proof/Extraction.v b/proof/Extraction.v new file mode 100644 index 0000000..dc93c21 --- /dev/null +++ b/proof/Extraction.v @@ -0,0 +1,17 @@ +(** * Extraction to OCaml — finiteness gate only + + Extracts [predicted_finite] to [lib/drl_verified/drl_verified.ml]. + To regenerate: cd proof && make *) + +From Stdlib Require Import Extraction. +From Stdlib Require Import ExtrOcamlBasic. +From Stdlib Require Import ExtrOcamlString. +From Stdlib Require Import ExtrOcamlNatInt. + +Require Import Schema. +Require Import Relation. +Require Import Drl. + +Set Extraction Output Directory "../lib/drl_verified". + +Extraction "drl_verified" predicted_finite. diff --git a/proof/Makefile b/proof/Makefile new file mode 100644 index 0000000..a9e1f72 --- /dev/null +++ b/proof/Makefile @@ -0,0 +1,14 @@ +COQMAKEFILE ?= Makefile.coq + +all: $(COQMAKEFILE) + mkdir -p ../lib/drl_verified + $(MAKE) -f $(COQMAKEFILE) + +$(COQMAKEFILE): _CoqProject + coq_makefile -f _CoqProject -o $(COQMAKEFILE) + +clean: $(COQMAKEFILE) + $(MAKE) -f $(COQMAKEFILE) clean + rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf + +.PHONY: all clean diff --git a/proof/Relation.v b/proof/Relation.v new file mode 100644 index 0000000..f7c087d --- /dev/null +++ b/proof/Relation.v @@ -0,0 +1,26 @@ +(** * Relation: minimal model for finiteness checking + + A relation is reduced to the two fields that [predicted_finite] + actually inspects: its name (for database lookup) and its + finiteness flag (for the gate decision). *) + +From Stdlib Require Import List. +From Stdlib Require Import String. +Require Import Schema. +Import ListNotations. + +Record relation := mkRelation { + rel_name : string; + rel_finite : bool; +}. + +(** A database is a named collection of relations. *) +Definition database := list (string * relation). + +(** Look up a relation by name. *) +Fixpoint db_lookup (name : string) (db : database) : option relation := + match db with + | [] => None + | (n, r) :: rest => + if String.eqb name n then Some r else db_lookup name rest + end. diff --git a/proof/Schema.v b/proof/Schema.v new file mode 100644 index 0000000..eb8f4c5 --- /dev/null +++ b/proof/Schema.v @@ -0,0 +1,5 @@ +(** * Schema: attribute name type *) + +From Stdlib Require Import String. + +Definition attr_name := string. diff --git a/proof/_CoqProject b/proof/_CoqProject new file mode 100644 index 0000000..0e6123e --- /dev/null +++ b/proof/_CoqProject @@ -0,0 +1,6 @@ +-R . Sakura + +Schema.v +Relation.v +Drl.v +Extraction.v diff --git a/proof/drl_verified.ml b/proof/drl_verified.ml new file mode 100644 index 0000000..f4c282a --- /dev/null +++ b/proof/drl_verified.ml @@ -0,0 +1,410 @@ + +(** val negb : bool -> bool **) + +let negb = function +| true -> false +| false -> true + +(** val fst : ('a1 * 'a2) -> 'a1 **) + +let fst = function +| (x, _) -> x + +(** val snd : ('a1 * 'a2) -> 'a2 **) + +let snd = function +| (_, y) -> y + +(** val app : 'a1 list -> 'a1 list -> 'a1 list **) + +let rec app l m = + match l with + | [] -> m + | a :: l1 -> a :: (app l1 m) + +(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) + +let rec map f = function +| [] -> [] +| a :: l0 -> (f a) :: (map f l0) + +(** val firstn : int -> 'a1 list -> 'a1 list **) + +let rec firstn n l = + (fun fO fS n -> if n=0 then fO () else fS (n-1)) + (fun _ -> []) + (fun n0 -> match l with + | [] -> [] + | a :: l0 -> a :: (firstn n0 l0)) + n + +(** val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list **) + +let rec flat_map f = function +| [] -> [] +| x :: l0 -> app (f x) (flat_map f l0) + +(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **) + +let rec existsb f = function +| [] -> false +| a :: l0 -> (||) (f a) (existsb f l0) + +(** val forallb : ('a1 -> bool) -> 'a1 list -> bool **) + +let rec forallb f = function +| [] -> true +| a :: l0 -> (&&) (f a) (forallb f l0) + +(** val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list **) + +let rec filter f = function +| [] -> [] +| x :: l0 -> if f x then x :: (filter f l0) else filter f l0 + +(** val find : ('a1 -> bool) -> 'a1 list -> 'a1 option **) + +let rec find f = function +| [] -> None +| x :: tl -> if f x then Some x else find f tl + +(** val eqb : char list -> char list -> bool **) + +let rec eqb s1 s2 = + match s1 with + | [] -> (match s2 with + | [] -> true + | _::_ -> false) + | c1::s1' -> + (match s2 with + | [] -> false + | c2::s2' -> if (=) c1 c2 then eqb s1' s2' else false) + +(** val append : char list -> char list -> char list **) + +let rec append s1 s2 = + match s1 with + | [] -> s2 + | c::s1' -> c::(append s1' s2) + +type attr_name = char list + +type domain_name = char list + +type schema = (attr_name * domain_name) list + +(** val has_attr : attr_name -> schema -> bool **) + +let has_attr a s = + existsb (fun p -> eqb a (fst p)) s + +(** val attr_names : schema -> attr_name list **) + +let attr_names s = + map fst s + +(** val filter_schema : attr_name list -> schema -> schema **) + +let filter_schema attrs s = + filter (fun p -> existsb (eqb (fst p)) attrs) s + +(** val merge_schema : schema -> schema -> schema **) + +let merge_schema s1 s2 = + app s1 (filter (fun p -> negb (has_attr (fst p) s1)) s2) + +(** val remove_attrs : attr_name list -> schema -> schema **) + +let remove_attrs attrs s = + filter (fun p -> negb (existsb (eqb (fst p)) attrs)) s + +(** val rename_in_schema : + (attr_name * attr_name) list -> schema -> schema **) + +let rename_in_schema renames s = + map (fun p -> + let a = fst p in + let d = snd p in + (match find (fun r -> eqb a (fst r)) renames with + | Some p0 -> let (_, a') = p0 in (a', d) + | None -> (a, d))) + s + +type value (* AXIOM TO BE REALIZED *) + +(** val value_eqb : value -> value -> bool **) + +let value_eqb = + failwith "AXIOM TO BE REALIZED (Sakura.Relation.value_eqb)" + +type tuple = (attr_name * value) list + +(** val tuple_lookup : attr_name -> tuple -> value option **) + +let rec tuple_lookup a = function +| [] -> None +| p :: rest -> + let (a', v) = p in if eqb a a' then Some v else tuple_lookup a rest + +(** val project_tuple : attr_name list -> tuple -> tuple **) + +let project_tuple attrs t = + filter (fun p -> existsb (eqb (fst p)) attrs) t + +(** val rename_tuple : (attr_name * attr_name) list -> tuple -> tuple **) + +let rename_tuple renames t = + map (fun p -> + let a = fst p in + let v = snd p in + (match find (fun r -> eqb a (fst r)) renames with + | Some p0 -> let (_, a') = p0 in (a', v) + | None -> (a, v))) + t + +(** val merge_tuples : tuple -> tuple -> tuple **) + +let merge_tuples t1 t2 = + app t1 (filter (fun p -> negb (existsb (eqb (fst p)) (map fst t1))) t2) + +(** val tuples_agree_on : attr_name list -> tuple -> tuple -> bool **) + +let tuples_agree_on attrs t1 t2 = + forallb (fun a -> + match tuple_lookup a t1 with + | Some v1 -> + (match tuple_lookup a t2 with + | Some v2 -> value_eqb v1 v2 + | None -> false) + | None -> (match tuple_lookup a t2 with + | Some _ -> false + | None -> true)) + attrs + +type relation = { rel_name : char list; rel_schema : schema; + rel_tuples : tuple list } + +type database = (char list * relation) list + +(** val db_lookup : char list -> database -> relation option **) + +let rec db_lookup name = function +| [] -> None +| p :: rest -> + let (n, r) = p in if eqb name n then Some r else db_lookup name rest + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +(** val predicted_schema : database -> query -> schema option **) + +let rec predicted_schema db = function +| Base name -> + (match db_lookup name db with + | Some r -> Some r.rel_schema + | None -> None) +| Const pairs -> + Some + (map (fun p -> ((fst p), + ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs) +| Select (_, source) -> predicted_schema db source +| Join (attrs, q1, q2) -> + (match predicted_schema db q1 with + | Some s1 -> + (match predicted_schema db q2 with + | Some s2 -> + Some + (merge_schema s1 + (remove_attrs (attr_names s1) (remove_attrs attrs s2))) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match predicted_schema db q1 with + | Some s1 -> + (match predicted_schema db q2 with + | Some s2 -> Some (merge_schema s1 s2) + | None -> None) + | None -> None) +| Project (attrs, q') -> + (match predicted_schema db q' with + | Some s -> Some (filter_schema attrs s) + | None -> None) +| Rename (renames, q') -> + (match predicted_schema db q' with + | Some s -> Some (rename_in_schema renames s) + | None -> None) +| Union (q1, _) -> predicted_schema db q1 +| Diff (q1, _) -> predicted_schema db q1 +| Take (_, q') -> predicted_schema db q' + +(** val literal_to_value : literal -> value **) + +let literal_to_value = + failwith "AXIOM TO BE REALIZED (Sakura.Drl.literal_to_value)" + +(** val eval_const : (attr_name * literal) list -> relation **) + +let eval_const pairs = + let tuple0 = map (fun p -> ((fst p), (literal_to_value (snd p)))) pairs in + let sch = + map (fun p -> ((fst p), + ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs + in + { rel_name = ('c'::('o'::('n'::('s'::('t'::[]))))); rel_schema = sch; + rel_tuples = (tuple0 :: []) } + +(** val semijoin : relation -> relation -> relation **) + +let semijoin filter_rel source = + let common = + filter (fun a -> has_attr a filter_rel.rel_schema) + (attr_names source.rel_schema) + in + let matches = fun t -> + existsb (fun ft -> tuples_agree_on common t ft) filter_rel.rel_tuples + in + { rel_name = source.rel_name; rel_schema = source.rel_schema; rel_tuples = + (filter matches source.rel_tuples) } + +(** val equijoin : attr_name list -> relation -> relation -> relation **) + +let equijoin attrs left right = + let joined = + flat_map (fun lt -> + flat_map (fun rt -> + if tuples_agree_on attrs lt rt then (merge_tuples lt rt) :: [] else []) + right.rel_tuples) + left.rel_tuples + in + let new_schema = + merge_schema left.rel_schema + (remove_attrs (attr_names left.rel_schema) + (remove_attrs attrs right.rel_schema)) + in + { rel_name = + (append ('j'::('o'::('i'::('n'::('_'::[]))))) + (append left.rel_name (append ('_'::[]) right.rel_name))); + rel_schema = new_schema; rel_tuples = joined } + +(** val cartesian : relation -> relation -> relation **) + +let cartesian left right = + let joined = + flat_map (fun lt -> map (fun rt -> merge_tuples lt rt) right.rel_tuples) + left.rel_tuples + in + { rel_name = + (append ('c'::('a'::('r'::('t'::('_'::[]))))) + (append left.rel_name (append ('_'::[]) right.rel_name))); + rel_schema = (merge_schema left.rel_schema right.rel_schema); rel_tuples = + joined } + +(** val project : attr_name list -> relation -> relation **) + +let project attrs r = + { rel_name = (append ('p'::('r'::('o'::('j'::('_'::[]))))) r.rel_name); + rel_schema = (filter_schema attrs r.rel_schema); rel_tuples = + (map (project_tuple attrs) r.rel_tuples) } + +(** val rename : (attr_name * attr_name) list -> relation -> relation **) + +let rename renames r = + { rel_name = + (append ('r'::('e'::('n'::('a'::('m'::('e'::('_'::[]))))))) r.rel_name); + rel_schema = (rename_in_schema renames r.rel_schema); rel_tuples = + (map (rename_tuple renames) r.rel_tuples) } + +(** val rel_union : relation -> relation -> relation **) + +let rel_union r1 r2 = + { rel_name = + (append ('u'::('n'::('i'::('o'::('n'::('_'::[])))))) + (append r1.rel_name (append ('_'::[]) r2.rel_name))); + rel_schema = r1.rel_schema; rel_tuples = + (app r1.rel_tuples r2.rel_tuples) } + +(** val rel_diff : relation -> relation -> relation **) + +let rel_diff r1 r2 = + let in_r2 = fun t -> + existsb (fun t2 -> tuples_agree_on (attr_names r1.rel_schema) t t2) + r2.rel_tuples + in + { rel_name = + (append ('d'::('i'::('f'::('f'::('_'::[]))))) + (append r1.rel_name (append ('_'::[]) r2.rel_name))); + rel_schema = r1.rel_schema; rel_tuples = + (filter (fun t -> negb (in_r2 t)) r1.rel_tuples) } + +(** val take : int -> relation -> relation **) + +let take n r = + { rel_name = (append ('t'::('a'::('k'::('e'::('_'::[]))))) r.rel_name); + rel_schema = r.rel_schema; rel_tuples = (firstn n r.rel_tuples) } + +(** val eval : database -> query -> relation option **) + +let rec eval db = function +| Base name -> db_lookup name db +| Const pairs -> Some (eval_const pairs) +| Select (filter_q, source_q) -> + (match eval db filter_q with + | Some filter_rel -> + (match eval db source_q with + | Some source_rel -> Some (semijoin filter_rel source_rel) + | None -> None) + | None -> None) +| Join (attrs, q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (equijoin attrs r1 r2) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (cartesian r1 r2) + | None -> None) + | None -> None) +| Project (attrs, q') -> + (match eval db q' with + | Some r -> Some (project attrs r) + | None -> None) +| Rename (renames, q') -> + (match eval db q' with + | Some r -> Some (rename renames r) + | None -> None) +| Union (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (rel_union r1 r2) + | None -> None) + | None -> None) +| Diff (q1, q2) -> + (match eval db q1 with + | Some r1 -> + (match eval db q2 with + | Some r2 -> Some (rel_diff r1 r2) + | None -> None) + | None -> None) +| Take (n, q') -> + (match eval db q' with + | Some r -> Some (take n r) + | None -> None) |