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 | 411 |
8 files changed, 0 insertions, 557 deletions
diff --git a/proof/.gitignore b/proof/.gitignore deleted file mode 100644 index 5ff7fe7..0000000 --- a/proof/.gitignore +++ /dev/null @@ -1,11 +0,0 @@ -# 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 deleted file mode 100644 index fd179a1..0000000 --- a/proof/Drl.v +++ /dev/null @@ -1,67 +0,0 @@ -(** * 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 deleted file mode 100644 index dc93c21..0000000 --- a/proof/Extraction.v +++ /dev/null @@ -1,17 +0,0 @@ -(** * 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 deleted file mode 100644 index a9e1f72..0000000 --- a/proof/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -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 deleted file mode 100644 index f7c087d..0000000 --- a/proof/Relation.v +++ /dev/null @@ -1,26 +0,0 @@ -(** * 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 deleted file mode 100644 index eb8f4c5..0000000 --- a/proof/Schema.v +++ /dev/null @@ -1,5 +0,0 @@ -(** * Schema: attribute name type *) - -From Stdlib Require Import String. - -Definition attr_name := string. diff --git a/proof/_CoqProject b/proof/_CoqProject deleted file mode 100644 index 0e6123e..0000000 --- a/proof/_CoqProject +++ /dev/null @@ -1,6 +0,0 @@ --R . Sakura - -Schema.v -Relation.v -Drl.v -Extraction.v diff --git a/proof/drl_verified.ml b/proof/drl_verified.ml deleted file mode 100644 index 137ad86..0000000 --- a/proof/drl_verified.ml +++ /dev/null @@ -1,411 +0,0 @@ -(** 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) |