diff options
Diffstat (limited to 'kvx/abstractbb')
| -rw-r--r-- | kvx/abstractbb/Impure/ImpConfig.v | 85 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpCore.v | 196 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpExtern.v | 7 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpHCons.v | 199 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpIO.v | 159 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpLoops.v | 123 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpMonads.v | 148 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ImpPrelude.v | 206 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/LICENSE | 165 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/README.md | 31 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml | 66 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli | 5 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml | 142 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli | 33 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml | 78 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli | 8 |
16 files changed, 0 insertions, 1651 deletions
diff --git a/kvx/abstractbb/Impure/ImpConfig.v b/kvx/abstractbb/Impure/ImpConfig.v deleted file mode 100644 index dd9785b5..00000000 --- a/kvx/abstractbb/Impure/ImpConfig.v +++ /dev/null @@ -1,85 +0,0 @@ -(** Impure Config for UNTRUSTED backend !!! *) - -Require Import ImpMonads. -Require Extraction. -(** Pure computations (used for extraction !) - -We keep module [Impure] opaque in order to check that Coq proof do not depend on -the implementation of [Impure]. - -*) - -Module Type ImpureView. - - Include MayReturnMonad. - -(* WARNING: THIS IS REALLY UNSAFE TO DECOMMENT THE "UnsafeImpure" module ! - - unsafe_coerce coerces an impure computation into a pure one ! - -*) - -(* START COMMENT *) - Module UnsafeImpure. - - Parameter unsafe_coerce: forall {A}, t A -> option A. - - Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x. - - Extraction Inline unsafe_coerce. - - End UnsafeImpure. -(* END COMMENT *) - - -End ImpureView. - - -Module Impure: ImpureView. - - Include IdentityMonad. - - Module UnsafeImpure. - - Definition unsafe_coerce {A} (x:t A) := Some x. - - Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x. - Proof. - unfold unsafe_coerce, mayRet; congruence. - Qed. - - End UnsafeImpure. - -End Impure. - - -(** Comment the above code and decomment this to test that coq proofs still work with an impure monad ! - -- this should fail only on extraction or if unsafe_coerce is used ! - -*) -(* -Module Impure: MayReturnMonad := PowerSetMonad. -*) - -Export Impure. - -Extraction Inline ret mk_annot. - - -(* WARNING. The following directive is unsound. - - Extraction Inline bind - -For example, it may lead to extract the following code as "true" (instead of an error raising code) - failwith "foo";;true - -*) - -Extract Inlined Constant bind => "(|>)". - - -Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *) -Extraction Inline t. - -Global Opaque t. diff --git a/kvx/abstractbb/Impure/ImpCore.v b/kvx/abstractbb/Impure/ImpCore.v deleted file mode 100644 index 508b3f19..00000000 --- a/kvx/abstractbb/Impure/ImpCore.v +++ /dev/null @@ -1,196 +0,0 @@ -(** Impure monad for interface with impure code - -*) - -Require Export Program. -Require Export ImpConfig. - -(* Theory: bind + embed => dbind - -Program Definition dbind {A B} (k1: t A) (k2: forall (a:A), (mayRet k1 a) -> t B) : t B - := bind (mk_annot k1) (fun a => k2 a _). - -Lemma mayRet_dbind: forall (A B:Type) k1 k2 (b:B), - mayRet (dbind k1 k2) b -> exists a:A, exists H: (mayRet k1 a), mayRet (k2 a H) b. -Proof. - intros A B k1 k2 b H; decompose [ex and] (mayRet_bind _ _ _ _ _ H). - eapply ex_intro. - eapply ex_intro. - eauto. -Qed. - -*) - -Definition wlp {A:Type} (k: t A) (P: A -> Prop): Prop - := forall a, mayRet k a -> P a. - -(* Notations *) - -(* Print Grammar constr. *) - -Module Notations. - - Bind Scope impure_scope with t. - Delimit Scope impure_scope with impure. - - Notation "?? A" := (t A) (at level 0, A at level 95): impure_scope. - - Notation "k '~~>' a" := (mayRet k a) (at level 75, no associativity): impure_scope. - - Notation "'RET' a" := (ret a) (at level 0): impure_scope. - - Notation "'DO' x '<~' k1 ';;' k2" := (bind k1 (fun x => k2)) - (at level 55, k1 at level 53, x at level 99, right associativity): impure_scope. - - Notation "k1 ';;' k2" := (bind k1 (fun _ => k2)) - (at level 55, right associativity): impure_scope. - - Notation "'WHEN' k '~>' a 'THEN' R" := (wlp k (fun a => R)) - (at level 73, R at level 100, right associativity): impure_scope. - - Notation "'ASSERT' P" := (ret (A:=P) _) (at level 0, only parsing): impure_scope. - -End Notations. - -Import Notations. -Local Open Scope impure. - -Goal ((?? list nat * ??nat -> nat) = ((?? ((list nat) * ?? nat) -> nat)))%type. -Proof. - apply refl_equal. -Qed. - - -(* wlp lemmas for tactics *) - -Lemma wlp_unfold A (k:??A)(P: A -> Prop): - (forall a, k ~~> a -> P a) - -> wlp k P. -Proof. - auto. -Qed. - -Lemma wlp_monotone A (k:?? A) (P1 P2: A -> Prop): - wlp k P1 - -> (forall a, k ~~> a -> P1 a -> P2 a) - -> wlp k P2. -Proof. - unfold wlp; eauto. -Qed. - -Lemma wlp_forall A B (k:?? A) (P: B -> A -> Prop): - (forall x, wlp k (P x)) - -> wlp k (fun a => forall x, P x a). -Proof. - unfold wlp; auto. -Qed. - -Lemma wlp_ret A (P: A -> Prop) a: - P a -> wlp (ret a) P. -Proof. - unfold wlp. - intros H b H0. - rewrite <- (mayRet_ret _ a b H0). - auto. -Qed. - -Lemma wlp_bind A B (k1:??A) (k2: A -> ??B) (P: B -> Prop): - wlp k1 (fun a => wlp (k2 a) P) -> wlp (bind k1 k2) P. -Proof. - unfold wlp. - intros H a H0. - case (mayRet_bind _ _ _ _ _ H0); clear H0. - intuition eauto. -Qed. - -Lemma wlp_ifbool A (cond: bool) (k1 k2: ?? A) (P: A -> Prop): - (cond=true -> wlp k1 P) -> (cond=false -> wlp k2 P) -> wlp (if cond then k1 else k2) P. -Proof. - destruct cond; auto. -Qed. - -Lemma wlp_letprod (A B C: Type) (p: A*B) (k: A -> B -> ??C) (P: C -> Prop): - (wlp (k (fst p) (snd p)) P) - -> (wlp (let (x,y):=p in (k x y)) P). -Proof. - destruct p; simpl; auto. -Qed. - -Lemma wlp_sum (A B C: Type) (x: A+B) (k1: A -> ??C) (k2: B -> ??C) (P: C -> Prop): - (forall a, x=inl a -> wlp (k1 a) P) -> - (forall b, x=inr b -> wlp (k2 b) P) -> - (wlp (match x with inl a => k1 a | inr b => k2 b end) P). -Proof. - destruct x; simpl; auto. -Qed. - -Lemma wlp_sumbool (A B:Prop) (C: Type) (x: {A}+{B}) (k1: A -> ??C) (k2: B -> ??C) (P: C -> Prop): - (forall a, x=left a -> wlp (k1 a) P) -> - (forall b, x=right b -> wlp (k2 b) P) -> - (wlp (match x with left a => k1 a | right b => k2 b end) P). -Proof. - destruct x; simpl; auto. -Qed. - -Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B) (P: B -> Prop): - (forall a, x=Some a -> wlp (k1 a) P) -> - (x=None -> wlp k2 P) -> - (wlp (match x with Some a => k1 a | None => k2 end) P). -Proof. - destruct x; simpl; auto. -Qed. - -(* Tactics - -MAIN tactics: - - xtsimplify "base": simplification using from hints in "base" database (in particular "wlp" lemmas). - - xtstep "base": only one step of simplification. - -For good performance, it is recommanded to have several databases. - -*) - -Ltac introcomp := - let a:= fresh "exta" in - let H:= fresh "Hexta" in - intros a H. - -(* decompose the current wlp goal using "introduction" rules *) -Ltac wlp_decompose := - apply wlp_ret - || apply wlp_bind - || apply wlp_ifbool - || apply wlp_letprod - || apply wlp_sum - || apply wlp_sumbool - || apply wlp_option - . - -(* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) -Ltac apply_wlp_hint hint := - eapply wlp_monotone; - [ hint; fail | idtac ] ; - simpl; introcomp. - -(* one step of wlp_xsimplify -*) -Ltac wlp_step hint := - match goal with - | |- (wlp _ _) => - wlp_decompose - || apply_wlp_hint hint - || (apply wlp_unfold; introcomp) - end. - -(* main general tactic -WARNING: for the good behavior of "wlp_xsimplify", "hint" must at least perform a "eauto". - -Example of use: - wlp_xsimplify (intuition eauto with base). -*) -Ltac wlp_xsimplify hint := - repeat (intros; subst; wlp_step hint; simpl; (tauto || hint)). - -Create HintDb wlp discriminated. - -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). diff --git a/kvx/abstractbb/Impure/ImpExtern.v b/kvx/abstractbb/Impure/ImpExtern.v deleted file mode 100644 index 8fb3cf3b..00000000 --- a/kvx/abstractbb/Impure/ImpExtern.v +++ /dev/null @@ -1,7 +0,0 @@ -(** Exporting Extern functions -*) - -Require Export ImpPrelude. -Require Export ImpIO. -Require Export ImpLoops. -Require Export ImpHCons. diff --git a/kvx/abstractbb/Impure/ImpHCons.v b/kvx/abstractbb/Impure/ImpHCons.v deleted file mode 100644 index 637116cc..00000000 --- a/kvx/abstractbb/Impure/ImpHCons.v +++ /dev/null @@ -1,199 +0,0 @@ -Require Export ImpIO. - -Import Notations. -Local Open Scope impure. - - -Axiom string_of_hashcode: hashcode -> ?? caml_string. -Extract Constant string_of_hashcode => "string_of_int". - -Axiom hash: forall {A}, A -> ?? hashcode. -Extract Constant hash => "Hashtbl.hash". - -(**************************) -(* (Weak) Sets *) - - -Import Dict. - -Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B. -Extract Constant make_dict => "ImpHConsOracles.make_dict". - - -Module Sets. - -Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}. - -Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod := - make_dict hp. - -Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit := - match l with - | nil => fun H => RET () - | x::l' => fun H => - d.(set)(x,x);; - add l' d - end. - -Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) := - DO d <~ empty hp (mod:=fun x => List.In x l);; - add l (mod:=fun x => List.In x l) d (H:=_);; - RET d. -Global Opaque create. - -Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool := - DO oy <~ (d.(get)) x;; - match oy with - | Some y => hp.(test_eq) x (`y) - | None => RET false - end. - -Local Hint Resolve test_eq_correct: wlp. - -Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod): - WHEN is_present hp x d ~> b THEN b=true -> mod x. -Proof. - wlp_simplify; subst; eauto. - - apply proj2_sig. - - discriminate. -Qed. -Hint Resolve is_present_correct: wlp. -Global Opaque is_present. - -Definition msg_assert_incl: pstring := "Sets.assert_incl". - -Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit := - match l with - | nil => RET () - | x::l' => - DO b <~ is_present hp x d;; - if b then - assert_incl hp l' d - else ( - hp.(log) x;; - FAILWITH msg_assert_incl - ) - end. - -Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod): - WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x. -Proof. - induction l; wlp_simplify; subst; eauto. -Qed. -Hint Resolve assert_incl_correct: wlp. -Global Opaque assert_incl. - -Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit := - (* println "";;print("dict_create ");;*) - DO d <~ create hp l2;; - (*print("assert_incl ");;*) - assert_incl hp l1 d. - -Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2: - WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2. -Proof. - wlp_simplify. -Qed. -Global Opaque assert_list_incl. -Hint Resolve assert_list_incl_correct: wlp. - -End Sets. - - - - -(********************************) -(* (Weak) HConsing *) - -Module HConsing. - -Export HConsingDefs. - -(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *) -Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A. -Extract Constant xhCons => "ImpHConsOracles.xhCons". - -Definition hCons_eq_msg: pstring := "xhCons: hash eq differs". - -Definition hCons {A} (hp: hashP A): ?? (hashConsing A) := - DO hco <~ xhCons hp ;; - RET {| - hC := (fun x => - DO x' <~ hC hco x ;; - DO b0 <~ hash_eq hp x.(hdata) x' ;; - assert_b b0 hCons_eq_msg;; - RET x'); - next_hid := hco.(next_hid); - next_log := hco.(next_log); - export := hco.(export); - remove := hco.(remove) - |}. - - -Lemma hCons_correct A (hp: hashP A): - WHEN hCons hp ~> hco THEN - (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) -> - forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'. -Proof. - wlp_simplify. -Qed. -Global Opaque hCons. -Hint Resolve hCons_correct: wlp. - - - -(* hashV: extending a given type with hash-consing *) -Record hashV {A:Type}:= { - data: A; - hid: hashcode -}. -Arguments hashV: clear implicits. - -Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {| - hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data); - get_hid := hid; - set_hid := fun v id => {| data := v.(data); hid := id |} -|}. - -Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}. - -Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) := - hCons (hashV_C hasheq). - -Lemma hConsV_correct A (hasheq: A -> A -> ?? bool): - WHEN hConsV hasheq ~> hco THEN - (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> - forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data). -Proof. - Local Hint Resolve f_equal2: core. - wlp_simplify. - exploit H; eauto. - + wlp_simplify. - + intros; congruence. -Qed. -Global Opaque hConsV. -Hint Resolve hConsV_correct: wlp. - -Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A := - DO clock <~ hco.(next_hid)();; - DO x' <~ hco.(hC) x;; - DO ok <~ hash_older x'.(hid) clock;; - if ok - then RET x' - else - hco.(remove) x;; - DO msg <~ unknownHash_msg x;; - FAILWITH msg. - -Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x: - WHEN hC_known hco msg x ~> x' THEN - (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) -> - x.(hdata).(data)=x'.(data). -Proof. - wlp_simplify. - unfold wlp in * |- ; eauto. -Qed. -Global Opaque hC_known. -Hint Resolve hC_known_correct: wlp. - -End HConsing. diff --git a/kvx/abstractbb/Impure/ImpIO.v b/kvx/abstractbb/Impure/ImpIO.v deleted file mode 100644 index 6c02c395..00000000 --- a/kvx/abstractbb/Impure/ImpIO.v +++ /dev/null @@ -1,159 +0,0 @@ -(** Extension of Coq language with some IO and exception-handling operators. - -TODO: integration with http://coq.io/ ? - -*) - -Require Export ImpPrelude. - -Import Notations. -Local Open Scope impure. - -(** Printing functions *) - -Axiom print: pstring -> ?? unit. -Extract Constant print => "ImpIOOracles.print". - -Axiom println: pstring -> ?? unit. -Extract Constant println => "ImpIOOracles.println". - -Axiom read_line: unit -> ?? pstring. -Extract Constant read_line => "ImpIOOracles.read_line". - -Require Import ZArith. -Axiom string_of_Z: Z -> ?? pstring. -Extract Constant string_of_Z => "ImpIOOracles.string_of_Z". - -(** timer *) - -Axiom timer: forall {A B}, (A -> ?? B)*A -> ?? B. -Extract Constant timer => "ImpIOOracles.timer". - -(** Exception Handling *) - -Axiom exit_observer: Type. -Extract Constant exit_observer => "((unit -> unit) ref)". - -Axiom new_exit_observer: (unit -> ??unit) -> ??exit_observer. -Extract Constant new_exit_observer => "ImpIOOracles.new_exit_observer". - -Axiom set_exit_observer: exit_observer * (unit -> ??unit) -> ??unit. -Extract Constant set_exit_observer => "ImpIOOracles.set_exit_observer". - -Axiom exn: Type. -Extract Inlined Constant exn => "exn". - -Axiom raise: forall {A}, exn -> ?? A. -Extract Constant raise => "raise". - -Axiom exn2string: exn -> ?? pstring. -Extract Constant exn2string => "ImpIOOracles.exn2string". - -Axiom fail: forall {A}, pstring -> ?? A. -Extract Constant fail => "ImpIOOracles.fail". - -Axiom try_with_fail: forall {A}, (unit -> ?? A) * (pstring -> exn -> ??A) -> ??A. -Extract Constant try_with_fail => "ImpIOOracles.try_with_fail". - -Axiom try_with_any: forall {A}, (unit -> ?? A) * (exn -> ??A) -> ??A. -Extract Constant try_with_any => "ImpIOOracles.try_with_any". - -Notation "'RAISE' e" := (DO r <~ raise (A:=False) e ;; RET (match r with end)) (at level 0): impure_scope. -Notation "'FAILWITH' msg" := (DO r <~ fail (A:=False) msg ;; RET (match r with end)) (at level 0): impure_scope. - -Definition _FAILWITH {A:Type} msg: ?? A := FAILWITH msg. - -Example _FAILWITH_correct A msg (P: A -> Prop): - WHEN _FAILWITH msg ~> r THEN P r. -Proof. - wlp_simplify. -Qed. - -Notation "'TRY' k1 'WITH_FAIL' s ',' e '=>' k2" := (try_with_fail (fun _ => k1, fun s e => k2)) - (at level 55, k1 at level 53, right associativity): impure_scope. - -Notation "'TRY' k1 'WITH_ANY' e '=>' k2" := (try_with_any (fun _ => k1, fun e => k2)) - (at level 55, k1 at level 53, right associativity): impure_scope. - - -Program Definition assert_b (b: bool) (msg: pstring): ?? b=true := - match b with - | true => RET _ - | false => FAILWITH msg - end. - -Lemma assert_wlp_true msg b: WHEN assert_b b msg ~> _ THEN b=true. -Proof. - wlp_simplify. -Qed. - -Lemma assert_false_wlp msg (P: Prop): WHEN assert_b false msg ~> _ THEN P. -Proof. - simpl; wlp_simplify. -Qed. - -Program Definition try_catch_fail_ensure {A} (k1: unit -> ?? A) (k2: pstring -> exn -> ??A) (P: A -> Prop | wlp (k1 tt) P /\ (forall s e, wlp (k2 s e) P)): ?? { r | P r } - := TRY - DO r <~ mk_annot (k1 tt);; - RET (exist P r _) - WITH_FAIL s, e => - DO r <~ mk_annot (k2 s e);; - RET (exist P r _). -Obligation 2. - unfold wlp in * |- *; eauto. -Qed. - -Notation "'TRY' k1 'CATCH_FAIL' s ',' e '=>' k2 'ENSURE' P" := (try_catch_fail_ensure (fun _ => k1) (fun s e => k2) (exist _ P _)) - (at level 55, k1 at level 53, right associativity): impure_scope. - -Definition is_try_post {A} (P: A -> Prop) k1 k2 : Prop := - wlp (k1 ()) P /\ forall (e:exn), wlp (k2 e) P. - -Program Definition try_catch_ensure {A} k1 k2 (P:A->Prop|is_try_post P k1 k2): ?? { r | P r } - := TRY - DO r <~ mk_annot (k1 ());; - RET (exist P r _) - WITH_ANY e => - DO r <~ mk_annot (k2 e);; - RET (exist P r _). -Obligation 1. - unfold is_try_post, wlp in * |- *; intuition eauto. -Qed. -Obligation 2. - unfold is_try_post, wlp in * |- *; intuition eauto. -Qed. - -Notation "'TRY' k1 'CATCH' e '=>' k2 'ENSURE' P" := (try_catch_ensure (fun _ => k1) (fun e => k2) (exist _ P _)) - (at level 55, k1 at level 53, right associativity): impure_scope. - - -Program Example tryex {A} (x y:A) := - TRY (RET x) - CATCH _ => (RET y) - ENSURE (fun r => r = x \/ r = y). -Obligation 1. - split; wlp_simplify. -Qed. - -Program Example tryex_test {A} (x y:A): - WHEN tryex x y ~> r THEN `r <> x -> `r = y. -Proof. - wlp_simplify. destruct exta as [r [X|X]]; intuition. -Qed. - - -Program Example try_branch1 {A} (x:A): ?? { r | r = x} := - TRY (RET x) - CATCH e => (FAILWITH "!") - ENSURE _. -Obligation 1. - split; wlp_simplify. -Qed. - -Program Example try_branch2 {A} (x:A): ?? { r | r = x} := - TRY (FAILWITH "!") - CATCH e => (RET x) - ENSURE _. -Obligation 1. - split; wlp_simplify. -Qed. diff --git a/kvx/abstractbb/Impure/ImpLoops.v b/kvx/abstractbb/Impure/ImpLoops.v deleted file mode 100644 index 33376c19..00000000 --- a/kvx/abstractbb/Impure/ImpLoops.v +++ /dev/null @@ -1,123 +0,0 @@ -(** Extension of Coq language with generic loops. *) - -Require Export ImpIO. - -Import Notations. -Local Open Scope impure. - - -(** While-loop iterations *) - -Axiom loop: forall {A B}, A * (A -> ?? (A+B)) -> ?? B. -Extract Constant loop => "ImpLoopOracles.loop". - - -Section While_Loop. - -(** Local Definition of "while-loop-invariant" *) -Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'. - -Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false} - := loop (A:={s | I s0 -> I s}) - (s0, - fun s => - match (cond s) with - | true => - DO s' <~ mk_annot (body s) ;; - RET (inl (A:={s | I s0 -> I s }) s') - | false => - RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s) - end). -Obligation 2. - unfold wli, wlp in * |-; eauto. -Qed. -Extraction Inline while. - -End While_Loop. - - -Section Loop_Until_None. -(** useful to demonstrate a UNSAT property *) - -(** Local Definition of "loop-until-None-invariant" *) -Let luni {S} (body: S -> ?? (option S)) (I: S -> Prop) := forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end. - -Program Definition loop_until_None {S} body (I: S -> Prop | luni body I) s0: ?? ~(I s0) - := loop (A:={s | I s0 -> I s}) - (s0, - fun s => - DO s' <~ mk_annot (body s) ;; - match s' with - | Some s1 => RET (inl (A:={s | I s0 -> I s }) s1) - | None => RET (inr (B:=~(I s0)) _) - end). -Obligation 2. - refine (H2 s _ _ H0). auto. -Qed. -Obligation 3. - intros X; refine (H1 s _ _ H). auto. -Qed. -Extraction Inline loop_until_None. - -End Loop_Until_None. - - -(*********************************************) -(* A generic fixpoint from an equality test *) - -Record answ {A B: Type} {R: A -> B -> Prop} := { - input: A ; - output: B ; - correct: R input output -}. -Arguments answ {A B}. - -Definition msg: pstring := "wapply fails". - -Definition beq_correct {A} (beq: A -> A -> ?? bool) := - forall x y, WHEN beq x y ~> b THEN b=true -> x=y. - -Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ?? answ R) (x:A): ?? B := - DO a <~ k x;; - DO b <~ beq x (input a) ;; - assert_b b msg;; - RET (output a). - -Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool) (k: A -> ?? answ R) x: - beq_correct beq - -> WHEN wapply beq k x ~> y THEN R x y. -Proof. - unfold beq_correct; wlp_simplify. - destruct exta; simpl; auto. -Qed. -Local Hint Resolve wapply_correct: wlp. -Global Opaque wapply. - -Axiom xrec_set_option: recMode -> ?? unit. -Extract Constant xrec_set_option => "ImpLoopOracles.xrec_set_option". - -(* TODO: generalizaton to get beq (and a Hash function ?) in parameters ? *) -Axiom xrec: forall {A B}, ((A -> ?? B) -> A -> ?? B) -> ?? (A -> ?? B). -Extract Constant xrec => "ImpLoopOracles.xrec". - -Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop) := - forall f x, WHEN recF f x ~> z THEN (forall x', WHEN f x' ~> y THEN R x' y) -> R x z. - - -Program Definition rec {A B} beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): ?? (A -> ?? B) := - DO f <~ xrec (B:=answ R) (fun f x => - DO y <~ mk_annot (recF (wapply beq f) x) ;; - RET {| input := x; output := `y |});; - RET (wapply beq f). -Obligation 1. - eapply H1; eauto. clear H H1. - wlp_simplify. -Qed. - -Lemma rec_correct A B beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): - WHEN rec beq recF R H1 H2 ~> f THEN forall x, WHEN f x ~> y THEN R x y. -Proof. - wlp_simplify. -Qed. -Hint Resolve rec_correct: wlp. -Global Opaque rec. diff --git a/kvx/abstractbb/Impure/ImpMonads.v b/kvx/abstractbb/Impure/ImpMonads.v deleted file mode 100644 index f01a2755..00000000 --- a/kvx/abstractbb/Impure/ImpMonads.v +++ /dev/null @@ -1,148 +0,0 @@ -(** Impure monad for interface with impure code -*) - - -Require Import Program. - - -Module Type MayReturnMonad. - - Axiom t: Type -> Type. - - Axiom mayRet: forall {A:Type}, t A -> A -> Prop. - - Axiom ret: forall {A}, A -> t A. - - Axiom bind: forall {A B}, (t A) -> (A -> t B) -> t B. - - Axiom mk_annot: forall {A} (k: t A), t { a: A | mayRet k a }. - - Axiom mayRet_ret: forall A (a b:A), - mayRet (ret a) b -> a=b. - - Axiom mayRet_bind: forall A B k1 k2 (b:B), - mayRet (bind k1 k2) b -> exists a:A, mayRet k1 a /\ mayRet (k2 a) b. - -End MayReturnMonad. - - - -(** Model of impure computation as predicate *) -Module PowerSetMonad<: MayReturnMonad. - - Definition t (A:Type) := A -> Prop. - - Definition mayRet {A:Type} (k: t A) a: Prop := k a. - - Definition ret {A:Type} (a:A) := eq a. - - Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := - fun b => exists a, k1 a /\ k2 a b. - - Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := fun _ => True. - - Lemma mayRet_ret A (a b:A): mayRet (ret a) b -> a=b. - Proof. - unfold mayRet, ret. firstorder. - Qed. - - Lemma mayRet_bind A B k1 k2 (b:B): - mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. - Proof. - unfold mayRet, bind. - firstorder. - Qed. - -End PowerSetMonad. - - -(** The identity interpretation *) -Module IdentityMonad<: MayReturnMonad. - - Definition t (A:Type) := A. - - (* may-return semantics of computations *) - Definition mayRet {A:Type} (a b:A): Prop := a=b. - - Definition ret {A:Type} (a:A) := a. - - Definition bind {A B:Type} (k1: A) (k2: A -> B) := k2 k1. - - Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } - := exist _ k (eq_refl k) . - - Lemma mayRet_ret (A:Type) (a b:A): mayRet (ret a) b -> a=b. - Proof. - intuition. - Qed. - - Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B): - mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. - Proof. - firstorder. - Qed. - -End IdentityMonad. - - -(** Model of impure computation as state-transformers *) -Module StateMonad<: MayReturnMonad. - - Parameter St: Type. (* A global state *) - - Definition t (A:Type) := St -> A * St. - - Definition mayRet {A:Type} (k: t A) a: Prop := - exists s, fst (k s)=a. - - Definition ret {A:Type} (a:A) := fun (s:St) => (a,s). - - Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := - fun s0 => let r := k1 s0 in k2 (fst r) (snd r). - - Program Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := - fun s0 => let r := k s0 in (exist _ (fst r) _, snd r). - Obligation 1. - unfold mayRet; eauto. - Qed. - - Lemma mayRet_ret {A:Type} (a b:A): mayRet (ret a) b -> a=b. - Proof. - unfold mayRet, ret. firstorder. - Qed. - - Lemma mayRet_bind {A B:Type} k1 k2 (b:B): - mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. - Proof. - unfold mayRet, bind. firstorder eauto. - Qed. - -End StateMonad. - -(** The deferred interpretation *) -Module DeferredMonad<: MayReturnMonad. - - Definition t (A:Type) := unit -> A. - - (* may-return semantics of computations *) - Definition mayRet {A:Type} (a: t A) (b:A): Prop := a tt=b. - - Definition ret {A:Type} (a:A) : t A := fun _ => a. - - Definition bind {A B:Type} (k1: t A) (k2: A -> t B) : t B := fun _ => k2 (k1 tt) tt. - - Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } - := fun _ => exist _ (k tt) (eq_refl (k tt)). - - Lemma mayRet_ret (A:Type) (a b: A): mayRet (ret a) b -> a=b. - Proof. - intuition. - Qed. - - Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B): - mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. - Proof. - firstorder. - Qed. - -End DeferredMonad. diff --git a/kvx/abstractbb/Impure/ImpPrelude.v b/kvx/abstractbb/Impure/ImpPrelude.v deleted file mode 100644 index de4c7973..00000000 --- a/kvx/abstractbb/Impure/ImpPrelude.v +++ /dev/null @@ -1,206 +0,0 @@ -Require Export String. -Require Export List. -Require Extraction. -Require Import Ascii. -Require Import BinNums. -Require Export ImpCore. -Require Export PArith. - - -Import Notations. -Local Open Scope impure. - -(** Impure lazy andb of booleans *) -Definition iandb (k1 k2: ??bool): ?? bool := - DO r1 <~ k1 ;; - if r1 then k2 else RET false. - -Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *) - -(** Strings for pretty-printing *) - -Axiom caml_string: Type. -Extract Constant caml_string => "string". - -(* New line *) -Definition nl: string := String (ascii_of_pos 10%positive) EmptyString. - -Inductive pstring: Type := - | Str: string -> pstring - | CamlStr: caml_string -> pstring - | Concat: pstring -> pstring -> pstring. - -Coercion Str: string >-> pstring. -Bind Scope string_scope with pstring. - -Notation "x +; y" := (Concat x y) - (at level 65, left associativity): string_scope. - -(** Coq references *) - -Record cref {A} := { - set: A -> ?? unit; - get: unit -> ?? A -}. -Arguments cref: clear implicits. - -Axiom make_cref: forall {A}, A -> ?? cref A. -Extract Constant make_cref => "(fun x -> let r = ref x in { set = (fun y -> r:=y); get = (fun () -> !r) })". - - -(** Data-structure for a logger *) - -Record logger {A:Type} := { - log_insert: A -> ?? unit; - log_info: unit -> ?? pstring; -}. -Arguments logger: clear implicits. - -Axiom count_logger: unit -> ?? logger unit. -Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (fun () -> count := !count + 1); log_info = (fun () -> (CamlStr (string_of_int !count))) })". - - -(** Axioms of Physical equality *) - -Axiom phys_eq: forall {A}, A -> A -> ?? bool. - -Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y. - - -(* We only check here that above axioms are not trivially inconsistent... - (but this does not prove the correctness of the extraction directive below). - *) -Module PhysEqModel. - -Definition phys_eq {A} (x y: A) := ret false. - -Lemma phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y. -Proof. - wlp_simplify. discriminate. -Qed. - -End PhysEqModel. - -Extract Inlined Constant phys_eq => "(==)". -Hint Resolve phys_eq_correct: wlp. - - -Axiom struct_eq: forall {A}, A -> A -> ?? bool. -Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y. -Extract Inlined Constant struct_eq => "(=)". -Hint Resolve struct_eq_correct: wlp. - - -(** Data-structure for generic hash-consing *) - -Axiom hashcode: Type. -Extract Constant hashcode => "int". - -(* NB: hashConsing is assumed to generate hash-code in ascending order. - This gives a way to check that a hash-consed value is older than an other one. -*) -Axiom hash_older: hashcode -> hashcode -> ?? bool. -Extract Inlined Constant hash_older => "(<)". - -Module Dict. - -Record hash_params {A:Type} := { - test_eq: A -> A -> ??bool; - test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y; - hashing: A -> ??hashcode; - log: A -> ??unit (* for debugging only *) -}. -Arguments hash_params: clear implicits. - - -Record t {A B:Type} := { - set: A * B -> ?? unit; - get: A -> ?? option B -}. -Arguments t: clear implicits. - -End Dict. - -Module HConsingDefs. - -Record hashinfo {A: Type} := { - hdata: A; - hcodes: list hashcode; -}. -Arguments hashinfo: clear implicits. - -(* for inductive types with intrinsic hash-consing *) -Record hashP {A:Type}:= { - hash_eq: A -> A -> ?? bool; - get_hid: A -> hashcode; - set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *) -}. -Arguments hashP: clear implicits. - -Axiom unknown_hid: hashcode. -Extract Constant unknown_hid => "-1". - -Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid. - -Record hashExport {A:Type}:= { - get_info: hashcode -> ?? hashinfo A; - iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *) -}. -Arguments hashExport: clear implicits. - -Record hashConsing {A:Type}:= { - hC: hashinfo A -> ?? A; - (**** below: debugging or internal functions ****) - next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *) - remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *) - next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *) - export: unit -> ?? hashExport A ; -}. -Arguments hashConsing: clear implicits. - -End HConsingDefs. - -(** recMode: this is mainly for Tests ! *) -Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec. - - -(* This a copy-paste from definitions in CompCert/Lib/CoqLib.v *) -Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. -Proof. auto. Qed. - -Ltac exploit x := - refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _ _) _) - || refine (modusponens _ _ (x _ _ _) _) - || refine (modusponens _ _ (x _ _) _) - || refine (modusponens _ _ (x _) _). diff --git a/kvx/abstractbb/Impure/LICENSE b/kvx/abstractbb/Impure/LICENSE deleted file mode 100644 index 65c5ca88..00000000 --- a/kvx/abstractbb/Impure/LICENSE +++ /dev/null @@ -1,165 +0,0 @@ - GNU LESSER GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - - This version of the GNU Lesser General Public License incorporates -the terms and conditions of version 3 of the GNU General Public -License, supplemented by the additional permissions listed below. - - 0. Additional Definitions. - - As used herein, "this License" refers to version 3 of the GNU Lesser -General Public License, and the "GNU GPL" refers to version 3 of the GNU -General Public License. - - "The Library" refers to a covered work governed by this License, -other than an Application or a Combined Work as defined below. - - An "Application" is any work that makes use of an interface provided -by the Library, but which is not otherwise based on the Library. -Defining a subclass of a class defined by the Library is deemed a mode -of using an interface provided by the Library. - - A "Combined Work" is a work produced by combining or linking an -Application with the Library. The particular version of the Library -with which the Combined Work was made is also called the "Linked -Version". - - The "Minimal Corresponding Source" for a Combined Work means the -Corresponding Source for the Combined Work, excluding any source code -for portions of the Combined Work that, considered in isolation, are -based on the Application, and not on the Linked Version. - - The "Corresponding Application Code" for a Combined Work means the -object code and/or source code for the Application, including any data -and utility programs needed for reproducing the Combined Work from the -Application, but excluding the System Libraries of the Combined Work. - - 1. Exception to Section 3 of the GNU GPL. - - You may convey a covered work under sections 3 and 4 of this License -without being bound by section 3 of the GNU GPL. - - 2. Conveying Modified Versions. - - If you modify a copy of the Library, and, in your modifications, a -facility refers to a function or data to be supplied by an Application -that uses the facility (other than as an argument passed when the -facility is invoked), then you may convey a copy of the modified -version: - - a) under this License, provided that you make a good faith effort to - ensure that, in the event an Application does not supply the - function or data, the facility still operates, and performs - whatever part of its purpose remains meaningful, or - - b) under the GNU GPL, with none of the additional permissions of - this License applicable to that copy. - - 3. Object Code Incorporating Material from Library Header Files. - - The object code form of an Application may incorporate material from -a header file that is part of the Library. You may convey such object -code under terms of your choice, provided that, if the incorporated -material is not limited to numerical parameters, data structure -layouts and accessors, or small macros, inline functions and templates -(ten or fewer lines in length), you do both of the following: - - a) Give prominent notice with each copy of the object code that the - Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the object code with a copy of the GNU GPL and this license - document. - - 4. Combined Works. - - You may convey a Combined Work under terms of your choice that, -taken together, effectively do not restrict modification of the -portions of the Library contained in the Combined Work and reverse -engineering for debugging such modifications, if you also do each of -the following: - - a) Give prominent notice with each copy of the Combined Work that - the Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the Combined Work with a copy of the GNU GPL and this license - document. - - c) For a Combined Work that displays copyright notices during - execution, include the copyright notice for the Library among - these notices, as well as a reference directing the user to the - copies of the GNU GPL and this license document. - - d) Do one of the following: - - 0) Convey the Minimal Corresponding Source under the terms of this - License, and the Corresponding Application Code in a form - suitable for, and under terms that permit, the user to - recombine or relink the Application with a modified version of - the Linked Version to produce a modified Combined Work, in the - manner specified by section 6 of the GNU GPL for conveying - Corresponding Source. - - 1) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (a) uses at run time - a copy of the Library already present on the user's computer - system, and (b) will operate properly with a modified version - of the Library that is interface-compatible with the Linked - Version. - - e) Provide Installation Information, but only if you would otherwise - be required to provide such information under section 6 of the - GNU GPL, and only to the extent that such information is - necessary to install and execute a modified version of the - Combined Work produced by recombining or relinking the - Application with a modified version of the Linked Version. (If - you use option 4d0, the Installation Information must accompany - the Minimal Corresponding Source and Corresponding Application - Code. If you use option 4d1, you must provide the Installation - Information in the manner specified by section 6 of the GNU GPL - for conveying Corresponding Source.) - - 5. Combined Libraries. - - You may place library facilities that are a work based on the -Library side by side in a single library together with other library -facilities that are not Applications and are not covered by this -License, and convey such a combined library under terms of your -choice, if you do both of the following: - - a) Accompany the combined library with a copy of the same work based - on the Library, uncombined with any other library facilities, - conveyed under the terms of this License. - - b) Give prominent notice with the combined library that part of it - is a work based on the Library, and explaining where to find the - accompanying uncombined form of the same work. - - 6. Revised Versions of the GNU Lesser General Public License. - - The Free Software Foundation may publish revised and/or new versions -of the GNU Lesser General Public License from time to time. Such new -versions will be similar in spirit to the present version, but may -differ in detail to address new problems or concerns. - - Each version is given a distinguishing version number. If the -Library as you received it specifies that a certain numbered version -of the GNU Lesser General Public License "or any later version" -applies to it, you have the option of following the terms and -conditions either of that published version or of any later version -published by the Free Software Foundation. If the Library as you -received it does not specify a version number of the GNU Lesser -General Public License, you may choose any version of the GNU Lesser -General Public License ever published by the Free Software Foundation. - - If the Library as you received it specifies that a proxy can decide -whether future versions of the GNU Lesser General Public License shall -apply, that proxy's public statement of acceptance of any version is -permanent authorization for you to choose that version for the -Library. diff --git a/kvx/abstractbb/Impure/README.md b/kvx/abstractbb/Impure/README.md deleted file mode 100644 index 2b19d14a..00000000 --- a/kvx/abstractbb/Impure/README.md +++ /dev/null @@ -1,31 +0,0 @@ -# `Impure`: importing OCaml functions as non-deterministic ones. - -The principle of this library is to encode the type `A -> B` of an -OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type -of an axiomatized monad that can be interpreted as `B -> Prop`. In -other word, this encoding abstracts an OCaml function as a function -returning a postcondition on its possible results (ie a relation between its -parameter and its result). Side-effects are simply ignored. And -reasoning on such a function is only possible in partial correctness. - -See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo). - -## Credits - -[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr). - -## Code Overview - -- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms. - -- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction. - -- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style). - -- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles. - -- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles. - [ImpExtern](ImpExtern.v) exports all these impure operators. - -- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles. - diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml deleted file mode 100644 index 2b66899b..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml +++ /dev/null @@ -1,66 +0,0 @@ -open ImpPrelude -open HConsingDefs - -let make_dict (type key) (p: key Dict.hash_params) = - let module MyHashedType = struct - type t = key - let equal = p.Dict.test_eq - let hash = p.Dict.hashing - end in - let module MyHashtbl = Hashtbl.Make(MyHashedType) in - let dict = MyHashtbl.create 1000 in - { - Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d); - Dict.get = (fun k -> MyHashtbl.find_opt dict k) - } - - -exception Stop;; - -let xhCons (type a) (hp:a hashP) = - (* We use a hash-table, but a hash-set would be sufficient ! *) - (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *) - (* Ideally, a parameter would allow to select between the weak or full version *) - let module MyHashedType = struct - type t = a hashinfo - let equal x y = hp.hash_eq x.hdata y.hdata - let hash x = Hashtbl.hash x.hcodes - end in - let module MyHashtbl = Hashtbl.Make(MyHashedType) in - let pick t = - let res = ref None in - try - MyHashtbl.iter (fun k d -> res:=Some (k,d); raise Stop) t; - None - with - | Stop -> !res - in - let t = MyHashtbl.create 1000 in - let logs = ref [] in - { - hC = (fun (k:a hashinfo) -> - match MyHashtbl.find_opt t k with - | Some d -> d - | None -> (*print_string "+";*) - let d = hp.set_hid k.hdata (MyHashtbl.length t) in - MyHashtbl.add t {k with hdata = d } d; d); - next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs)); - next_hid = (fun () -> MyHashtbl.length t); - remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x); - export = fun () -> - match pick t with - | None -> { get_info = (fun _ -> raise Not_found); iterall = (fun _ -> ()) } - | Some (k,_) -> - (* the state is fully copied at export ! *) - let logs = ref (List.rev_append (!logs) []) in - let rec step_log i = - match !logs with - | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i) - | _ -> [] - in let a = Array.make (MyHashtbl.length t) k in - MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t; - { - get_info = (fun i -> a.(i)); - iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a) - } - } diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli deleted file mode 100644 index 5075d176..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli +++ /dev/null @@ -1,5 +0,0 @@ -open ImpPrelude -open HConsingDefs - -val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t -val xhCons: 'a hashP -> 'a hashConsing diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml deleted file mode 100644 index 9e63c12d..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml +++ /dev/null @@ -1,142 +0,0 @@ -(* Warning - -These oracles assumes the following extraction directives: - "Require Import ExtrOcamlString." - -*) - -open ImpPrelude -(* -open BinNums -open Datatypes -*) - -(* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *) -exception Overflow - -let aux_add: ('a, 'b) Hashtbl.t -> 'b Queue.t -> 'a -> 'b -> unit - = fun t q i p -> - if i < 1 then (* protection against wrap around *) - raise Overflow; - Queue.add p q; - Hashtbl.add t i p - -let memo_int2pos: int -> int -> BinNums.positive - = fun n -> - (* init of the Hashtbl *) - let n = max n 1 in - let t = Hashtbl.create n in - let q = Queue.create () in - aux_add t q 1 BinNums.Coq_xH ; - for i = 1 to (n-1)/2 do - let last = Queue.take q in - let ni = 2*i in - aux_add t q ni (BinNums.Coq_xO last); - aux_add t q (ni+1) (BinNums.Coq_xI last) - done; - if n mod 2 = 0 then ( - let last = Queue.take q in - Hashtbl.add t n (BinNums.Coq_xO last) - ); - (* memoized translation of i *) - let rec find i = - try - (* Printf.printf "-> %d\n" i; *) - Hashtbl.find t i - with Not_found -> - (* Printf.printf "<- %d\n" i; *) - if i <= 0 then - invalid_arg "non-positive integer" - else - let p = find (i/2) in - let pi = if i mod 2 = 0 then BinNums.Coq_xO p else BinNums.Coq_xI p in - Hashtbl.add t i pi; - pi - in find;; - -let new_exit_observer: (unit -> unit) -> (unit -> unit) ref - = fun f -> - let o = ref f in - at_exit (fun () -> !o()); - o;; - -let set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit - = fun (r, f) -> r := f - -let rec print: pstring -> unit - = fun ps -> - match ps with - | Str l -> List.iter print_char l - | CamlStr s -> print_string s - | Concat(ps1,ps2) -> (print ps1; print ps2);; - -let println: pstring -> unit - = fun l -> print l; print_newline() - -let read_line () = - CamlStr (Stdlib.read_line());; - -exception ImpureFail of pstring;; - -let exn2string: exn -> pstring - = fun e -> CamlStr (Printexc.to_string e) - -let fail: pstring -> 'a - = fun s -> raise (ImpureFail s);; - -let try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a - = fun (k1, k2) -> - try - k1() - with - | (ImpureFail s) as e -> k2 s e - -let try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a - = fun (k1, k2) -> - try - k1() - with - | e -> k2 e - -(** MISC **) - -let rec posTr: BinNums.positive -> int -= function - | BinNums.Coq_xH -> 1 - | BinNums.Coq_xO p -> (posTr p)*2 - | BinNums.Coq_xI p -> (posTr p)*2+1;; - -let zTr: BinNums.coq_Z -> int -= function - | BinNums.Z0 -> 0 - | BinNums.Zpos p -> posTr p - | BinNums.Zneg p -> - (posTr p) - -let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH))) - -let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring -= let (q,r) = BinInt.Z.pos_div_eucl p ten in - let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in - match q with - | BinNums.Z0 -> acc0 - | BinNums.Zpos p0 -> string_of_pos p0 acc0 - | _ -> assert false - -(* -let string_of_Z_debug: BinNums.coq_Z -> pstring -= fun p -> CamlStr (string_of_int (zTr p)) -*) - -let string_of_Z: BinNums.coq_Z -> pstring -= function - | BinNums.Z0 -> CamlStr "0" - | BinNums.Zpos p -> string_of_pos p (CamlStr "") - | BinNums.Zneg p -> Concat (CamlStr "-", string_of_pos p (CamlStr "")) - -let timer ((f:'a -> 'b), (x:'a)) : 'b = - Gc.compact(); - let itime = (Unix.times()).Unix.tms_utime in - let r = f x in - let rt = (Unix.times()).Unix.tms_utime -. itime in - Printf.printf "time = %f\n" rt; - r diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli deleted file mode 100644 index 6064286a..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli +++ /dev/null @@ -1,33 +0,0 @@ -open ImpPrelude - - -(* -Memoized version of translation from int -> BinNums.positive. -The first arg is an indicative bound on the max int translated: -it pre-computes all positives lower or equal to this bound. -*) -val memo_int2pos: int -> int -> BinNums.positive - -val read_line: unit -> pstring - -val print: pstring -> unit - -val println: pstring -> unit - -val string_of_Z: BinNums.coq_Z -> pstring - -val timer : (('a -> 'b ) * 'a) -> 'b - -val new_exit_observer: (unit -> unit) -> (unit -> unit) ref - -val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit - -val exn2string: exn -> pstring - -val fail: pstring -> 'a - -exception ImpureFail of pstring;; - -val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a - -val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml deleted file mode 100644 index cb7625e5..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml +++ /dev/null @@ -1,78 +0,0 @@ -open ImpPrelude -open Datatypes - -(** GENERIC ITERATIVE LOOP **) - -(* a simple version of loop *) -let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - = fun (a0, f) -> - let rec iter: 'a -> 'b - = fun a -> - match f a with - | Coq_inl a' -> iter a' - | Coq_inr b -> b - in - iter a0;; - -(* loop from while *) -let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - = fun (a0, f) -> - let s = ref (f a0) in - while (match !s with Coq_inl _ -> true | _ -> false) do - match !s with - | Coq_inl a -> s:=f a - | _ -> assert false - done; - match !s with - | Coq_inr b -> b - | _ -> assert false;; - -let loop = simple_loop - - -(** GENERIC FIXPOINTS **) - -let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let rec f x = recf f x in - f - -let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let memo = Hashtbl.create 10 in - let rec f x = - try - Hashtbl.find memo x - with - Not_found -> - let r = recf f x in - Hashtbl.replace memo x r; - r - in f - -let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let fix = ref (fun x -> failwith "init") in - fix := (fun x -> recf !fix x); - !fix;; - -let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let memo = ref None in - let rec f x = - match !memo with - | Some y -> y - | None -> - let r = recf f x in - memo := Some r; - r - in f - -let xrec_mode = ref MemoRec - -let xrec_set_option : recMode -> unit -= fun m -> xrec_mode := m - -let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) - = fun recf -> - match !xrec_mode with - | StdRec -> std_rec recf - | MemoRec -> memo_rec recf - | BareRec -> bare_rec recf - | BuggyRec -> buggy_rec recf diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli deleted file mode 100644 index 194696a1..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli +++ /dev/null @@ -1,8 +0,0 @@ -open ImpPrelude -open Datatypes - -val loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - -val xrec_set_option: recMode -> unit - -val xrec: (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) |