From 6e4f49f7b8154d21c2c42f9978e6829d7a22a1de Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Sep 2020 07:52:57 +0200 Subject: starting to move common files --- lib/Impure/ImpConfig.v | 85 +++++++++++++++ lib/Impure/ImpCore.v | 196 +++++++++++++++++++++++++++++++++ lib/Impure/ImpExtern.v | 7 ++ lib/Impure/ImpHCons.v | 199 +++++++++++++++++++++++++++++++++ lib/Impure/ImpIO.v | 159 +++++++++++++++++++++++++++ lib/Impure/ImpLoops.v | 123 +++++++++++++++++++++ lib/Impure/ImpMonads.v | 148 +++++++++++++++++++++++++ lib/Impure/ImpPrelude.v | 206 +++++++++++++++++++++++++++++++++++ lib/Impure/LICENSE | 165 ++++++++++++++++++++++++++++ lib/Impure/README.md | 31 ++++++ lib/Impure/ocaml/ImpHConsOracles.ml | 66 +++++++++++ lib/Impure/ocaml/ImpHConsOracles.mli | 5 + lib/Impure/ocaml/ImpIOOracles.ml | 142 ++++++++++++++++++++++++ lib/Impure/ocaml/ImpIOOracles.mli | 33 ++++++ lib/Impure/ocaml/ImpLoopOracles.ml | 78 +++++++++++++ lib/Impure/ocaml/ImpLoopOracles.mli | 8 ++ 16 files changed, 1651 insertions(+) create mode 100644 lib/Impure/ImpConfig.v create mode 100644 lib/Impure/ImpCore.v create mode 100644 lib/Impure/ImpExtern.v create mode 100644 lib/Impure/ImpHCons.v create mode 100644 lib/Impure/ImpIO.v create mode 100644 lib/Impure/ImpLoops.v create mode 100644 lib/Impure/ImpMonads.v create mode 100644 lib/Impure/ImpPrelude.v create mode 100644 lib/Impure/LICENSE create mode 100644 lib/Impure/README.md create mode 100644 lib/Impure/ocaml/ImpHConsOracles.ml create mode 100644 lib/Impure/ocaml/ImpHConsOracles.mli create mode 100644 lib/Impure/ocaml/ImpIOOracles.ml create mode 100644 lib/Impure/ocaml/ImpIOOracles.mli create mode 100644 lib/Impure/ocaml/ImpLoopOracles.ml create mode 100644 lib/Impure/ocaml/ImpLoopOracles.mli (limited to 'lib/Impure') diff --git a/lib/Impure/ImpConfig.v b/lib/Impure/ImpConfig.v new file mode 100644 index 00000000..dd9785b5 --- /dev/null +++ b/lib/Impure/ImpConfig.v @@ -0,0 +1,85 @@ +(** 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/lib/Impure/ImpCore.v b/lib/Impure/ImpCore.v new file mode 100644 index 00000000..508b3f19 --- /dev/null +++ b/lib/Impure/ImpCore.v @@ -0,0 +1,196 @@ +(** 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/lib/Impure/ImpExtern.v b/lib/Impure/ImpExtern.v new file mode 100644 index 00000000..8fb3cf3b --- /dev/null +++ b/lib/Impure/ImpExtern.v @@ -0,0 +1,7 @@ +(** Exporting Extern functions +*) + +Require Export ImpPrelude. +Require Export ImpIO. +Require Export ImpLoops. +Require Export ImpHCons. diff --git a/lib/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v new file mode 100644 index 00000000..637116cc --- /dev/null +++ b/lib/Impure/ImpHCons.v @@ -0,0 +1,199 @@ +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/lib/Impure/ImpIO.v b/lib/Impure/ImpIO.v new file mode 100644 index 00000000..6c02c395 --- /dev/null +++ b/lib/Impure/ImpIO.v @@ -0,0 +1,159 @@ +(** 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/lib/Impure/ImpLoops.v b/lib/Impure/ImpLoops.v new file mode 100644 index 00000000..33376c19 --- /dev/null +++ b/lib/Impure/ImpLoops.v @@ -0,0 +1,123 @@ +(** 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/lib/Impure/ImpMonads.v b/lib/Impure/ImpMonads.v new file mode 100644 index 00000000..f01a2755 --- /dev/null +++ b/lib/Impure/ImpMonads.v @@ -0,0 +1,148 @@ +(** 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/lib/Impure/ImpPrelude.v b/lib/Impure/ImpPrelude.v new file mode 100644 index 00000000..de4c7973 --- /dev/null +++ b/lib/Impure/ImpPrelude.v @@ -0,0 +1,206 @@ +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/lib/Impure/LICENSE b/lib/Impure/LICENSE new file mode 100644 index 00000000..65c5ca88 --- /dev/null +++ b/lib/Impure/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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/lib/Impure/README.md b/lib/Impure/README.md new file mode 100644 index 00000000..2b19d14a --- /dev/null +++ b/lib/Impure/README.md @@ -0,0 +1,31 @@ +# `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/lib/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml new file mode 100644 index 00000000..2b66899b --- /dev/null +++ b/lib/Impure/ocaml/ImpHConsOracles.ml @@ -0,0 +1,66 @@ +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/lib/Impure/ocaml/ImpHConsOracles.mli b/lib/Impure/ocaml/ImpHConsOracles.mli new file mode 100644 index 00000000..5075d176 --- /dev/null +++ b/lib/Impure/ocaml/ImpHConsOracles.mli @@ -0,0 +1,5 @@ +open ImpPrelude +open HConsingDefs + +val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t +val xhCons: 'a hashP -> 'a hashConsing diff --git a/lib/Impure/ocaml/ImpIOOracles.ml b/lib/Impure/ocaml/ImpIOOracles.ml new file mode 100644 index 00000000..9e63c12d --- /dev/null +++ b/lib/Impure/ocaml/ImpIOOracles.ml @@ -0,0 +1,142 @@ +(* 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/lib/Impure/ocaml/ImpIOOracles.mli b/lib/Impure/ocaml/ImpIOOracles.mli new file mode 100644 index 00000000..6064286a --- /dev/null +++ b/lib/Impure/ocaml/ImpIOOracles.mli @@ -0,0 +1,33 @@ +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/lib/Impure/ocaml/ImpLoopOracles.ml b/lib/Impure/ocaml/ImpLoopOracles.ml new file mode 100644 index 00000000..cb7625e5 --- /dev/null +++ b/lib/Impure/ocaml/ImpLoopOracles.ml @@ -0,0 +1,78 @@ +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/lib/Impure/ocaml/ImpLoopOracles.mli b/lib/Impure/ocaml/ImpLoopOracles.mli new file mode 100644 index 00000000..194696a1 --- /dev/null +++ b/lib/Impure/ocaml/ImpLoopOracles.mli @@ -0,0 +1,8 @@ +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 ) -- cgit