diff --git a/src/AM_Helpers.v b/src/AM_Helpers.v index f2cf0e7..7c4ba43 100644 --- a/src/AM_Helpers.v +++ b/src/AM_Helpers.v @@ -1,16 +1,9 @@ (* Helper definitions for AM Client and Server implementations. *) -Require Import Term Cvm_Run Attestation_Session ID_Type EqClass. +Require Import Term ID_Type. -Require Import Impl_appraisal Appraisal_IO_Stubs IO_Stubs AM_Monad ErrorStMonad_Coq. +Require Import Interface. -Require Import Interface Maps Auto StructTactics. - -Require Import Disclose ErrorStringConstants. - -Require Import Coq.Program.Tactics. - -Require Import List. Import ListNotations. diff --git a/src/AM_Json_Interfaces.v b/src/AM_Json_Interfaces.v index 0643a6d..a240c1e 100644 --- a/src/AM_Json_Interfaces.v +++ b/src/AM_Json_Interfaces.v @@ -1,7 +1,8 @@ Require Import List. Import ListNotations. -Require Import BS Term_Defs Attestation_Session Interface String IO_Stubs Manifest_Admits ErrorStMonad_Coq AM_Monad Session_Config_Compiler Manifest. -Require Import ErrorStringConstants AM_Helpers Impl_appraisal Cvm_Run AM_Manager. +Require Import BS Term_Defs Attestation_Session Interface String IO_Stubs Manifest_Admits ErrorStMonad_Coq AM_Monad Session_Config_Compiler. +Require Import ErrorStringConstants Impl_appraisal Cvm_Run AM_Manager. +Import ErrNotation. Definition am_check_auth_tok (t:Term) (fromPl:Plc) (authTok:ReqAuthTok) : AM AppResultC := @@ -12,7 +13,7 @@ Definition am_check_auth_tok (t:Term) (fromPl:Plc) (authTok:ReqAuthTok) | false => am_failm (am_error errStr_requester_bound) | true => gen_appraise_AM auth_et auth_ev end) ;; - ret appres + err_ret appres end. (* Definition am_serve_auth_tok_req (t:Term) (fromPl : Plc) diff --git a/src/AM_Monad.v b/src/AM_Monad.v index 191c84f..6370c7e 100644 --- a/src/AM_Monad.v +++ b/src/AM_Monad.v @@ -1,7 +1,7 @@ (* Monadic helpers and custom automation for the AM Monad (AM) *) Require Import List String. -Require Import ErrorStMonad_Coq BS Maps Term_Defs_Core Term_Defs Cvm_Run Cvm_St. +Require Import ErrorStMonad_Coq Maps Term_Defs Cvm_Run Cvm_St Cvm_Monad. Require Import ErrorStringConstants Appraisal_IO_Stubs Attestation_Session. @@ -16,76 +16,36 @@ Definition am_error_to_string (err:AM_Error) : string := | cvm_error e => errStr_cvm_error end. -Definition fromSome{A E:Type} (default:A) (opt:ResultT A E): A := - match opt with - | resultC x => x - | _ => default - end. - -(* Definition run_am_app_comp_with_default{A:Type} (am_comp:AM A) (default_A:A) (b:bool): A := - if (b) - then ( - let optRes := evalErr am_comp empty_amst in - let v := - match optRes with - | resultC _ => (negb b) - | errC e => print_am_error e b - end in - if(v) - then - (default_A) - else - (fromSome default_A optRes) - ) - else - (default_A). *) - -Definition run_am_app_comp_init_with_default{A:Type} (am_comp:AM A) (st:AM_St) (default_A:A) (b:bool): A := - if (b) - then ( - let optRes := evalErr am_comp st in - let v := - match optRes with - | resultC _ => (negb b) - | errC e => print_am_error e b - end in - if(v) - then - (default_A) - else - (fromSome default_A optRes) - ) - else - (default_A). - Definition run_am_app_comp_init {A:Type} (am_comp:AM A) (st:AM_St) : ResultT A string := match (fst (am_comp st)) with | resultC x => resultC x | errC e => errC (am_error_to_string e) end. +Import ErrNotation. + Definition get_AM_config : AM Session_Config := (* TODO: consider moving this functionality to a Reader-like monad i.e. an 'ask' primitive *) - st <- get ;; - ret (am_config st). + st <- err_get ;; + err_ret (am_config st). Definition am_newNonce (bs:BS) : AM nat := - oldSt <- get ;; + oldSt <- err_get ;; let oldMap := am_nonceMap oldSt in let oldId := am_nonceId oldSt in let oldAMConfig := am_config oldSt in let newMap := map_set oldMap oldId bs in let newId := oldId + 1 in - put (mkAM_St newMap newId oldAMConfig) ;; - ret oldId. + err_put (mkAM_St newMap newId oldAMConfig) ;; + err_ret oldId. Definition am_getNonce (nid:nat) : AM BS := - oldSt <- get ;; + oldSt <- err_get ;; let oldMap := am_nonceMap oldSt in let resopt := map_get oldMap nid in match resopt with - | Some res => ret res + | Some res => err_ret res | None => am_failm (am_error errStr_amNonce) end. @@ -93,23 +53,17 @@ Definition am_getNonce (nid:nat) : AM BS := Definition am_runCvm_nonce (t:Term) (bs:BS) (ac : Session_Config) : AM (nat * RawEv) := nid <- am_newNonce bs ;; match run_cvm_w_config t [bs] ac with - | resultC res_st => ret (nid, (get_bits (st_ev res_st))) + | resultC res_st => err_ret (nid, (get_bits (st_ev res_st))) | errC e => am_failm (cvm_error e) end. - Ltac am_monad_unfold := - repeat unfold - get_AM_config, - am_newNonce, - am_getNonce, - - - am_failm, - get, - when, - put, - nop, - modify, - bind, - ret in * ; - simpl in * . \ No newline at end of file +Ltac am_monad_unfold := + repeat + (repeat unfold + get_AM_config, + am_newNonce, + am_getNonce, + am_failm, + am_runCvm_nonce in *; + repeat cvm_monad_unfold; + simpl in *). \ No newline at end of file diff --git a/src/AM_St.v b/src/AM_St.v index dc98ab2..07e7f61 100644 --- a/src/AM_St.v +++ b/src/AM_St.v @@ -1,6 +1,6 @@ (* Definitions for AM Monad State (AM_St) and AM Monad (AM). *) -Require Import Maps ResultT BS Term_Defs_Core Cvm_St ErrorStMonad_Coq String Attestation_Session. +Require Import Maps Term_Defs_Core Cvm_St ErrorStMonad_Coq String Attestation_Session. Require Import List. diff --git a/src/Anno_Term_Defs.v b/src/Anno_Term_Defs.v index f9a9b06..7e64e9d 100644 --- a/src/Anno_Term_Defs.v +++ b/src/Anno_Term_Defs.v @@ -4,12 +4,11 @@ *) -Require Import Term_Defs OptMonad_Coq BS Preamble. +Require Import Term_Defs Preamble. Require Import StructTactics Defs. -Require Import Lia Coq.Program.Tactics. -Require Import List. +Require Import Lia. Import List.ListNotations. @@ -85,7 +84,7 @@ Proof. generalizeEverythingElse t''. induction t''; intros H H0; ff. -Defined. +Qed. (** This function annotates a term. It feeds a natural number throughout the computation so as to ensure each event has a unique @@ -156,7 +155,7 @@ Proof. erewrite <- IHt2. jkjke. jkjke. -Defined. +Qed. (* Propositional versions of anno function equalities *) Inductive annoP: AnnoTerm -> Term -> Prop := @@ -197,7 +196,7 @@ Proof. repeat expand_let_pairs; simpl; try (repeat jkjk; auto;congruence); try (repeat jkjk'; auto). -Defined. +Qed. (** This predicate determines if an annotated term is well formed, @@ -245,7 +244,7 @@ Proof. induction t; intros; try destruct a; ff. -Defined. +Qed. Lemma anno_mono : forall (t:Term) (i j:nat) (t':AnnoTerm), anno t i = (j,t') -> @@ -255,7 +254,7 @@ Proof. ff; repeat find_apply_hyp_hyp; lia. -Defined. +Qed. #[export] Hint Resolve anno_mono : core. Lemma anno_range: @@ -264,7 +263,7 @@ Lemma anno_range: range (t') = (i, j). Proof. induction x; intros; ff. -Defined. +Qed. (** Lemma stating that any annotated term produced via anno is well formed *) @@ -394,7 +393,7 @@ Proof. eassumption. } tauto. -Defined. +Qed. (* Computes the length of the "span" or range of event IDs for a given Term *) (* TODO: consider changing this to event_id_span_Term *) @@ -488,4 +487,4 @@ Proof. split; eapply anno_mono; eauto. } lia. -Defined. +Qed. diff --git a/src/Appraisal_Defs.v b/src/Appraisal_Defs.v index 6e650de..044c7ee 100644 --- a/src/Appraisal_Defs.v +++ b/src/Appraisal_Defs.v @@ -1,8 +1,8 @@ (* Appraisal primitive implementations: evidence unbundling, nonce generation, appraisal ASP dispatch. *) -Require Import String Term_Defs_Core Term_Defs AM_St EqClass Maps. +Require Import String Term_Defs EqClass Maps. -Require Import Appraisal_IO_Stubs ErrorStMonad_Coq AM_Monad AM_St Manifest_Admits ErrorStringConstants Attestation_Session. +Require Import Appraisal_IO_Stubs ErrorStMonad_Coq AM_Monad ErrorStringConstants Attestation_Session. Axiom decrypt_prim_runtime : forall bs params pk e, @@ -23,12 +23,14 @@ match params with end end. +Import ErrNotation. + Definition decrypt_bs_to_rawev' (bs:BS) (params:ASP_PARAMS) (et:Evidence) : AM RawEv := ac <- get_AM_config ;; match (decrypt_bs_to_rawev bs params ac) with | resultC r => match (check_et_size et r) with - | resultC tt => ret r + | resultC tt => err_ret r | errC e => am_failm (am_dispatch_error e) end | errC e => am_failm (am_dispatch_error e) @@ -36,7 +38,7 @@ Definition decrypt_bs_to_rawev' (bs:BS) (params:ASP_PARAMS) (et:Evidence) : AM R Definition checkNonce' (nid:nat) (nonceCandidate:BS) : AM BS := nonceGolden <- am_getNonce nid ;; - ret (checkNonce nonceGolden nonceCandidate). + err_ret (checkNonce nonceGolden nonceCandidate). Definition check_asp_EXTD (params:ASP_PARAMS) (ls:RawEv) (ac : Session_Config) : ResultT RawEv DispatcherErrors := ac.(aspCb) params ls. @@ -47,7 +49,7 @@ Definition check_asp_EXTD' (params:ASP_PARAMS) (p:Plc) (sig:RawEv) (ls:RawEv) : match (map_get (ASP_to_APPR_ASP_Map ac) att_id) with | Some appr_asp => match (check_asp_EXTD (asp_paramsC appr_asp args targ targid) (app sig ls) ac) with - | resultC r => ret r + | resultC r => err_ret r | errC e => am_failm (am_dispatch_error e) end | None => am_failm (am_dispatch_error (Runtime "We made it to appraisal without a translation for our attestation ASP"%string)) diff --git a/src/Appraisal_Evidence.v b/src/Appraisal_Evidence.v index 00c217a..864b14a 100644 --- a/src/Appraisal_Evidence.v +++ b/src/Appraisal_Evidence.v @@ -4,28 +4,28 @@ Also included: properties about CVM internal Evidence and Event handling. TODO: This file has become quite bloated. May need to refactor/decompose. *) -Require Import ConcreteEvidence AutoApp Auto ResultT Helpers_CvmSemantics Term_Defs Anno_Term_Defs Cvm_St Cvm_Impl Defs StructTactics OptMonad_Coq IO_Stubs Evidence_Bundlers Axioms_Io External_Facts Attestation_Session. +Require Import ConcreteEvidence AutoApp Defs StructTactics OptMonad_Coq Anno_Term_Defs Cvm_Impl Cvm_St ResultT Axioms_Io Attestation_Session External_Facts Helpers_CvmSemantics Cvm_Monad More_lists Auto. Require Import List. -Import ListNotations. +Import ListNotations OptNotation. Require Import Lia Coq.Program.Tactics. Definition peel_bs (ls:RawEv) : Opt (BS * RawEv) := match ls with - | bs :: ls' => OptMonad_Coq.ret (bs, ls') - | _ => OptMonad_Coq.failm + | bs :: ls' => opt_ret (bs, ls') + | _ => opt_failm end. Fixpoint peel_n (n : nat) (ls : RawEv) : Opt (RawEv * RawEv) := match n with - | 0 => OptMonad_Coq.ret ([], ls) + | 0 => opt_ret ([], ls) | S n' => match ls with - | [] => OptMonad_Coq.failm + | [] => opt_failm | x :: ls' => '(ls1, ls2) <- peel_n n' ls' ;; - OptMonad_Coq.ret (x :: ls1, ls2) + opt_ret (x :: ls1, ls2) end end. @@ -36,7 +36,7 @@ Proof. intros. eapply firstn_length_le. lia. -Defined. +Qed. Lemma skipn_long: forall (e:list BS) x y, length e = x + y -> @@ -46,7 +46,7 @@ Proof. assert (length (skipn x e) = length e - x). { eapply skipn_length. } lia. -Defined. +Qed. Lemma peel_fact': forall e x y H, length e = S x -> @@ -56,7 +56,7 @@ Proof. intros. destruct e; ff; eauto. -Defined. +Qed. Lemma peel_fact: forall e x y H et, length e = S x -> @@ -68,7 +68,7 @@ Proof. econstructor. eapply peel_fact'; eauto. lia. -Defined. +Qed. Fixpoint encodeEv (e:EvidenceC) : RawEv := match e with @@ -147,14 +147,10 @@ Proof. invc H. destruct et; repeat ff; - try (unfold OptMonad_Coq.bind in *); + try (unfold opt_bind in *); repeat ff; try solve_by_inversion. - - - - eauto. - -Defined. +Qed. Ltac do_inv_recon_mt := match goal with @@ -172,7 +168,7 @@ Proof. intros. invc H. repeat ff; try solve_by_inversion; eauto. -Defined. +Qed. Ltac do_inv_recon_mt' := match goal with @@ -190,8 +186,8 @@ Lemma inv_recon_nn: forall ls et n n0, Proof. intros. invc H. - destruct et; repeat ff; try (unfold OptMonad_Coq.bind in *); repeat ff; destruct ls; try solve_by_inversion. -Defined. + destruct et; repeat ff; try (unfold opt_bind in *); repeat ff; destruct ls; try solve_by_inversion. +Qed. Ltac do_inv_recon_nn := match goal with @@ -208,7 +204,7 @@ Lemma peel_n_spec : forall n ls ls1 ls2, ls = ls1 ++ ls2 /\ length ls1 = n. Proof. induction n; intuition; repeat ff; subst; - unfold OptMonad_Coq.ret, OptMonad_Coq.bind in *; repeat ff; eauto. + unfold opt_ret, opt_bind in *; repeat ff; eauto. - eapply IHn in Heqo; intuition; subst; eauto. - eapply IHn in Heqo; intuition; subst; eauto. Qed. @@ -221,10 +217,10 @@ Proof. intuition; invc H. generalizeEverythingElse et. destruct et; repeat ff; intuition; - try (unfold OptMonad_Coq.bind, OptMonad_Coq.ret in *); + try (unfold opt_bind, opt_ret in *); repeat ff; try solve_by_inversion. eapply peel_n_spec in Heqo; intuition; subst; eauto. -Defined. +Qed. Ltac do_inv_recon_gg := match goal with @@ -247,8 +243,8 @@ Lemma inv_recon_hh: forall p ps ls et n et', Proof. intros. invc H. - destruct et; repeat ff; try (unfold OptMonad_Coq.bind in *); repeat ff; destruct ls; try solve_by_inversion. -Defined. + destruct et; repeat ff; try (unfold opt_bind in *); repeat ff; destruct ls; try solve_by_inversion. +Qed. Ltac do_inv_recon_hh := match goal with @@ -267,10 +263,10 @@ Lemma inv_recon_ee: forall p ps ls et n ec', Proof. intros. invc H. - destruct et; repeat ff; try (unfold OptMonad_Coq.bind in *); + destruct et; repeat ff; try (unfold opt_bind in *); repeat ff; destruct ls; try solve_by_inversion; repeat eexists; ff. -Defined. +Qed. Ltac do_inv_recon_ee := match goal with @@ -289,10 +285,10 @@ Lemma inv_recon_ss: forall ls et ec1 ec2, Proof. intros. invc H. - destruct et; repeat ff; try (unfold OptMonad_Coq.bind in *); + destruct et; repeat ff; try (unfold opt_bind in *); repeat ff; try solve_by_inversion; eauto. -Defined. +Qed. Ltac do_inv_recon_ss := match goal with @@ -323,11 +319,11 @@ Lemma recon_inv_gg: forall sig ls p ps et e, Proof. intros. invc H. - repeat ff; try (unfold OptMonad_Coq.bind in *); repeat ff; + repeat ff; try (unfold opt_bind in *); repeat ff; econstructor. find_apply_lem_hyp peel_n_spec; intuition; find_apply_lem_hyp app_inv_head_iff; subst; eauto. -Defined. +Qed. Ltac do_recon_inv_gg := match goal with @@ -348,7 +344,7 @@ Lemma recon_inv_ss: forall ls H1 H2 ec1 ec2, Proof. intros. invc H. - repeat ff; try (unfold OptMonad_Coq.bind in *); repeat ff; + repeat ff; try (unfold opt_bind in *); repeat ff; split; econstructor; try @@ -379,14 +375,13 @@ Proof. intros. econstructor. congruence. -Defined. +Qed. Lemma fold_recev: forall e0 e1, reconstruct_ev' e0 e1 = reconstruct_ev (evc e0 e1). Proof. - ff. - tauto. -Defined. + ffa. +Qed. Ltac do_wrap_reconP := repeat @@ -401,7 +396,7 @@ Ltac do_rewrap_reconP := | [H: reconstruct_evP (evc _ (?cc _)) _ |- _] => invc H; - repeat Auto.ff; + ffa; try rewrite fold_recev in *; do_wrap_reconP end. @@ -416,28 +411,27 @@ Proof. - (* mt case *) invc H. ff. - tauto. - (* nn case *) invc H. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. - (* uu case *) - destruct f; ff. + destruct f; ffa. + (* COMP case *) invc H. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. + (* ENCR case *) invc H. unfold reconstruct_ev in *. unfold reconstruct_ev' in *. - unfold OptMonad_Coq.bind in *. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + unfold opt_bind in *. + repeat ff; try (unfold opt_bind in * ); repeat ff. + (* EXTD case *) invc H. ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. assert (e1 = et_fun e2 ). { eapply IHe1. @@ -453,7 +447,7 @@ Proof. invc H. unfold reconstruct_ev in *. ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. assert (e1 = et_fun e2). { eapply IHe1. econstructor. @@ -466,7 +460,7 @@ Proof. - (* ss case *) invc H. ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. assert (e1_1 = et_fun e1). { eapply IHe1_1. @@ -492,7 +486,7 @@ Proof. split; destruct s; ff; try unfold mt_evc; ff; econstructor; ff. -Defined. +Qed. Ltac do_wfec_split := match goal with @@ -515,7 +509,7 @@ Lemma recon_encodeEv: forall bits et ec, Proof. intros. generalizeEverythingElse ec. - induction ec; intros. + induction ec; intros; ffa. - dd. do_inv_recon. @@ -532,7 +526,7 @@ Proof. ff. invc H. repeat ff. - unfold OptMonad_Coq.bind in *. + unfold opt_bind in *. ff. find_apply_lem_hyp peel_n_spec; intuition; subst; find_apply_lem_hyp app_inv_head_iff; subst. @@ -556,19 +550,13 @@ Proof. ff. unfold reconstruct_ev' in *. ff. - unfold OptMonad_Coq.bind in *. + unfold opt_bind in *. ff. rewrite fold_recev in *. unfold reconstruct_ev in *. unfold reconstruct_ev' in *. - destruct et; try solve_by_inversion. - ff. - unfold OptMonad_Coq.bind in *. - ff. - unfold OptMonad_Coq.bind in *. - ff. - unfold OptMonad_Coq.bind in *. - ff. + destruct et; try solve_by_inversion; + ffa using (unfold opt_bind in *). - (* kpc case *) @@ -576,35 +564,14 @@ Proof. assert (exists et', et = uu p KEEP a et'). { - destruct et; try solve_by_inversion. - + - invc H. - ff. - + - invc H. - ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. - + - invc H. - ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. - eexists. - tauto. - + - invc H. - ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + destruct et; try solve_by_inversion; + invc H; ffa using (unfold opt_bind in *). } destruct_conjs. subst. - invc H. - ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + invc H; ffa using (unfold opt_bind in *). eapply IHec. econstructor. ff. @@ -614,7 +581,7 @@ Proof. ff. invc H. ff. - unfold OptMonad_Coq.bind in *. + unfold opt_bind in *. ff. rewrite fold_recev in *. do_wrap_reconP. @@ -656,7 +623,7 @@ Proof. invc H. dd. ff. - unfold OptMonad_Coq.bind in *. + unfold opt_bind in *. ff. do_inv_recon. assert (wf_ec (evc r1 H1)). @@ -690,11 +657,11 @@ Proof. unfold reconstruct_ev' in *. destruct e0; try solve_by_inversion. ff. - unfold OptMonad_Coq.bind in *. ff. - unfold OptMonad_Coq.bind in *. ff. + unfold opt_bind in *. ff. + unfold opt_bind in *. ff. econstructor. ff. - unfold OptMonad_Coq.bind in *. ff. + unfold opt_bind in *. ff. - (* kpc case *) invc H. destruct e; try solve_by_inversion. @@ -702,9 +669,9 @@ Proof. ff. + ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. + - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. assert (wf_ec (evc r e)). { eapply IHec. econstructor. @@ -713,14 +680,14 @@ Proof. ff. + ff. - repeat ff; try (unfold OptMonad_Coq.bind in * ); repeat ff. + repeat ff; try (unfold opt_bind in * ); repeat ff. - do_inv_recon. invc H. dd. ff. - unfold OptMonad_Coq.bind in *. + unfold opt_bind in *. ff. @@ -761,7 +728,7 @@ Proof. invc H; invc H0. repeat jkjke'. ff. -Defined. +Qed. Ltac do_reconP_determ := repeat @@ -790,7 +757,7 @@ Proof. intros. destruct e; ff; eauto. -Defined. +Qed. Ltac do_some_recons' := match goal with @@ -818,7 +785,7 @@ Lemma peel_n_none_spec : forall n ls, Proof. induction n; intuition; simpl in *; repeat ff; try lia; - unfold OptMonad_Coq.ret, OptMonad_Coq.bind in *; repeat ff; eauto. + unfold opt_ret, opt_bind in *; repeat ff; eauto. eapply IHn in Heqo. lia. Qed. @@ -832,41 +799,11 @@ Proof. destruct e. generalizeEverythingElse e. induction e; intros. - - - try (repeat ff; eauto; tauto). - try - ( inv_wfec; ff; - do_some_recons'); - try ( - repeat do_rcih; - destruct_conjs; - repeat jkjke'); - try ( inv_wfec; ff; - repeat do_rcih; - destruct_conjs; - repeat jkjke'; - repeat ff; eauto). + - inv_wfec; ff. - (* nn case *) - repeat ff. - (unfold OptMonad_Coq.bind in * ). - repeat ff. - + - eauto. - + - inv_wfec. - ff. - destruct r; try solve_by_inversion. - ff. - unfold OptMonad_Coq.ret in *. - repeat ff. - - - + - destruct r; try solve_by_inversion. - ff. - invc H. - ff. + ffa using (unfold opt_bind in * ); + inv_wfec; destruct r. - (* uu case *) @@ -877,7 +814,7 @@ Proof. inv_wfec. ff. repeat ff; - (unfold OptMonad_Coq.bind in * ); + (unfold opt_bind in * ); repeat ff; eauto. ++ @@ -899,7 +836,7 @@ Proof. inv_wfec. ff. repeat ff; - (unfold OptMonad_Coq.bind in * ); + (unfold opt_bind in * ); repeat ff; eauto. ++ ff. @@ -918,7 +855,7 @@ Proof. + (* EXTD case *) inv_wfec. ff. - unfold OptMonad_Coq.bind in * ; + unfold opt_bind in * ; repeat ff; eauto; subst; eauto; try do_inv_recon. @@ -941,36 +878,34 @@ Proof. ++ assert (r = []). { eapply peel_n_none_spec in Heqo; lia. } subst; simpl in *; destruct n; simpl in *; try lia; - unfold OptMonad_Coq.ret in *; congruence. + unfold opt_ret in *; congruence. + (* KILL case *) - inv_wfec. - ff. - eauto. + inv_wfec; ff. + (* KEEP case *) inv_wfec. simpl in H1. - ff. + ffa using (unfold opt_bind in *). - repeat ff; - (unfold OptMonad_Coq.bind in * ); - repeat ff; eauto. assert (exists ee, Some ee = reconstruct_ev' r e). { eapply IHe. econstructor. eassumption. } - destruct_conjs. - congruence. - - (* ss case *) - try (ff; eauto; tauto). - inv_wfec; ff. - do_rcih. - do_rcih. - destruct_conjs. - jkjke'. - jkjke'. - ff. - eauto. + ffa. + - (* ss case *) + assert (wf_ec (evc (firstn (et_size e1) r) e1)). + { + inv_wfec; econstructor; + simpl in *; + eapply firstn_length_le; lia. + } + assert (wf_ec (evc (skipn (et_size e1) r) e2)). + { + inv_wfec; econstructor; + simpl in *. + rewrite skipn_length; lia. + } + ffa using (try break_exists; unfold opt_bind in *). Qed. Lemma some_reconsP : forall e, @@ -983,7 +918,7 @@ Proof. eexists. econstructor. eassumption. -Defined. +Qed. Ltac do_somerecons := repeat @@ -1059,7 +994,6 @@ Fixpoint cvm_evidence_denote (t:AnnoTerm) (p:Plc) (ec:EvidenceC) : EvidenceC := end. Set Warnings "-notation-overridden". -Require Import Cvm_Monad. Set Warnings "+notation-overridden". @@ -1121,26 +1055,23 @@ Proof. try ( repeat find_apply_hyp_hyp; lia). -Defined. +Qed. *) - (* asp case *) destruct a; try destruct a; - ff; try tauto; + ffa; try tauto; try (wrap_ccp_anno; ff). - (* at case *) - repeat ff; - unfold doRemote_session' in *; - repeat Auto.ff. - lia. + ffa using (cvm_monad_unfold; try lia). - (* lseq case *) wrap_ccp_anno. - destruct r; ff. - destruct u; ff. + destruct r; ffa. + destruct u; ffa. @@ -1343,7 +1274,7 @@ Proof. subst. symmetry. eapply cvm_spans; eauto. -Defined. +Qed. (** * Propositional version of span_cvm *) @@ -1378,8 +1309,8 @@ Proof. intros. inv_wfec. jkjke'. - eapply More_lists.firstn_append. -Defined. + eapply firstn_append. +Qed. Ltac do_wfec_firstn := match goal with @@ -1401,7 +1332,7 @@ Proof. inv_wfec. jkjke'. eapply More_lists.skipn_append. -Defined. +Qed. Ltac do_wfec_skipn := match goal with @@ -1452,64 +1383,33 @@ Proof. induction t1; intros. - (* asp case *) rewrite <- ccp_iff_cc in *; - simpl in *; monad_unfold; simpl in *. - repeat ff; try (econstructor; simpl in *; eauto; fail). - ff; econstructor; simpl in *; eauto. - rewrite app_length. - invc H; find_injection; find_rewrite. - rewrite EqClass.nat_eqb_eq in *; eauto. + simpl in *; cvm_monad_unfold; simpl in *. + ff; try (econstructor; simpl in *; eauto; fail). + econstructor. + rewrite app_length; + rewrite EqClass.nat_eqb_eq in *; subst; + ff. - (* at case *) - wrap_ccp; - unfold doRemote_session' in *; - monad_unfold; - repeat (break_match; subst; repeat find_rewrite; - repeat find_injection; intuition; eauto; try congruence); - find_eapply_lem_hyp check_cvm_policy_preserves_state; - simpl in *; repeat find_injection; eauto. + invc H0; repeat cvm_monad_unfold; ffa; eapply wf_ec_preserved_remote; eauto. - (* lseq case *) wrap_ccp. ff; eauto. - (* bseq case *) - wrap_ccp. - - ff; eauto. - - (* do_wfec_split. *) - - find_apply_hyp_hyp. - find_apply_hyp_hyp. - econstructor. - dd. - inv_wfec. - repeat jkjke'. - eapply app_length. + wrap_ccp; ffa. + inv_wfec; econstructor; + rewrite app_length; ffa. - (* bpar case *) - wrap_ccp. - ff; eauto. - - (* do_wfec_split. *) - - find_apply_hyp_hyp. - - inv_wfec; - ff; - econstructor; - dd; - repeat jkjke'. - - erewrite app_length. - - assert (wf_ec (evc r1 e1)). + wrap_ccp; ffa; cbn; ffa. + assert (wf_ec (evc r0 e1)). { rewrite <- Heqe1. - eapply wf_ec_preserved_par. - econstructor; eassumption. + eapply wf_ec_preserved_par; ffa. } - - solve_by_inversion. + econstructor; inv_wfec; + rewrite app_length; ffa. Qed. Ltac do_wfec_preserved := @@ -1552,17 +1452,15 @@ Proof. dd. assert (et_fun (cvm_evidence_denote annt1 p e) = aeval annt1 p (et_fun e)) by eauto. repeat jkjke. - - - dd. + - dd. jkjke. jkjke. destruct s; destruct s; destruct s0; eauto. - - - dd. + - dd. jkjke. jkjke. destruct s; destruct s; destruct s0; eauto. -Defined. +Qed. (** * Lemma: CVM execution always succeeds *) @@ -1574,7 +1472,7 @@ Proof. destruct (build_cvm t st) eqn:ee. subst. eauto. -Defined. +Qed. Ltac do_exists_some_cc t st := assert_new_proof_by @@ -1582,8 +1480,6 @@ Ltac do_exists_some_cc t st := ltac:(eapply exists_some_cc); destruct_conjs. - - (** * Helper Lemma stating: CVM traces are "cumulative" (or monotonic). Traces are only ever extended--prefixes are maintained. *) Lemma st_trace_cumul'' : forall t m k e v_full v_suffix res i ac, @@ -1604,7 +1500,7 @@ Proof. match goal with | A : ASP_Core |- _ => destruct A end; simpl in *; eauto. - * unfold nullEv in *; monad_unfold; ff; rewrite app_assoc; eauto. + * unfold nullEv in *; cvm_monad_unfold; ff; rewrite app_assoc; eauto. * ff. * ff; rewrite app_assoc; eauto. * simpl in *; @@ -1628,12 +1524,8 @@ Proof. try congruence; try rewrite app_assoc; eauto ). - (* at case *) - wrap_ccp. - repeat Auto.ff; - unfold doRemote_session' in *; - repeat Auto.ff; - repeat rewrite app_assoc; - eauto. + invc H; invc H0; + repeat cvm_monad_unfold; ffa using (try rewrite app_assoc; eauto). - (* alseq case *) repeat ff. @@ -1695,7 +1587,7 @@ Proof. + assert (errC c0 = resultC u). { - wrap_ccp_dohi. ff; + wrap_ccp_dohi; ff. rewrite <- ccp_iff_cc in *. eapply cvm_errors_deterministic. eapply Heqp5. @@ -1711,12 +1603,12 @@ Proof. } solve_by_inversion. + - assert (errC c1 = resultC u). + assert (errC c0 = resultC u). { wrap_ccp_dohi. ff. rewrite <- ccp_iff_cc in *. - eapply cvm_errors_deterministic. - eapply Heqp10. eauto. + eapply cvm_errors_deterministic; + ffa. } solve_by_inversion. + @@ -1740,7 +1632,7 @@ Proof. wrap_ccp_dohi. ff. rewrite <- ccp_iff_cc in *. eapply cvm_errors_deterministic. - eapply Heqp6. eauto. + eapply Heqp8. eauto. } solve_by_inversion. + @@ -1749,7 +1641,7 @@ Proof. wrap_ccp_dohi. ff. rewrite <- ccp_iff_cc in *. eapply cvm_errors_deterministic. - eapply Heqp6. eauto. + eapply Heqp8. eauto. } solve_by_inversion. + @@ -1806,7 +1698,7 @@ Proof. eapply st_trace_cumul''; eauto. repeat rewrite app_nil_r. eauto. -Defined. +Qed. (** * Lemma stating: CVM traces are "cumulative" (or monotonic). @@ -1849,14 +1741,10 @@ Proof. + assert (c = c0). { - edestruct cvm_errors_deterministic. - invc H2. - invc H. - apply H1. - invc H2. - apply H0. - ff. - + edestruct cvm_errors_deterministic; ffa. + invc H2; ffa. + invc H; ffa. + simpl in *; ffa. } subst. eassumption. @@ -1894,10 +1782,8 @@ Ltac do_suffix name := (_) {| st_ev := _; st_trace := ?tr'; st_evid := _; st_config := _ |} (*H2: well_formed_r ?t*) |- _] => - assert_new_proof_as_by - (exists l, tr' = tr ++ l) - ltac:(eapply suffix_prop; [apply H']) - name + fail_if_in_hyps_type (exists l, tr' = tr ++ l); + assert (exists l, tr' = tr ++ l) as name by (eapply suffix_prop; [apply H']) end. (** * Structural Lemma: Decomposes the CVM trace for the lseq phrase into the appending of the two traces @@ -2032,7 +1918,7 @@ Proof. wrap_ccp_dohi. congruence. -Defined. +Qed. Ltac do_restl := match goal with @@ -2056,7 +1942,7 @@ Proof. induction t1; intros; repeat ff; repeat jkjke. -Defined. +Qed. Axiom cvm_evidence_correct_type : forall t p e e', cvm_evidence t p e = e' -> @@ -2090,7 +1976,7 @@ Lemma doRemote_session'_sc_immut : forall t st st' res p ev, Proof. unfold doRemote_session'. intuition. - monad_unfold. + cvm_monad_unfold. ff. Qed. @@ -2098,24 +1984,7 @@ Lemma build_cvm_sc_immut : forall t st st' res, build_cvm t st = (res, st') -> st_config st = st_config st'. Proof. - induction t; simpl in *; intuition; eauto; ff. - - monad_unfold; destruct a; ff. - - repeat (monad_unfold; simpl in *; intuition; eauto; ff); - eapply doRemote_session'_sc_immut in Heqp0; eauto. - - monad_unfold; ff; eauto; - try eapply IHt1 in Heqp; - try eapply IHt2 in Heqp0; - find_rewrite; eauto. - - monad_unfold; ff; eauto; - try eapply IHt1 in Heqp; - try eapply IHt2 in Heqp4; - simpl in *; eauto; - find_rewrite; eauto. - - monad_unfold; ff; eauto; - try eapply IHt1 in Heqp; - try eapply IHt2 in Heqp4; - simpl in *; eauto; - find_rewrite; eauto. + induction t; simpl in *; intuition; eauto; ffa using cvm_monad_unfold. Qed. Lemma build_cvmP_sc_immut : forall t st st' res, @@ -2143,18 +2012,14 @@ Proof. - (* aasp case *) rewrite <- ccp_iff_cc in *. - - Auto.ff. - destruct a; - (try dd; eauto); try (repeat Auto.ff). + ffa. + destruct a; (try dd; eauto); ffa using cvm_monad_unfold. - (* at case *) rewrite <- ccp_iff_cc in *. dd. - repeat Auto.ff. - unfold doRemote_session' in *; - repeat Auto.ff. + repeat ffa. - (* alseq case *) do_suffix blah. @@ -2187,7 +2052,7 @@ Proof. - (* abseq case *) simpl in *; repeat ff; subst; - wrap_ccp; repeat ff; + wrap_ccp; cbn in *; repeat ff; cbn in *; repeat match goal with | x : EvC |- _ => destruct x @@ -2211,23 +2076,20 @@ Proof. - (* abpar case *) - destruct s; repeat Auto.ff. - + destruct s; repeat ffa; + wrap_ccp; cbn in *; repeat ff; cbn in *; + repeat (ffa; match goal with + | u : unit |- _ => + destruct u + end). + - wrap_ccp. - Auto.ff. - find_apply_hyp_hyp. - - assert (e0 = eval t2 (session_plc ac') et). { eapply par_evidence_r; eauto. } - congruence. + ffa. + - wrap_ccp. - Auto.ff. find_apply_hyp_hyp. assert (e0 = eval t2 (session_plc ac') mt). @@ -2235,13 +2097,10 @@ Proof. rewrite par_evidence_clear in *. eapply par_evidence_r; eauto. } - congruence. + wrap_ccp. - Auto.ff. - find_apply_hyp_hyp. - + ffa. assert (e0 = eval t2 (session_plc ac') et). { eapply par_evidence_r; eauto. @@ -2249,9 +2108,7 @@ Proof. congruence. + wrap_ccp. - Auto.ff. - find_apply_hyp_hyp. - + ffa. assert (e0 = eval t2 (session_plc ac') mt). { rewrite par_evidence_clear in *. @@ -2276,41 +2133,6 @@ Proof. eapply cvm_refines_lts_evidence'. eauto. Qed. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - (** BEGIN Deprecated parallel annotated term stuff *) @@ -2324,7 +2146,7 @@ Proof. econstructor. eexists. jkjke. -Defined. +Qed. (* Lemma anno_parPloc_redo: forall t pt loc loc', @@ -2334,7 +2156,7 @@ Proof. intros. econstructor. jkjke. -Defined. +Qed. *) Lemma anno_parPloc_redo: forall t pt loc loc', anno_par_list' t loc = Some (loc', pt) -> @@ -2343,7 +2165,7 @@ Proof. intros. econstructor. jkjke. -Defined. +Qed. *) diff --git a/src/Appraisal_IO_Stubs.v b/src/Appraisal_IO_Stubs.v index 36f4783..f974307 100644 --- a/src/Appraisal_IO_Stubs.v +++ b/src/Appraisal_IO_Stubs.v @@ -1,8 +1,8 @@ (* Admitted definitions of external IO operations required by Appraisal. *) -Require Import ResultT Term_Defs_Core Term_Defs. +Require Import ResultT Term_Defs_Core. -Require Import Manifest_Admits ErrorStMonad_Coq Cvm_St AM_St Attestation_Session. +Require Import Manifest_Admits AM_St Attestation_Session. Require Import String ErrorStringConstants. diff --git a/src/Attestation_Session.v b/src/Attestation_Session.v index f3f0524..8efddb9 100644 --- a/src/Attestation_Session.v +++ b/src/Attestation_Session.v @@ -1,5 +1,5 @@ Require Import Maps Term_Defs_Core Manifest. -Require Import String List ResultT. +Require Import String List. Require Import JSON Stringifiable. Import ListNotations. diff --git a/src/Auto.v b/src/Auto.v index a72bdb7..1b9705a 100644 --- a/src/Auto.v +++ b/src/Auto.v @@ -4,8 +4,7 @@ Author: Adam Petz, ampetz@ku.edu *) -Require Import StructTactics Cvm_Monad Term_Defs Term. -Require Import Coq.Arith.Peano_dec Lia. +Require Import StructTactics Cvm_Monad. Require Export Defs. @@ -23,17 +22,12 @@ Ltac annogo := vmsts; repeat dunit. custom unfolders. *) Ltac df := repeat ( - cbn in *; - unfold runErr in *; - repeat break_let; - repeat (monad_unfold; cbn in *; find_inversion); - monad_unfold; - repeat dunit; - unfold snd in * ). - -(* Common "first swipe" automation tactic throughout this development. - Breaks match statements if found, then either solves or simplifies. *) -Ltac ff := repeat break_match; try solve_by_inversion; df. + simpl in *; + repeat break_let; + repeat (cvm_monad_unfold; simpl in *; find_inversion); + cvm_monad_unfold; + repeat dunit; + unfold snd in * ). (* Destruct specific matches on Option types *) Ltac dosome := @@ -48,24 +42,6 @@ Ltac dosome := destruct o; try solve_by_inversion end; df). -(* Smarter rewriter *) -Ltac subst' := - match goal with - | [H: ?A = _, H2: context[?A] |- _] => rewrite H in *; clear H - | [H: ?A = _ |- context[?A]] => rewrite H in *; clear H - end. - -(* Same as subst', but does NOT clear hyps after rewriting *) -Ltac subst'' := - match goal with - | [H:?A = _, H2: context [?A] |- _] => rewrite H in * - | [H:?A = _ |- context [?A]] => rewrite H in * - end. - -Ltac assert_new_proof_as_by H tac n := - fail_if_in_hyps_type H; - assert H as n by tac. - (* Slight (non-existential) variation of `jkjke` from Defs.v *) Ltac jkjk_s := match goal with diff --git a/src/AutoApp.v b/src/AutoApp.v index 01319ca..3bb737a 100644 --- a/src/AutoApp.v +++ b/src/AutoApp.v @@ -1,8 +1,7 @@ (* Misc automation tactics. TODO: Some of these might be repeats or overlap. *) -Require Import StructTactics Auto Cvm_St Cvm_Monad ErrorStMonad_Coq Cvm_Impl. -Require Import List. +Require Import StructTactics Auto Cvm_Monad. Ltac dosome_eq y := match goal with @@ -55,7 +54,7 @@ Ltac haaa := Ltac stt := cbn in *; - monad_unfold; + cvm_monad_unfold; try solve_by_inversion; repeat break_let; dosome; diff --git a/src/Axioms_Io.v b/src/Axioms_Io.v index 76a93b4..c80b449 100644 --- a/src/Axioms_Io.v +++ b/src/Axioms_Io.v @@ -4,9 +4,8 @@ Uninterpreted functions and rewrite rules that model external (remote and local Author: Adam Petz, ampetz@ku.edu *) -Require Import Term_Defs Anno_Term_Defs Interface LTS IO_Stubs ResultT Cvm_St Attestation_Session Maps. +Require Import Term_Defs Anno_Term_Defs Interface LTS IO_Stubs. -Require Import List. Import ListNotations. (** IO Axioms *) diff --git a/src/Client_AM.v b/src/Client_AM.v index 37f035e..e9f8508 100644 --- a/src/Client_AM.v +++ b/src/Client_AM.v @@ -1,8 +1,8 @@ (* Implementation of a top-level Client (initiator) thread for Client AMs in end-to-end Copland Attestation + Appraisal protocols. *) -Require Import String List. +Require Import String. -Require Import Term Cvm_Run EqClass Cvm_St. +Require Import Term EqClass. Require Import Impl_appraisal Appraisal_IO_Stubs IO_Stubs AM_Monad ErrorStMonad_Coq. @@ -12,9 +12,7 @@ Require Import Disclose ErrorStringConstants Manifest_Admits. Require Import AM_Helpers Auto. -Require Import StructTactics Coq.Program.Tactics. - -Import ListNotations. +Import ListNotations ErrNotation. (* Set Nested Proofs Allowed. @@ -54,11 +52,11 @@ Definition am_sendReq_app (uuid : UUID) (att_sess : Attestation_Session) (t:Term Definition gen_nonce_if_none_local (initEv:option EvC) : AM EvC := match initEv with - | Some (evc ebits et) => ret mt_evc - | None => - let nonce_bits := gen_nonce_bits in - nid <- am_newNonce nonce_bits ;; - ret (evc [nonce_bits] (nn nid)) + | Some (evc ebits et) => err_ret mt_evc + | None => + let nonce_bits := gen_nonce_bits in + nid <- am_newNonce nonce_bits ;; + err_ret (evc [nonce_bits] (nn nid)) end. (* Definition gen_authEvC_if_some (ot:option Term) (uuid : UUID) (myPlc:Plc) (init_evc:EvC) : AM EvC := @@ -94,7 +92,7 @@ Definition run_demo_client_AM (t:Term) (top_plc:Plc) (att_plc:Plc) (et:Evidence) Definition check_et_length (et:Evidence) (ls:RawEv) : AM unit := if (eqb (et_size et) (length ls)) -then ret tt +then err_ret tt else (am_failm (am_dispatch_error (Runtime errStr_et_size))). Definition am_appraise (att_sess : Attestation_Session) (t:Term) (toPlc:Plc) (init_et:Evidence) (cvm_ev:RawEv) (apprUUID : UUID) (local_appraisal:bool) : AM AppResultC := @@ -109,13 +107,13 @@ Definition am_appraise (att_sess : Attestation_Session) (t:Term) (toPlc:Plc) (in | false => match run_appraisal_client att_sess t toPlc init_et cvm_ev apprUUID with | errC msg => am_failm (am_dispatch_error (Runtime msg)) - | resultC res => ret res + | resultC res => err_ret res end end) ;; (* let expected_et := eval t toPlc init_et in app_res <- gen_appraise_AM expected_et cvm_ev ;; *) - ret (app_res). + err_ret (app_res). @@ -247,8 +245,6 @@ Definition check_disclosure_policy (t:Term) (p:Plc) (e:Evidence) : AM unit := ret (am_appev app_res). *) -Require Import Auto. - Fixpoint nonce_ids_et' (et:Evidence) (ls:list N_ID) : list N_ID := match et with | mt => ls @@ -276,13 +272,8 @@ Lemma no_nonces'' : forall et ls, no_nonces_pred et -> nonce_ids_et' et ls = ls. Proof. - induction et; intros; ff. - - - invc H. - eauto. - - - invc H. - erewrite IHet1; eauto. + induction et; intros; ffa. + erewrite IHet1; ff. Qed. @@ -290,40 +281,10 @@ Lemma no_nonces_eval : forall t p et, no_nonces_pred et -> no_nonces_pred (eval t p et). Proof. - induction t; intros; ff. - - - destruct a; ff. - + - econstructor. - + - destruct f; ff. - ++ - econstructor. - destruct s; ff. - econstructor. - ++ - econstructor. - destruct s; ff. - econstructor. - ++ - econstructor. - destruct s; ff. - econstructor. - ++ - econstructor. - ++ - destruct s; ff. - econstructor. - + - econstructor; eauto. - + - econstructor; eauto. - + - econstructor; eauto. - - - eauto. - - - eauto. + induction t; intros; ffa. + - destruct a; ffa using (econstructor). + simpl in *; ff; try econstructor; simpl in *; + destruct s; ff; econstructor. - destruct s. destruct s; destruct s0; ff. @@ -373,15 +334,12 @@ no_nonces_pred et -> nonce_ids_et' (eval t p et) ls = ls. Proof. induction t; intros; try (ff; congruence). - - - ff. + - ff. unfold eval_asp in *. destruct a; ff; subst; try destruct s; ff; try eapply no_nonces''; eauto. - - - eauto. - ff. @@ -451,11 +409,8 @@ Lemma nid_in_gen : forall et ls nid ls', In nid (nonce_ids_et' et ls) -> In nid ls \/ In nid (nonce_ids_et' et ls'). Proof. - induction et; intros; ff. - - - door; ff. - - - eauto. + induction et; intros; ffa; + simpl in *. - edestruct IHet2. eassumption. @@ -472,10 +427,10 @@ Proof. Qed. Lemma nonce_ids_ss_decom : forall nid et1 et2 ls, -In nid (nonce_ids_et' et2 (nonce_ids_et' et1 ls)) -> -In nid ls \/ -In nid (nonce_ids_et' et1 []) \/ -In nid (nonce_ids_et' et2 []). + In nid (nonce_ids_et' et2 (nonce_ids_et' et1 ls)) -> + In nid ls \/ + In nid (nonce_ids_et' et1 []) \/ + In nid (nonce_ids_et' et2 []). Proof. intros. eapply nid_in_gen with (ls' := []) in H. @@ -486,18 +441,12 @@ Proof. Qed. Lemma nonce_ids_et_cumul_nil: forall nid et ls, -In nid (nonce_ids_et' et []) -> -In nid (nonce_ids_et' et ls). + In nid (nonce_ids_et' et []) -> + In nid (nonce_ids_et' et ls). Proof. - induction et; intros; ff. - - - door; try solve_by_inversion. + induction et; intros; ffa using intuition. - - eauto. - - - edestruct nonce_ids_ss_decom; eauto. - - solve_by_inversion. + edestruct nonce_ids_ss_decom; ffa. door. @@ -507,29 +456,15 @@ Proof. eapply nonce_ids_et_cumul; eauto. eauto. - Qed. +Qed. Lemma nid_nonce_ids_eval : forall t p et ls nid, In nid (nonce_ids_et' (eval t p et) ls) -> In nid ls \/ In nid (nonce_ids_et' et []). Proof. induction t; intros; ff. - - - destruct a; ff. - + - eapply nid_in_gen; auto. - + - destruct f; ff; - destruct s; ff; - eapply nid_in_gen; auto. - + - eapply nid_in_gen; auto. - + - eapply nid_in_gen; auto. - + - eapply nid_in_gen; auto. - - - eauto. + - destruct a; ffa; try eapply nid_in_gen; auto; + destruct s; ffa; eapply nonce_ids_et_cumul; eauto. - assert ( In nid ls \/ diff --git a/src/ConcreteEvidence.v b/src/ConcreteEvidence.v index e9a9166..8a5f3b8 100644 --- a/src/ConcreteEvidence.v +++ b/src/ConcreteEvidence.v @@ -100,7 +100,7 @@ Proof. induction e''; intros; try evSubTFacts; eauto. -Defined. +Qed. (** Typed Concrete Evidence subterm relation *) Inductive EvSub: EvidenceC -> EvidenceC -> Prop := @@ -133,7 +133,7 @@ Proof. intros. induction H; intros; cbn in *; eauto. -Defined. +Qed. Lemma evsub_hh: forall e e' e0, EvSub e0 e' -> @@ -199,4 +199,4 @@ Proof. intros e e' e'' H H0. generalizeEverythingElse e''. induction e''; intros; ff; invc H0; eauto. -Defined. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/src/CvmSemantics.v b/src/CvmSemantics.v index ba69c83..96f98de 100644 --- a/src/CvmSemantics.v +++ b/src/CvmSemantics.v @@ -5,13 +5,12 @@ Author: Adam Petz, ampetz@ku.edu *) -Require Import More_lists Defs Term_Defs Anno_Term_Defs ConcreteEvidence LTS Event_system Term_system Main Appraisal_Evidence AutoApp. -Require Import ResultT Term Cvm_Monad StructTactics Auto. -Require Import Axioms_Io Cvm_Impl Cvm_Run External_Facts Helpers_CvmSemantics Evidence_Bundlers Attestation_Session. +Require Import Anno_Term_Defs ConcreteEvidence Appraisal_Evidence AutoApp Main. +Require Import ResultT Cvm_Monad Auto External_Facts. +Require Import Axioms_Io Helpers_CvmSemantics Attestation_Session. -Require Import List. Import ListNotations. -Require Import Coq.Program.Tactics Coq.Program.Equality. +Require Import Coq.Program.Tactics. Require Import Coq.Arith.Peano_dec Lia. @@ -26,7 +25,7 @@ Lemma splitEv_T_l_LEFT: forall e bits bits' es e0 sp, Proof. intros. ff. -Defined. +Qed. Lemma aeval_anno: forall a i n e0, (aeval (snd (anno (unanno a) i)) n e0 = aeval a n e0). @@ -36,26 +35,26 @@ Proof. induction a; intros; ff; repeat jkjke'; repeat jkjke. -Defined. +Qed. Lemma evc_inv: forall e, e = evc (get_bits e) (get_et e). Proof. destruct e; eauto. -Defined. +Qed. Lemma front_app{A} : forall (x:A) xs ys, x :: xs ++ ys = [x] ++ xs ++ ys. Proof. tauto. -Defined. +Qed. Lemma back_app{A:Type}: forall (x y:A), [x; y] = [x] ++ [y]. Proof. tauto. -Defined. +Qed. Ltac inv_wfec := repeat @@ -71,7 +70,7 @@ Proof. inv_wfec. jkjke'. eapply More_lists.firstn_append. -Defined. +Qed. Ltac do_wfec_firstn := match goal with @@ -93,7 +92,7 @@ Proof. inv_wfec. jkjke'. eapply More_lists.skipn_append. -Defined. +Qed. Ltac do_wfec_skipn := match goal with @@ -129,7 +128,7 @@ Proof. dd; try (erewrite app_length); jkjke). -Defined. +Qed. (* TODO: this lemma does not hold for (Some eec ... = Some mtc) case @@ -188,7 +187,7 @@ Proof. intros. destruct e; ff; eauto. -Defined. +Qed. Ltac do_some_recons' := match goal with @@ -217,16 +216,7 @@ Lemma event_id_spans_same : forall t, Proof. intros. induction t; ff. - - - destruct a; ff; try tauto. - + - destruct s; ff. - - - jkjke'. - - - destruct s0; ff; lia. - - - destruct s0; ff; lia. + - unfold asp_term_to_core; ffa. Qed. (** * Lemma: CVM increases event IDs according to event_id_span' denotation. *) @@ -269,7 +259,7 @@ Lemma span_cvm: forall atp t annt i j e e' tr tr' i' ac ac', j = i'. Proof. eapply span_cvm. -Defined. +Qed. (** * Propositional version of span_cvm *) Lemma anno_span_cvm: forall t pt annt i i' e e' tr tr' st_evid1 ac ac', @@ -323,7 +313,7 @@ Theorem cvm_refines_lts_events : Proof. intros t atp annt cvm_tr bits bits' et et' i i' ac ac' annoParPH annPH H'. generalizeEverythingElse t. - induction t; intros. + induction t; intros; ffa. - (* aasp case *) wrap_ccp_anno. @@ -331,85 +321,19 @@ Proof. destruct a; invc annoParPH; ff; wrap_ccp_anno; - try (econstructor; econstructor; reflexivity). - destruct f. - + - ff. - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - ff. - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - ff. - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - ff. - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - ff. - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - ++ - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - + - wrap_ccp_anno. - repeat Auto.ff. - try (econstructor; econstructor; reflexivity). - - + try (econstructor; econstructor; reflexivity); ffa; + wrap_ccp_anno; econstructor; econstructor. - (* aatt case *) wrap_ccp_anno. - unfold doRemote_session' in *; - repeat ff. - + ff. assert (n = i + event_id_span' t + 1) by lia. subst. (* clear H2. *) assert (t = unanno a) as HN. { - invc Heqp3. + invc Heqp1. erewrite <- anno_unanno at 1. rewrite H. @@ -523,9 +447,12 @@ Proof. - (* abseq case *) wrap_ccp_anno; - repeat Auto.ff; + repeat (try cbn in *; ff); wrap_ccp_anno; - repeat Auto.ff; + repeat (try cbn in *; ff); + repeat match goal with + | u : unit |- _ => destruct u + end; repeat do_sc_immut. + @@ -595,13 +522,8 @@ Proof. eassumption. assert (st_evid = Nat.pred (st_evid + 1)) by lia. - rewrite H2 in *. - - + ffa. econstructor; eauto; simpl in *. - assert (Nat.pred (st_evid + 1) + 1 = st_evid + 1) by lia. - rewrite H3 in *. - eauto. + assert (n = st_evid1). @@ -673,7 +595,7 @@ Proof. eassumption. assert (st_evid = Nat.pred (st_evid + 1)) by lia. - rewrite H2 at 2. + ffa. econstructor. @@ -753,7 +675,7 @@ Proof. eassumption. assert (st_evid = Nat.pred (st_evid + 1)) by lia. - rewrite H2 at 2. + ffa. econstructor. @@ -833,7 +755,7 @@ Proof. eassumption. assert (st_evid = Nat.pred (st_evid + 1)) by lia. - rewrite H2 at 2. + ffa. econstructor. @@ -844,10 +766,13 @@ Proof. - (* abpar case *) wrap_ccp_anno; - repeat Auto.ff; + repeat (try cbn in *; ff); wrap_ccp_anno; - repeat Auto.ff; - do_sc_immut. + repeat (try cbn in *; ff); + repeat match goal with + | u : unit |- _ => destruct u + end; + repeat do_sc_immut. + @@ -864,7 +789,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H4. + subst. @@ -918,7 +843,7 @@ Proof. eassumption. assert ((st_evid + event_id_span (copland_compile t2)) = Nat.pred ((st_evid + event_id_span (copland_compile t2)) + 1)) by lia. - rewrite H2 at 2. + ffa. eapply lstar_tran. @@ -940,7 +865,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H4. + subst. do_suffix blah. @@ -981,7 +906,7 @@ Proof. } repeat rewrite app_assoc in *. - rewrite H1. + rewrite H2. rewrite events_cvm_to_core_mt. @@ -994,7 +919,7 @@ Proof. eassumption. assert ((st_evid + event_id_span (copland_compile t2)) = Nat.pred ((st_evid + event_id_span (copland_compile t2)) + 1)) by lia. - rewrite H2 at 2. + ffa. eapply lstar_tran. @@ -1016,7 +941,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H4. + subst. do_suffix blah. @@ -1057,7 +982,7 @@ Proof. } repeat rewrite app_assoc in *. - rewrite H1. + rewrite H2. eapply lstar_transitive. @@ -1068,7 +993,7 @@ Proof. eassumption. assert ((st_evid + event_id_span (copland_compile t2)) = Nat.pred ((st_evid + event_id_span (copland_compile t2)) + 1)) by lia. - rewrite H2 at 2. + ffa. eapply lstar_tran. @@ -1091,7 +1016,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H4. + subst. @@ -1134,7 +1059,7 @@ Proof. } repeat rewrite app_assoc in *. - rewrite H1. + rewrite H2. rewrite events_cvm_to_core_mt. @@ -1147,7 +1072,7 @@ Proof. eassumption. assert ((st_evid + event_id_span (copland_compile t2)) = Nat.pred ((st_evid + event_id_span (copland_compile t2)) + 1)) by lia. - rewrite H2 at 2. + ffa. eapply lstar_tran. @@ -1225,7 +1150,6 @@ build_cvmP (copland_compile t1) |}. Proof. ff. - eauto. Qed. Axiom cvm_thread_start_clear : forall t p e n, @@ -1259,10 +1183,10 @@ Proof. induction t; intros. - (* asp case *) wrap_ccp_anno; - repeat Auto.ff; - destruct a; invc H; repeat Auto.ff; + repeat ff; + destruct a; invc H; repeat ff; wrap_ccp_anno; - repeat Auto.ff; + repeat ff; try destruct s; wrap_ccp_anno; try destruct f; try destruct H1; @@ -1273,12 +1197,9 @@ Proof. - wrap_ccp_anno. ff. - unfold Cvm_Monad.doRemote_session' in *; - repeat Auto.ff. assert (n = cvmi + event_id_span' t + 1) by lia. subst. - clear H5. assert (t = unanno a) as H11. { @@ -1314,43 +1235,31 @@ Proof. try solve_by_inversion. } - door; ff; eauto. - - assert ( - build_cvm (copland_compile t) - {| st_ev := (evc bits e); - st_trace := []; - st_evid := (S cvmi); st_config := ac' |} = - (resultC tt, - {| st_ev := cvm_evidence_core (copland_compile t) (session_plc ac') (evc bits e); - st_trace := cvm_events_core (copland_compile t) (session_plc ac') (get_et (evc bits e)); - st_evid := ( (S cvmi) + event_id_span (copland_compile t)); - st_config := ac' - |})). { - apply build_cvm_external. - } - - destruct (cvm_evidence_core (copland_compile t) p (evc bits e)). - unfold cvm_events in *. - - econstructor. - admit. - - (* eapply IHt; admit. [ | simpl in *; econstructor; eauto | eauto ]. - 2: { *) - subst; rewrite eval_aeval'; apply evtsattrpy; - simpl; lia. - (* } + door; ffa using cvm_monad_unfold; eauto; + try (subst; rewrite eval_aeval'; apply evtsattrpy; simpl; lia). econstructor. - - invc Heqp1. - repeat ff. - rewrite <- event_id_spans_same. + assert (exists ac, p = (session_plc ac)). + { + exists (Build_Session_Config p (ASP_to_APPR_ASP_Map ac') + (aspCb ac') (plc_map ac') (pubkey_map ac') (policy ac')); + ffa. + } + break_exists. + ffa. + pose proof (build_cvm_external (copland_compile (unanno a)) + (evc bits e) (S cvmi) x). simpl in *. - assert (S (cvmi + event_id_span' (unanno a)) = - cvmi + event_id_span' (unanno a) + 1) by lia. - rewrite H4. - eassumption. *) + rewrite ccp_iff_cc in *. + unfold cvm_events. + pose proof (cvm_evidence_exists_remote + (copland_compile (unanno a)) (session_plc x) (evc bits e)). + break_exists. + find_rewrite. + repeat rewrite event_id_works in *. + repeat rewrite <- event_id_works in *. + rewrite PeanoNat.Nat.add_1_r in *. + eapply IHt; eauto. + - (* alseq case *) invc H. edestruct alseq_decomp; eauto. @@ -1391,12 +1300,7 @@ Proof. door. + - apply evtslseql. - eapply IHt1. - econstructor. - eassumption. - eassumption. - eassumption. + apply evtslseql; ffa. + @@ -1407,10 +1311,11 @@ Proof. assert (t1 = unanno a). { symmetry. - invc Heqp1. + match goal with + | H : annoP_indexed _ t1 _ _ |- _ => invc H + end. erewrite <- anno_unanno. - rewrite H9. - tauto. + rewrite H8; ffa. } eapply cvm_refines_lts_evidence. econstructor; eauto. @@ -1420,7 +1325,9 @@ Proof. find_rewrite. - invc Heqp2. + match goal with + | H : annoP_indexed _ t2 _ _ |- _ => invc H + end. apply evtslseqr. eapply IHt2. econstructor. @@ -1429,10 +1336,14 @@ Proof. eassumption. - (* abseq case *) wrap_ccp_anno; - repeat Auto.ff; + repeat (try cbn in *; ff); wrap_ccp_anno; - repeat Auto.ff; + repeat (try cbn in *; ff); + repeat match goal with + | u : unit |- _ => destruct u + end; repeat do_sc_immut. + + assert (n = st_evid1). @@ -1791,11 +1702,15 @@ Proof. - (* abpar case *) wrap_ccp_anno; - Auto.ff; + repeat (try cbn in *; ff); wrap_ccp_anno; - Auto.ff; + repeat (try cbn in *; ff); + repeat match goal with + | u : unit |- _ => destruct u + end; repeat do_sc_immut. + + assert (n = st_evid). @@ -1812,7 +1727,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H6. + subst. @@ -1893,7 +1808,7 @@ Proof. door. - invc H3; try solve_by_inversion. + invc H4; try solve_by_inversion. door. @@ -1907,14 +1822,14 @@ Proof. eapply cvm_evidence_exists_remote. } destruct_conjs. - rewrite H6 in *. + rewrite H7 in *. eapply IHt2. eassumption. simpl. econstructor. eassumption. - apply H3. + ffa. door. @@ -1924,34 +1839,16 @@ Proof. eassumption. simpl. assert (S cvmi = cvmi + 1) by lia. - rewrite H4. + rewrite H5. eapply restl. eassumption. eassumption. - invc H3; try solve_by_inversion. - - eapply evtsbparjoin. - simpl. - lia. - - eauto. - - (* - - eapply evtsbparsplit. - simpl; eauto. - solve_by_inversion. - - admit. (* TODO: axiom? *) - eauto. - - *) - - + invc H4; try solve_by_inversion; subst. + auto. subst. - apply evtsbparjoin. + eapply evtsbparjoin. simpl. lia. @@ -1970,7 +1867,7 @@ Proof. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H6. + subst. @@ -2025,114 +1922,88 @@ Proof. In ev (cvm_events_core (copland_compile t2) (session_plc ac') mt) \/ In ev blah \/ In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). -{ - -invc H1. -left; eauto. -auto with *. - - - -Unset Printing Notations. - -assert (In ev ([cvm_thread_start 0 (session_plc ac') (copland_compile t2) mt] ++ blah ++ [cvm_thread_end 0]) \/ - In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). - { - assert ( - (cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e) = - (cvm_thread_start 0 (session_plc ac') (copland_compile t2)) mt). - { - eapply cvm_thread_start_clear. - } - rewrite H1 in *; clear H1. - - auto with *. - - } - - invc H1. - - assert (In ev (cvm_events_core (copland_compile t2) (session_plc ac') mt) \/ - In ev blah). - { - eapply cvm_thread_in_ev; eassumption. - } - - door. - eauto. - eauto. - eauto. - -} - -door. + { -invc H3; try solve_by_inversion. + invc H1. + left; eauto. + auto with *. -door. -eapply evtsbparr. -pose (build_cvm_external (copland_compile t2) (evc bits mt) st_evid ac'). + Unset Printing Notations. -assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits mt) = -evc b et). -{ - eapply cvm_evidence_exists_remote. -} -destruct_conjs. -rewrite H6 in *. + assert (In ev ([cvm_thread_start 0 (session_plc ac') (copland_compile t2) mt] ++ blah ++ [cvm_thread_end 0]) \/ + In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). + { + assert ( + (cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e) = + (cvm_thread_start 0 (session_plc ac') (copland_compile t2)) mt). + { + eapply cvm_thread_start_clear. + } + rewrite H1 in *; clear H1. -eapply IHt2. -eassumption. -econstructor. -simpl. -eassumption. + auto with *. -apply H3. + } + invc H1. -door. + assert (In ev (cvm_events_core (copland_compile t2) (session_plc ac') mt) \/ + In ev blah). + { + eapply cvm_thread_in_ev; eassumption. + } -apply evtsbparl. -eapply IHt1. + door. + eauto. + eauto. + eauto. -eassumption. -simpl. -assert (S cvmi = cvmi + 1) by lia. -rewrite H4. -eapply restl. -eassumption. -eassumption. + } -invc H3; try solve_by_inversion. + door. -eapply evtsbparjoin. -simpl. -lia. + invc H4; try solve_by_inversion. + door. + eapply evtsbparr. -eauto. + pose (build_cvm_external (copland_compile t2) (evc bits mt) st_evid ac'). -(* + assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits mt) = + evc b et). + { + eapply cvm_evidence_exists_remote. + } + destruct_conjs. + rewrite H7 in *. -eapply evtsbparsplit. -simpl; eauto. -solve_by_inversion. + eapply IHt2. + eassumption. + econstructor. + simpl. + eassumption. -admit. (* TODO: axiom? *) -eauto. + apply H4. -*) + door. + apply evtsbparl. + eapply IHt1. - subst. + eassumption. + simpl. + assert (S cvmi = cvmi + 1) by lia. + rewrite H5. + eapply restl. + eassumption. + eassumption. - apply evtsbparjoin. - simpl. - lia. + invc H4; try solve_by_inversion. + ffa. + assert (n = st_evid). @@ -2148,7 +2019,7 @@ eauto. assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - subst. clear H6. + subst. @@ -2203,266 +2074,210 @@ eauto. In ev (cvm_events_core (copland_compile t2) (session_plc ac') e) \/ In ev blah \/ In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). -{ - -invc H1. -left; eauto. -auto with *. - -assert (In ev ([cvm_thread_start 0 (session_plc ac') (copland_compile t2) e] ++ blah ++ [cvm_thread_end 0]) \/ - In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). - { - auto with *. - } - - invc H1. - - assert (In ev (cvm_events_core (copland_compile t2) (session_plc ac') e) \/ - In ev blah). - { - eapply cvm_thread_in_ev; eassumption. - } - - door. - eauto. - eauto. - eauto. - -} - -door. - -invc H3; try solve_by_inversion. - -door. - -eapply evtsbparr. - - - -pose (build_cvm_external (copland_compile t2) (evc bits e) st_evid ac'). - -assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits e) = -evc b et). -{ - eapply cvm_evidence_exists_remote. -} -destruct_conjs. -rewrite H6 in *. + { + invc H1. + left; eauto. + auto with *. + assert (In ev ([cvm_thread_start 0 (session_plc ac') (copland_compile t2) e] ++ blah ++ [cvm_thread_end 0]) \/ + In ev [join (st_evid + event_id_span (copland_compile t2)) (session_plc ac')]). + { + auto with *. + } -eapply IHt2. -eassumption. + invc H1. -simpl. -econstructor. -eassumption. + assert (In ev (cvm_events_core (copland_compile t2) (session_plc ac') e) \/ + In ev blah). + { + eapply cvm_thread_in_ev; eassumption. + } -apply H3. + door. + eauto. + eauto. + eauto. + } -door. + door. -apply evtsbparl. -eapply IHt1. + invc H4; try solve_by_inversion. -eassumption. -simpl. -assert (S cvmi = cvmi + 1) by lia. -rewrite H4. -eapply restl. -eassumption. -eassumption. + door. -invc H3; try solve_by_inversion. + eapply evtsbparr. -eapply evtsbparjoin. -simpl. -lia. + pose (build_cvm_external (copland_compile t2) (evc bits e) st_evid ac'). -eauto. + assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits e) = + evc b et). + { + eapply cvm_evidence_exists_remote. + } + destruct_conjs. + rewrite H7 in *. -(* -eapply evtsbparsplit. -simpl; eauto. -solve_by_inversion. -admit. (* TODO: axiom? *) -eauto. + eapply IHt2. + eassumption. -*) + simpl. + econstructor. + eassumption. + apply H4. - subst. - apply evtsbparjoin. - simpl. - lia. + door. - + - assert (n = st_evid). - { - assert (cvmi+1 = S cvmi) by lia. - find_rewrite. - invc Heqp. - - eapply span_cvm; eauto. - econstructor; tauto. - } - subst. + apply evtsbparl. + eapply IHt1. - assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. - - subst. clear H6. - - - - do_suffix blah. + eassumption. + simpl. + assert (S cvmi = cvmi + 1) by lia. + rewrite H5. + eapply restl. + eassumption. + eassumption. - destruct_conjs; subst. - repeat do_restl. + invc H4; try solve_by_inversion. + auto. + ffa. - assert (ev = Term_Defs.split cvmi (session_plc ac') \/ - In ev ([cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e] ++ blah ++ - [cvm_thread_end 0]) \/ - ev = join (st_evid + event_id_span (copland_compile t2)) (session_plc ac') - ). - { - apply in_app_or in H1. - door. + - assert( - (([Term_Defs.split cvmi (session_plc ac'); - cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e] ++ blah) ++ - [cvm_thread_end 0]) = - ([Term_Defs.split cvmi (session_plc ac')] ++ - ([(cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e)] ++ blah ++ - [cvm_thread_end 0]))). + assert (n = st_evid). { - simpl. - tauto. + assert (cvmi+1 = S cvmi) by lia. + find_rewrite. + invc Heqp. + + eapply span_cvm; eauto. + econstructor; tauto. } - rewrite H1 in H0. + subst. - apply in_app_or in H0. + assert (n0 = st_evid + event_id_span (copland_compile t2)) by lia. + + subst. + + + + do_suffix blah. + + destruct_conjs; subst. + repeat do_restl. + + assert (ev = Term_Defs.split cvmi (session_plc ac') \/ + In ev ([cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e] ++ blah ++ + [cvm_thread_end 0]) \/ + ev = join (st_evid + event_id_span (copland_compile t2)) (session_plc ac') + ). + { + apply in_app_or in H1. door. - ++ - invc H0; try eauto; try solve_by_inversion. - ++ - eauto. - - + invc H0; try eauto; try solve_by_inversion. - } - - door. - subst. + + + assert( + (([Term_Defs.split cvmi (session_plc ac'); + cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e] ++ blah) ++ + [cvm_thread_end 0]) = + ([Term_Defs.split cvmi (session_plc ac')] ++ + ([(cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e)] ++ blah ++ + [cvm_thread_end 0]))). + { + simpl. + tauto. + } + rewrite H1 in H0. - apply evtsbparsplit. - auto. - door. - Unset Printing Notations. + apply in_app_or in H0. + door. + ++ + invc H0; try eauto; try solve_by_inversion. + ++ + eauto. - assert ( - (cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e) = - (cvm_thread_start 0 (session_plc ac') (copland_compile t2)) mt). - { - eapply cvm_thread_start_clear. + + invc H0; try eauto; try solve_by_inversion. } - rewrite H3 in *; clear H1. - - assert ( - In ev (cvm_events_core (copland_compile t2) (session_plc ac') mt) \/ - In ev blah). - { - - eapply cvm_thread_in_ev; eassumption. - - - } - door. - - 2: { - - apply evtsbparl. - - simpl in *. - unfold mt_evc in *. - assert (S cvmi = cvmi + 1) by lia. - rewrite <- H4 in *. + door. + subst. - eapply IHt1. - eassumption. - eapply restl; eauto. + apply evtsbparsplit. + auto. + door. + Unset Printing Notations. - rewrite fufu in Heqp2; eauto. - eauto. + assert ( + (cvm_thread_start 0 (session_plc ac') (lseqc (aspc CLEAR) (copland_compile t2)) e) = + (cvm_thread_start 0 (session_plc ac') (copland_compile t2)) mt). + { + eapply cvm_thread_start_clear. + } + rewrite H4 in *. + assert ( + In ev (cvm_events_core (copland_compile t2) (session_plc ac') mt) \/ + In ev blah). + { + eapply cvm_thread_in_ev; eassumption. -(* - ff. - assert (( - (Term_Defs.split cvmi p :: (cvm_thread_start 0 p <{ (CLR -> (copland_compile t2)) }> e)) :: blah) = - [Term_Defs.split cvmi p :: (cvm_thread_start 0 p <{ CLR -> (copland_compile t2) }> e)] ++ blah). - eassumption. - (* - assert ((Term_Defs.split cvmi p :: cvm_thread_start 0 p <{ CLR -> (copland_compile t2) }> e :: blah) = - ([Term_Defs.split cvmi p :: cvm_thread_start 0 p <{ CLR -> (copland_compile t2) }> e] ++ blah)). - { - intuition. - } - *) - admit. - *) + } + door. - } + 2: { + apply evtsbparl. - apply evtsbparr. + simpl in *. + unfold mt_evc in *. + assert (S cvmi = cvmi + 1) by lia. + rewrite <- H6 in *. + eapply IHt1. + eassumption. + eapply restl; eauto. - pose (build_cvm_external (copland_compile t2) (evc bits mt) st_evid ac'). + rewrite fufu in *; eauto. + eauto. + } -assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits mt) = -evc b et). -{ - eapply cvm_evidence_exists_remote. -} -destruct_conjs. -rewrite H6 in *. + apply evtsbparr. + pose (build_cvm_external (copland_compile t2) (evc bits mt) st_evid ac'). - simpl. + assert (exists b et, cvm_evidence_core (copland_compile t2) (session_plc ac') (evc bits mt) = + evc b et). + { + eapply cvm_evidence_exists_remote. + } + destruct_conjs. + rewrite H8 in *. - eapply IHt2. - eassumption. - econstructor. - eassumption. - eauto. - eauto. + simpl. - subst. + eapply IHt2. + eassumption. - apply evtsbparjoin. - simpl. - lia. -(* TODO: We need to just fix the remote call one, I am not really sure how it should be working, it seems a bit odd the actual output statement? *) -Admitted. -(* Qed. *) + econstructor; ffa. + ffa. + ffa. +Qed. diff --git a/src/Cvm_Impl.v b/src/Cvm_Impl.v index d98b08d..c2f7b89 100644 --- a/src/Cvm_Impl.v +++ b/src/Cvm_Impl.v @@ -7,10 +7,8 @@ Author: Adam Petz, ampetz@ku.edu *) -Require Import Term_Defs Anno_Term_Defs Cvm_Monad. - -Require Import List. -Import ListNotations. +Require Import Term_Defs Cvm_Monad ErrorStMonad_Coq. +Import ErrNotation. (** Monadic CVM implementation (top-level) *) Fixpoint build_cvm (t:Core_Term) : CVM unit := diff --git a/src/Cvm_Monad.v b/src/Cvm_Monad.v index a7ae39e..6a5f249 100644 --- a/src/Cvm_Monad.v +++ b/src/Cvm_Monad.v @@ -5,9 +5,9 @@ Author: Adam Petz, ampetz@ku.edu *) -Require Import ResultT Term_Defs Term ConcreteEvidence Evidence_Bundlers Defs Axioms_Io StructTactics Maps Session_Config_Compiler. +Require Import ResultT Term Evidence_Bundlers Axioms_Io Maps Session_Config_Compiler. -Require Import Coq.Program.Tactics Lia. +Require Import Coq.Program.Tactics. Require Import Manifest_Admits ErrorStringConstants Attestation_Session. @@ -16,56 +16,58 @@ Import ListNotations. Require Export Cvm_St ErrorStMonad_Coq IO_Stubs Interface. +Import ErrNotation. + (** * CVM monadic primitive operations *) Definition get_ev : CVM EvC := - st <- get ;; - ret (st_ev st). + st <- err_get ;; + err_ret (st_ev st). Definition get_trace : CVM (list Ev) := - st <- get ;; - ret (st_trace st). + st <- err_get ;; + err_ret (st_trace st). Definition get_evid : CVM Event_ID := - st <- get ;; - ret (st_evid st). + st <- err_get ;; + err_ret (st_evid st). Definition get_config : CVM Session_Config := (* TODO: consider moving this functionality to a Reader-like monad i.e. an 'ask' primitive *) - st <- get ;; - ret (st_config st). + st <- err_get ;; + err_ret (st_config st). Definition put_ev (e' : EvC) : CVM unit := tr <- get_trace ;; i <- get_evid ;; sc <- get_config ;; - put (mk_st e' tr i sc). + err_put (mk_st e' tr i sc). Definition put_trace (tr' : list Ev) : CVM unit := e <- get_ev ;; i <- get_evid ;; sc <- get_config ;; - put (mk_st e tr' i sc). + err_put (mk_st e tr' i sc). Definition put_evid (i' : Event_ID) : CVM unit := e <- get_ev ;; tr <- get_trace ;; sc <- get_config ;; - put (mk_st e tr i' sc). + err_put (mk_st e tr i' sc). Definition get_pl : CVM Plc := sc <- get_config ;; - ret (session_plc sc). + err_ret (session_plc sc). Definition inc_id : CVM Event_ID := tr <- get_trace ;; e <- get_ev ;; i <- get_evid ;; sc <- get_config ;; - put (mk_st e tr (Nat.add i (S O)) sc) ;; - ret i. + err_put (mk_st e tr (Nat.add i (S O)) sc) ;; + err_ret i. Definition modify_evm (f:EvC -> EvC) : CVM unit := e <- get_ev ;; @@ -97,7 +99,7 @@ Definition split_ev : CVM unit := Definition tag_ASP (params :ASP_PARAMS) (mpl:Plc) (e:EvC) : CVM Event_ID := x <- inc_id ;; add_trace [umeas x mpl params (get_et e)] ;; - ret x. + err_ret x. (* Helper function that builds a new internal evidence bundle based on the evidence extension parameter of an ASP term. *) @@ -105,21 +107,21 @@ Definition fwd_asp (fwd:FWD) (rwev : RawEv) (e:EvC) (p:Plc) (ps:ASP_PARAMS): CVM match fwd with | COMP => match comp_bundle rwev e p ps with - | resultC e' => ret e' - | errC e => failm (dispatch_error (Runtime e)) + | resultC e' => err_ret e' + | errC e => err_failm (dispatch_error (Runtime e)) end | EXTD n => match extd_bundle rwev e p n ps with - | resultC e' => ret e' - | errC e => failm (dispatch_error (Runtime e)) + | resultC e' => err_ret e' + | errC e => err_failm (dispatch_error (Runtime e)) end | ENCR => match encr_bundle rwev e p ps with - | resultC e' => ret e' - | errC e => failm (dispatch_error (Runtime e)) + | resultC e' => err_ret e' + | errC e => err_failm (dispatch_error (Runtime e)) end - | KILL => ret mt_evc - | KEEP => ret e + | KILL => err_ret mt_evc + | KEEP => err_ret e end. (** * Stub for invoking external ASP procedures. @@ -128,8 +130,8 @@ Definition fwd_asp (fwd:FWD) (rwev : RawEv) (e:EvC) (p:Plc) (ps:ASP_PARAMS): CVM Definition do_asp (params :ASP_PARAMS) (e:RawEv) (x:Event_ID) : CVM RawEv := sc <- get_config ;; match (sc.(aspCb) params e) with - | resultC r => ret r - | errC e => failm (dispatch_error e) + | resultC r => err_ret r + | errC e => err_failm (dispatch_error e) end. (* Simulates invoking an arbitrary ASP. Tags the event, builds and returns @@ -140,7 +142,7 @@ Definition invoke_ASP (fwd:FWD) (params:ASP_PARAMS) (* (ac : AM_Config) *) : CVM x <- tag_ASP params p e ;; rawev <- do_asp params (get_bits e) x ;; outev <- fwd_asp fwd rawev e p params ;; - ret outev. + err_ret outev. Definition copyEv : CVM EvC := p <- get_pl ;; @@ -152,10 +154,10 @@ Definition nullEv : CVM EvC := p <- get_pl ;; x <- inc_id ;; add_trace [null x p] ;; - ret mt_evc. + err_ret mt_evc. Definition clearEv : unit -> CVM EvC := - fun _ => ret mt_evc. + fun _ => err_ret mt_evc. (* Helper that interprets primitive core terms in the CVM. *) Definition do_prim (a:ASP_Core) (* (ac : AM_Config) *) : CVM EvC := @@ -195,13 +197,16 @@ Definition tag_RPY (p:Plc) (q:Plc) (e:EvC) : CVM unit := Definition get_cvm_policy : CVM PolicyT := sc <- get_config ;; - ret (policy sc). + err_ret (policy sc). + +Definition policy_list_not_disclosed (t:Term) (p:Plc) (e:Evidence) (ls: list (Plc * ASP_ID)) : bool := (* true. *) + forallb (fun pr => negb (term_discloses_aspid_to_remote_enc_bool t p e (fst pr) (snd pr))) ls. Definition check_cvm_policy (t:Term) (pTo:Plc) (et:Evidence) : CVM unit := pol <- get_cvm_policy ;; match (policy_list_not_disclosed t pTo et pol) with - | true => ret tt - | false => failm (dispatch_error (Runtime errStr_disclosePolicy)) + | true => err_ret tt + | false => err_failm (dispatch_error (Runtime errStr_disclosePolicy)) end. Definition do_remote (t:Term) (pTo:Plc) (e:EvC) (sc : Session_Config) @@ -236,8 +241,8 @@ Definition doRemote_session' (t:Term) (pTo:Plc) (e:EvC) : CVM EvC := check_cvm_policy t pTo (get_et e) ;; sc <- get_config ;; match (do_remote t pTo e sc) with - | resultC ev => ret (evc ev (eval t pTo (get_et e))) - | errC e => failm (dispatch_error e) + | resultC ev => err_ret (evc ev (eval t pTo (get_et e))) + | errC e => err_failm (dispatch_error e) end. Definition remote_session (t:Term) (p:Plc) (q:Plc) (e:EvC) : CVM EvC := @@ -245,13 +250,13 @@ Definition remote_session (t:Term) (p:Plc) (q:Plc) (e:EvC) : CVM EvC := e' <- doRemote_session' t q e ;; add_trace (cvm_events t q (get_et e)) ;; inc_remote_event_ids t ;; - ret e'. + err_ret e'. Definition doRemote (t:Term) (q:Plc) (e:EvC) : CVM EvC := p <- get_pl ;; e' <- remote_session t p q e ;; tag_RPY p q e' ;; - ret e'. + err_ret e'. Definition join_seq (e1:EvC) (e2:EvC): CVM unit := p <- get_pl ;; @@ -272,12 +277,15 @@ Definition wait_par_thread (loc:Loc) (t:Core_Term) (e:EvC) : CVM EvC := e' <- do_wait_par_thread loc t p e ;; add_trace [cvm_thread_end loc] ;; inc_par_event_ids t ;; - ret e'. + err_ret e'. -Ltac monad_unfold := +Ltac cvm_monad_unfold := repeat unfold - execErr, do_prim, + doRemote, + remote_session, + doRemote_session', + check_cvm_policy, invoke_ASP, fwd_asp, extd_bundle, @@ -286,21 +294,15 @@ Ltac monad_unfold := do_asp, clearEv, copyEv, + nullEv, get_ev, get_pl, get_config, add_trace, modify_evm, - add_trace, - failm, - get, - when, - put, - nop, - modify, - bind, - ret in * ; + add_trace in * ; + repeat err_monad_unfold; simpl in * . (* Grouping together some common hypothesis normalizations. Inverting pairs of @@ -311,9 +313,9 @@ Ltac pairs := repeat match goal with | [H: (Some _, _) = - (Some _, _) |- _ ] => invc H; monad_unfold + (Some _, _) |- _ ] => invc H; cvm_monad_unfold | [H: {| st_ev := _; st_trace := _; st_evid := _; st_config := _ |} = {| st_ev := _; st_trace := _; st_evid := _; st_config := _ |} |- _ ] => - invc H; monad_unfold - end; destruct_conjs; monad_unfold. + invc H; cvm_monad_unfold + end; destruct_conjs; cvm_monad_unfold. diff --git a/src/Cvm_Run.v b/src/Cvm_Run.v index 952ed12..49320bd 100644 --- a/src/Cvm_Run.v +++ b/src/Cvm_Run.v @@ -1,6 +1,6 @@ (* Top-level definitions for running CVM monad computations. *) -Require Import Term_Defs Anno_Term_Defs Cvm_Impl Cvm_St ErrorStMonad_Coq String +Require Import Term_Defs Cvm_Impl Cvm_St ErrorStMonad_Coq String ErrorStringConstants Attestation_Session. Require Import List. diff --git a/src/Cvm_St.v b/src/Cvm_St.v index 2681317..dccd4f3 100644 --- a/src/Cvm_St.v +++ b/src/Cvm_St.v @@ -6,7 +6,7 @@ CVM Monad definition. Author: Adam Petz, ampetz@ku.edu *) -Require Import ConcreteEvidence ErrorStMonad_Coq ID_Type Attestation_Session. +Require Import ConcreteEvidence ErrorStMonad_Coq Attestation_Session. Require Import List. Import ListNotations. Require Import Manifest_Admits. diff --git a/src/Defs.v b/src/Defs.v index 70e8ce6..58fdf15 100644 --- a/src/Defs.v +++ b/src/Defs.v @@ -12,6 +12,7 @@ Import List.ListNotations. Require Import Coq.Program.Tactics. +Require Import Ltac2.Ltac2. (* rewrite (existentially) an arbitrary hypothesis and attempt eauto *) Ltac jkjke := @@ -46,22 +47,31 @@ Ltac door := destruct H end; destruct_conjs. -Lemma pairsinv : forall (a a' b b':nat), - a <> a' -> (a,b) <> (a',b'). -Proof. - intros. - congruence. -Defined. - - (* Simplification hammer. Used at beginning of many proofs in this development. Conservative simplification, break matches, invert on resulting goals *) Ltac ff := - repeat (cbn in *; - repeat break_match; - repeat find_inversion; - try solve_by_inversion). + repeat ( + (* try cbn in *; *) + try simpl in *; + try break_match; + repeat (find_rewrite; clean); + repeat find_injection; + simpl in *; subst; eauto; + try congruence; + try solve_by_inversion + ). + +Ltac ffa := + repeat (ff; + repeat find_apply_hyp_hyp; + ff). + +Tactic Notation "ffa" "using" tactic(tac) := + repeat (ff; + repeat find_apply_hyp_hyp; + tac; + ff). Ltac fail_if_in_hyps_type t := lazymatch goal with @@ -91,11 +101,6 @@ Ltac find_apply_hyp_hyp' := pose_new_proof (H H') end. -Ltac find_apply_lem_hyp lem := - match goal with - | [ H : _ |- _ ] => apply lem in H - end. - Ltac find_pose_new_lem_hyp lem := match goal with | [ H : _ |- _ ] => pose_new_proof (lem H) diff --git a/src/Disclose.v b/src/Disclose.v index 3ecce54..bb3ddb8 100644 --- a/src/Disclose.v +++ b/src/Disclose.v @@ -4,15 +4,11 @@ Experiments in stating "disclosure" properties of the CVM. Author: Adam Petz, ampetz@ku.edu *) -Require Import Term_Defs Anno_Term_Defs Term LTS Cvm_Impl Cvm_St Trace Main ConcreteEvidence Attestation_Session. +Require Import Term_Defs. -Require Import CvmSemantics Appraisal_Evidence Eqb_Evidence Auto ID_Type EqClass Helpers_CvmSemantics (* Disclose_Gen *) External_Facts Axioms_Io. +Require Import Anno_Term_Defs ConcreteEvidence Eqb_Evidence CvmSemantics Auto EqClass Main Attestation_Session Helpers_CvmSemantics Cvm_St ResultT. -Require Import StructTactics. - -Require Import ErrorStMonad_Coq. - -Require Import Coq.Program.Tactics PeanoNat Lia. +Require Import StructTactics Coq.Program.Tactics. Require Import List. Import ListNotations. @@ -111,7 +107,7 @@ Proof. repeat match goal with | H : _ /\ _ |- _ => destruct H | H : _ \/ _ |- _ => destruct H - | [ H : (_ =? _)%string = true |- _ ] => + | [ H : String.eqb _ _ = true |- _ ] => rewrite String.eqb_eq in *; subst end; eauto; try (econstructor; eauto; intros HC; congruence). @@ -269,51 +265,27 @@ Lemma term_disc_remote_enc : forall t p e i r p0, term_discloses_aspid_to_remote_enc t p e i r -> term_discloses_aspid_to_remote_enc <{ @ p [t] }> p0 e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - find_rewrite. - apply Bool.orb_true_r. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Lemma term_disc_lseq_l_enc : forall t1 t2 p e i r, term_discloses_aspid_to_remote_enc t1 p e i r -> term_discloses_aspid_to_remote_enc <{ t1 -> t2 }> p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - find_rewrite. - apply Bool.orb_true_l. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Lemma term_disc_lseq_r_enc : forall t1 t2 p e i r, term_discloses_aspid_to_remote_enc t2 p (eval t1 p e) i r -> term_discloses_aspid_to_remote_enc <{ t1 -> t2 }> p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - find_rewrite. - apply Bool.orb_true_r. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Close Scope cop_ent_scope. @@ -322,73 +294,27 @@ Lemma term_disc_bseq_l_enc : forall t1 t2 p e i r s, term_discloses_aspid_to_remote_enc t1 p (splitEv_T_l s e) i r -> term_discloses_aspid_to_remote_enc (bseq s t1 t2) p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - subst. - destruct s0; - destruct s1; - - simpl in *; - (* rewrite H0; *) - find_rewrite; - - rewrite Bool.orb_true_l; - auto. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Lemma term_disc_bseq_r_enc : forall t1 t2 p e i r s, term_discloses_aspid_to_remote_enc t2 p (splitEv_T_r s e) i r -> term_discloses_aspid_to_remote_enc (bseq s t1 t2) p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - subst. - destruct s0; - destruct s1; - - simpl in *; - find_rewrite; - - rewrite Bool.orb_true_r; - auto. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Lemma term_disc_bpar_l_enc : forall t1 t2 p e i r s, term_discloses_aspid_to_remote_enc t1 p (splitEv_T_l s e) i r -> term_discloses_aspid_to_remote_enc (bpar s t1 t2) p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - subst. - destruct s0; - destruct s1; - - simpl in *; - find_rewrite; - - rewrite Bool.orb_true_l; - auto. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. @@ -396,24 +322,9 @@ Lemma term_disc_bpar_r_enc : forall t1 t2 p e i r s, term_discloses_aspid_to_remote_enc t2 p (splitEv_T_r s e) i r -> term_discloses_aspid_to_remote_enc (bpar s t1 t2) p e i r. Proof. - intros. - invc H. - destruct_conjs. - econstructor. - split. - - - eassumption. - - - ff. - subst. - destruct s0; - destruct s1; - - simpl in *; - find_rewrite; - - rewrite Bool.orb_true_r; - auto. + intros; invc H; destruct_conjs; + econstructor; split; eauto; + ff; rewrite Bool.orb_true_iff; ff. Qed. Lemma term_discloses_respects_events : forall annt t p e r H2, @@ -423,26 +334,15 @@ Lemma term_discloses_respects_events : forall annt t p e r H2, Proof. intros. unfold not in * ; intros. - (* - unfold events_discloses_aspid in *. - (* - assert (exists annt cvmi, annoP_indexed annt t 0 cvmi). admit. - destruct_conjs. - specialize (H0 H1 H2 H3). *) - destruct_conjs. - subst. - *) - generalizeEverythingElse t. induction t; intros. - (* asp case *) - invc H. - destruct_conjs. - invc H0. - destruct_conjs. - door; - repeat ff. + invc H; + destruct_conjs; + invc H0; + destruct_conjs; + door; ff. - (* at case *) invc H0. destruct_conjs. @@ -454,7 +354,7 @@ Proof. invc H. destruct_conjs. - invc H5; try solve_by_inversion. + invc H6; try solve_by_inversion. ff. invc H0. ++ diff --git a/src/Eqb_Evidence.v b/src/Eqb_Evidence.v index db2dc41..c156ec0 100644 --- a/src/Eqb_Evidence.v +++ b/src/Eqb_Evidence.v @@ -228,7 +228,7 @@ Proof. eapply H; eauto. + eauto. -Defined. +Qed. Lemma eqb_eq_list {A:Type}: forall x y f, @@ -307,7 +307,7 @@ Proof. eapply H. reflexivity. eapply list_beq_refl; eauto. -Defined. +Qed. Definition eqb_fwd (fwd1 fwd2 : FWD) : bool := match fwd1, fwd2 with @@ -398,10 +398,10 @@ Proof. repeat rewrite Bool.andb_true_iff. split; eauto. -Defined. +Qed. *) -Lemma eqb_plc_refl : forall p0, Eqb_Evidence.eqb_plc p0 p0 = true. +Lemma eqb_plc_refl : forall p0, eqb_plc p0 p0 = true. Proof. intros; apply eqb_eq_plc; auto. Qed. \ No newline at end of file diff --git a/src/ErrorStMonad_Coq.v b/src/ErrorStMonad_Coq.v index a9b93f9..f6ac6ac 100644 --- a/src/ErrorStMonad_Coq.v +++ b/src/ErrorStMonad_Coq.v @@ -11,9 +11,9 @@ Export ResultT. (* Generalized Error + State Monad *) Definition Err(S A E: Type) : Type := S -> (ResultT A E) * S % type. -Definition ret {S A E : Type} (a : A) : Err S A E := fun s => (resultC a, s). +Definition err_ret {S A E : Type} (a : A) : Err S A E := fun s => (resultC a, s). -Definition bind {S A B E : Type} (m : Err S A E) (f : A -> Err S B E) : Err S B E := +Definition err_bind {S A B E : Type} (m : Err S A E) (f : A -> Err S B E) : Err S B E := fun s => let '(a, s') := m s in match a with @@ -23,50 +23,41 @@ Definition bind {S A B E : Type} (m : Err S A E) (f : A -> Err S B E) : Err S B | errC e => (errC e,s') end. -Definition failm {S A E : Type} (e:E) : Err S A E := fun s => (errC e, s). - +Definition err_failm {S A E : Type} (e:E) : Err S A E := fun s => (errC e, s). -(* alias for ret *) -(*Definition write_output {S O} (o : O) : GenHandler1 S O := ret o.*) +Definition err_modify {S E} (f : S -> S) : Err S unit E := fun s => (resultC tt, f s). -Definition modify {S E} (f : S -> S) : Err S unit E := fun s => (resultC tt, f s). +Definition err_put {S E} (s : S) : Err S unit E := fun _ => (resultC tt, s). -Definition put {S E} (s : S) : Err S unit E := fun _ => (resultC tt, s). - -Definition get {S E} : Err S S E := fun s => (resultC s, s). - -Definition runErr {S A E} (h : Err S A E) (s : S) : (ResultT A E) * S % type := - h s. - -Definition evalErr {S A E} (h : Err S A E) (s : S) : ResultT A E := - fst (runErr h s). - -Definition execErr {S A E} (h : Err S A E) (s : S) : S := - snd (h s). - -Definition nop {S E: Type} := @ret S _ E tt. +Definition err_get {S E} : Err S S E := fun s => (resultC s, s). Module ErrNotation. -Notation "a >> b" := (bind a (fun _ => b)) (at level 50). +Notation "a >> b" := (err_bind a (fun _ => b)) (at level 50). -Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2)) +Notation "x <- c1 ;; c2" := (@err_bind _ _ _ _ c1 (fun x => c2)) (at level 100, c1 at next level, right associativity). Notation "e1 ;; e2" := (_ <- e1 ;; e2) (at level 100, right associativity). Notation "' pat <- c1 ;; c2" := - (@bind _ _ c1 (fun x => match x with pat => c2 end)) + (@err_bind _ _ c1 (fun x => match x with pat => c2 end)) (at level 100, pat pattern, c1 at next level, right associativity). End ErrNotation. -Export ErrNotation. +Import ErrNotation. -Definition gets {S} {A} {E} (f:S -> A) : Err S A E := - st <- get ;; - ret (f st). +Definition err_gets {S} {A} {E} (f:S -> A) : Err S A E := + st <- err_get ;; + err_ret (f st). -Definition when {S A E} (b : bool) (m : Err S A E) : Err S unit E := - if b then m ;; ret tt else nop. +Ltac err_monad_unfold := + repeat unfold err_ret, + err_bind, + err_failm, + err_modify, + err_put, + err_get, + err_gets in *. \ No newline at end of file diff --git a/src/Evidence_Bundlers.v b/src/Evidence_Bundlers.v index 8e9eeae..4239546 100644 --- a/src/Evidence_Bundlers.v +++ b/src/Evidence_Bundlers.v @@ -6,7 +6,7 @@ Extracted code could be simplified to only the raw evidence operation. *) Require Import List String. -Require Import ConcreteEvidence IO_Stubs ResultT ErrorStringConstants EqClass. +Require Import ConcreteEvidence ResultT ErrorStringConstants EqClass. Import ListNotations. diff --git a/src/External_Facts.v b/src/External_Facts.v index 4bc1f3c..e99a17f 100644 --- a/src/External_Facts.v +++ b/src/External_Facts.v @@ -4,7 +4,7 @@ Axioms and derived lemmas that capture the semantics of external CVM instances. Author: Adam Petz, ampetz@ku.edu *) -Require Import Term_Defs Anno_Term_Defs Cvm_St Cvm_Impl Axioms_Io Helpers_CvmSemantics Cvm_Monad ID_Type Attestation_Session. +Require Import Term_Defs Anno_Term_Defs Cvm_Impl Axioms_Io Cvm_Monad Attestation_Session. Require Import List. Import ListNotations. @@ -12,18 +12,11 @@ Import ListNotations. (* TODO: This seems obscenely strong!? *) Axiom build_cvm_external' : forall (t : Core_Term) (e : EvC) (tr:list Ev) (i:Event_ID) (ac : Session_Config), - runErr - (build_cvm t) - {| st_ev := e; - st_trace := tr; - st_evid := i; - st_config := ac |} = - (resultC tt, - {| st_ev := cvm_evidence_core t (session_plc ac) e; - st_trace := tr ++ (cvm_events_core t (session_plc ac) (get_et e)); - st_evid := (i + event_id_span t); - st_config := ac - |}). + build_cvm t {| st_ev := e; st_trace := tr; st_evid := i; st_config := ac |} + = (resultC tt, {| st_ev := cvm_evidence_core t (session_plc ac) e; + st_trace := tr ++ (cvm_events_core t (session_plc ac) (get_et e)); + st_evid := (i + event_id_span t); + st_config := ac |}). Lemma build_cvm_external : forall (t : Core_Term) (e : EvC) i ac, build_cvm t @@ -39,6 +32,5 @@ Lemma build_cvm_external : forall (t : Core_Term) (e : EvC) i ac, |}). Proof. intros. - assert ([] ++ (cvm_events_core t (session_plc ac) (get_et e)) = (cvm_events_core t (session_plc ac) (get_et e))) by eauto. eapply build_cvm_external'. -Defined. +Qed. diff --git a/src/Extraction_Cvm_Cake.v b/src/Extraction_Cvm_Cake.v index 56963a5..d51988d 100644 --- a/src/Extraction_Cvm_Cake.v +++ b/src/Extraction_Cvm_Cake.v @@ -25,6 +25,7 @@ Extraction Implicit do_wait_par_thread [2 3 4]. Extract Constant sig_params => "( undefined () )". Extract Constant hsh_params => "( undefined () )". +Extract Inlined Constant Nat.eqb => "(op=)". (* Extract Constant + => "add". *) (* Extract Constant Nat.add => "(+)". *) diff --git a/src/Helpers_Appraisal.v b/src/Helpers_Appraisal.v index 7583490..9eddfe6 100644 --- a/src/Helpers_Appraisal.v +++ b/src/Helpers_Appraisal.v @@ -143,7 +143,7 @@ Proof. rewrite H3 in *. rewrite Heqo in *. solve_by_inversion. -Defined. +Qed. *) Lemma uuc_app: forall e' e'' params p n, @@ -159,7 +159,7 @@ Proof. generalizeEverythingElse e'. induction e'; intros; ff. -Defined. +Qed. (* @@ -314,7 +314,7 @@ Defined. eassumption. destruct_conjs. eauto. *) -Defined. +Qed. *) Lemma hhc_app: forall e' p bs et, @@ -328,7 +328,7 @@ Proof. ff; try evSubFacts; eauto. -Defined. +Qed. Ltac find_wfec := repeat @@ -394,7 +394,7 @@ Proof. unfold not_none_none in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_none_abseq_pieces: forall s t1 t2, not_none_none (bseq s t1 t2) -> @@ -403,7 +403,7 @@ Proof. unfold not_none_none in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_none_abpar_pieces: forall s t1 t2, not_none_none (bpar s t1 t2) -> @@ -412,7 +412,7 @@ Proof. unfold not_none_none in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_none_aatt_pieces: forall q t1, not_none_none (att q t1) -> @@ -422,7 +422,7 @@ Proof. unfold not_none_none in *; unfold not in *. eauto. -Defined. +Qed. Lemma not_hshsig_alseq_pieces: forall t1 t2, not_hash_sig_term (lseq t1 t2) -> @@ -432,7 +432,7 @@ Proof. unfold not_hash_sig_term in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_hshsig_abseq_pieces: forall s t1 t2, not_hash_sig_term (bseq s t1 t2) -> @@ -442,7 +442,7 @@ Proof. unfold not_hash_sig_term in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_hshsig_abpar_pieces: forall s t1 t2, not_hash_sig_term (bpar s t1 t2) -> @@ -452,7 +452,7 @@ Proof. unfold not_hash_sig_term in *; unfold not in *. split; eauto. -Defined. +Qed. Lemma not_hshsig_aatt_pieces: forall q t1, not_hash_sig_term (att q t1) -> @@ -462,7 +462,7 @@ Proof. unfold not_hash_sig_term in *; unfold not in *. eauto. -Defined. +Qed. Ltac do_not_none_alseq_pieces := match goal with @@ -574,7 +574,7 @@ Proof. left. repeat eexists. eauto. -Defined. +Qed. Lemma not_none_none_contra_bpar: forall t1 t2 (P:Prop), not_none_none (bpar (NONE, NONE) t1 t2) -> @@ -587,7 +587,7 @@ Proof. right. repeat eexists. eauto. -Defined. +Qed. Ltac do_none_none_contra_bseq := match goal with @@ -622,7 +622,7 @@ Proof. try eauto; (* aatt, alseq cases *) try (destruct s; destruct s; destruct s0; ff; do_none_none_contra). (* abseq, abpar cases *) -Defined. +Qed. Lemma evsubt_preserved: forall t pt e e' et et' tr tr' p p' ett i i', not_none_none t -> @@ -643,7 +643,7 @@ Proof. subst. eapply evsubt_preserved_eval; eauto. -Defined. +Qed. Lemma not_ev: forall t e, not_hash_sig_term_ev t e -> @@ -652,7 +652,7 @@ Proof. intros; cbv in *. destruct_conjs. eauto. -Defined. +Qed. Lemma etfun_exists: forall y, exists y', y = et_fun y'. @@ -685,7 +685,7 @@ Proof. destruct_conjs. exists (ppc IHy1 IHy2). ff. -Defined. +Qed. Lemma not_hshsig_uuc: forall e' params p x, not_hash_sig_ev e' -> @@ -695,7 +695,7 @@ Proof. evSubFacts; try (destruct_conjs; solve_by_inversion); eauto. -Defined. +Qed. Lemma not_hshsig_ggc: forall e' n bs, not_hash_sig_ev e' -> @@ -705,7 +705,7 @@ Proof. evSubFacts; try (destruct_conjs; solve_by_inversion); eauto. -Defined. +Qed. Lemma gg_recons: forall e ecc x y, reconstruct_evP ecc e -> @@ -759,7 +759,7 @@ Proof. do_ggsub. repeat eexists. eauto. -Defined. +Qed. Lemma recon_evdenote_decomp: forall a p e, exists ecc, @@ -799,7 +799,7 @@ Proof. eexists. econstructor. eapply recon_same. -Defined. +Qed. Lemma recon_evP_ssc_decomp: forall ecc' a p e e' a0, reconstruct_evP ecc' @@ -813,8 +813,8 @@ Proof. do_inv_recon_ss. invc H. repeat ff. - unfold OptMonad_Coq.bind in *. - unfold OptMonad_Coq.ret in *. + unfold opt_bind in *. + unfold opt_ret in *. repeat ff. rewrite fold_recev in *. split. @@ -826,7 +826,7 @@ Proof. econstructor. symmetry. eassumption. -Defined. +Qed. Lemma recon_evP_ppc_decomp: forall ecc' a p e e' a0, reconstruct_evP ecc' @@ -840,8 +840,8 @@ Proof. do_inv_recon_pp. invc H. repeat ff. - unfold OptMonad_Coq.bind in *. - unfold OptMonad_Coq.ret in *. + unfold opt_bind in *. + unfold opt_ret in *. repeat ff. rewrite fold_recev in *. split. @@ -853,7 +853,7 @@ Proof. econstructor. symmetry. eassumption. -Defined. +Qed. Ltac do_evsub_ih'' := match goal with @@ -1007,7 +1007,7 @@ Proof. repeat eexists; eauto. + do_none_none_contra. -Defined. +Qed. Ltac do_evaccum e' := repeat @@ -1232,7 +1232,7 @@ Proof. eauto. right. eauto. -Defined. +Qed. Ltac do_sig_is He := repeat @@ -1381,7 +1381,7 @@ Proof. eassumption. subst. eauto. -Defined. +Qed. Ltac do_nhst_lseqr := match goal with @@ -1501,7 +1501,7 @@ Proof. do_ggsub. repeat eexists. eauto. -Defined. +Qed. Lemma hshsig_ev_term_contra: forall t annt p e e', @@ -2196,7 +2196,7 @@ Proof. ++ exfalso. eapply not_none_none_contra_bpar; eauto. -Defined. +Qed. Lemma uu_preserved: forall t1 t2 annt p n p0 e e''' e' params et, @@ -2271,7 +2271,7 @@ Proof. right; repeat (eexists; eauto). jkjke'. -Defined. +Qed. Ltac do_ste := try do_nhste_att; @@ -2306,7 +2306,7 @@ Proof. eapply sig_term_ev_bseql. eassumption. destruct s; destruct s; destruct s0; ff. -Defined. +Qed. Ltac do_nhse_bseql_nosplit := match goal with @@ -2334,7 +2334,7 @@ Proof. eapply sig_term_ev_bseqr. eassumption. destruct s; destruct s; destruct s0; ff. -Defined. +Qed. Ltac do_nhse_bseqr_nosplit := match goal with @@ -2364,7 +2364,7 @@ Proof. eapply sig_term_ev_bparl. eassumption. destruct s; destruct s; destruct s0; ff. -Defined. +Qed. Ltac do_nhse_bparl_nosplit := match goal with @@ -2392,7 +2392,7 @@ Proof. eapply sig_term_ev_bparr. eassumption. destruct s; destruct s; destruct s0; ff. -Defined. +Qed. Ltac do_nhse_bparr_nosplit := match goal with diff --git a/src/Helpers_CvmSemantics.v b/src/Helpers_CvmSemantics.v index 42d6143..376760b 100644 --- a/src/Helpers_CvmSemantics.v +++ b/src/Helpers_CvmSemantics.v @@ -4,70 +4,17 @@ Helper lemmas for proofs about the CVM semantics. Author: Adam Petz, ampetz@ku.edu *) -Require Import Anno_Term_Defs Cvm_Monad Cvm_Impl Term_Defs Auto StructTactics AutoApp Attestation_Session ResultT. +Require Import Anno_Term_Defs Cvm_Monad Cvm_Impl Term_Defs Auto Attestation_Session StructTactics AutoApp. +Require Import Coq.Program.Tactics. -Require Import Coq.Program.Tactics Coq.Program.Equality. - -Require Import List. Import ListNotations. -Lemma sc_immut : forall t e tr i ac, - st_config - (execErr - (build_cvm t) - {| - st_ev := e; - st_trace := tr; - st_evid := i; - st_config := ac - |}) = ac. -Proof. - induction t; repeat (monad_unfold; simpl in *); intuition. - - destruct a; monad_unfold; eauto; - destruct (aspCb ac a (get_bits e)) eqn:E1; simpl in *; eauto. - repeat ff. - - - (* at case *) - repeat ff; - unfold doRemote_session' in *; - repeat ff. - - - pose proof (IHt1 e tr i ac). - destruct (build_cvm t1 {| st_ev := e; st_trace := tr; st_evid := i; st_config := ac |}) eqn:C1; - simpl in *; eauto; - destruct r; simpl in *; intuition; eauto. - destruct c; simpl in *. - pose proof (IHt2 st_ev st_trace st_evid st_config). - destruct (build_cvm t2 {| st_ev := st_ev; st_trace := st_trace; st_evid := st_evid; st_config := st_config |}) eqn:C2; - simpl in *; subst; eauto. - - - monad_unfold; simpl in *. - pose proof (IHt1 e (tr ++ [Term_Defs.split i (session_plc ac)]) (i + 1) ac). - destruct (build_cvm t1 {| st_ev := e; st_trace := tr ++ [Term_Defs.split i (session_plc ac) ]; st_evid := (i + 1); st_config := ac |}) eqn:C1; - simpl in *; eauto; - destruct r; simpl in *; intuition; eauto. - destruct c; simpl in *. - pose proof (IHt2 e st_trace st_evid st_config). - destruct (build_cvm t2 {| st_ev := e; st_trace := st_trace; st_evid := st_evid; st_config := st_config |}) eqn:C2; - simpl in *; subst; eauto; - destruct r; simpl in *; eauto. - - monad_unfold; simpl in *. - pose proof (IHt1 e ((tr ++ [Term_Defs.split i (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]) (i + 1) ac). - destruct (build_cvm t1 {| st_ev := e; st_trace := (tr ++ [Term_Defs.split i (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]; st_evid := (i + 1); st_config := ac |}) eqn:C1; - simpl in *; eauto; - destruct r; simpl in *; intuition; eauto. -Qed. - Lemma sc_immut_better : forall t st r st', build_cvm t st = (r, st') -> st_config st = st_config st'. Proof. - intuition. - pose proof (sc_immut t (st_ev st) (st_trace st) (st_evid st) (st_config st)). - unfold execErr in *. - simpl in *. - destruct st; simpl in *. - find_rewrite; simpl in *; eauto. + induction t; repeat (cvm_monad_unfold; simpl in *); intuition; + ffa using cvm_monad_unfold. Qed. (* Hack to apply a specific induction hypothesis in some proofs *) @@ -83,19 +30,16 @@ Ltac anhl := end. Ltac monad_simp := - repeat (monad_unfold; simpl in *; eauto). + repeat (cvm_monad_unfold; simpl in *; eauto). Lemma check_cvm_policy_preserves_state : forall t p evt st1 st1' r, check_cvm_policy t p evt st1 = (r, st1') -> st1 = st1'. Proof. - induction t; simpl in *; intuition; eauto; ff; - break_match; repeat find_injection; eauto. + induction t; simpl in *; intuition; eauto; ffa using cvm_monad_unfold. Qed. Global Hint Resolve check_cvm_policy_preserves_state : core. -Require Import EqClass. - (* Lemma policy_list_not_disclosed_same_outputs : forall a p evt pol1 pol2 r1 r2, policy_list_not_disclosed a p evt pol1 = r1 -> policy_list_not_disclosed a p evt pol2 = r2 -> @@ -131,10 +75,7 @@ Lemma check_cvm_policy_same_outputs : forall t p evt st1 st1' r1 st2 st2' r2, (policy (st_config st1) = policy (st_config st2)) -> r1 = r2 /\ st1 = st1' /\ st2 = st2'. Proof. - induction t; simpl in *; intuition; eauto; - unfold check_cvm_policy in *; monad_simp; eauto; - repeat (break_match; repeat find_rewrite; repeat find_injection; - simpl in *; eauto). + induction t; simpl in *; intuition; eauto; ffa using cvm_monad_unfold. Qed. Global Hint Resolve check_cvm_policy_same_outputs : core. @@ -143,56 +84,19 @@ Theorem evidence_deterministic_output_on_results : forall t e tr1 tr2 i1 i2 ac s build_cvm t {| st_ev := e; st_trace := tr2; st_evid := i2; st_config := ac |} = (resultC tt, st2) -> st1.(st_ev) = st2.(st_ev). Proof. - induction t; intros; monad_simp. - - destruct a; monad_simp; invc H; invc H0; eauto; - destruct (aspCb ac a (get_bits e)); - simpl in *; invc H1; invc H2; eauto. - repeat ff. - - ff; - unfold doRemote_session' in *; - repeat (break_match; try monad_unfold; repeat find_rewrite; repeat find_injection; try congruence; eauto); - repeat find_eapply_lem_hyp check_cvm_policy_preserves_state; - subst; simpl in *; repeat find_rewrite; repeat find_injection; eauto. - - destruct (build_cvm t1 {| st_ev := e; st_trace := tr1; st_evid := i1; st_config := ac |}) eqn:E1; - destruct (build_cvm t1 {| st_ev := e; st_trace := tr2; st_evid := i2; st_config := ac |}) eqn:E2; - destruct r, r0; invc H; invc H0; destruct u, u0, c, c0. - pose proof (IHt1 _ _ _ _ _ _ _ _ E1 E2); simpl in *; subst. - assert (st_config = st_config0). { - pose proof (sc_immut t1 e tr2 i2 ac); monad_unfold; - pose proof (sc_immut t1 e tr1 i1 ac); monad_unfold. - rewrite E1, E2 in *; simpl in *; subst; eauto. - } - subst; clear E1 E2. - destruct (build_cvm t2 {| st_ev := st_ev0; st_trace := st_trace; st_evid := st_evid; st_config := st_config0 |}) eqn:E1; - destruct (build_cvm t2 {| st_ev := st_ev0; st_trace := st_trace0; st_evid := st_evid0; st_config := st_config0 |}) eqn:E2; - invc H1; invc H2; simpl in *; eauto. - - destruct (build_cvm t1 {| st_ev := e; st_trace := tr1 ++ [Term_Defs.split i1 (session_plc ac)]; st_evid := i1 + 1; st_config := ac |}) eqn:E1; - destruct (build_cvm t1 {| st_ev := e; st_trace := tr2 ++ [Term_Defs.split i2 (session_plc ac)]; st_evid := i2 + 1; st_config := ac |}) eqn:E2; - destruct r, r0; invc H; invc H0; destruct u, u0, c, c0. - pose proof (IHt1 _ _ _ _ _ _ _ _ E1 E2); simpl in *; subst. - assert (st_config = st_config0). { - pose proof (sc_immut t1 e (tr2 ++ [Term_Defs.split i2 (session_plc ac)]) (i2 + 1) ac); monad_unfold; - pose proof (sc_immut t1 e (tr1 ++ [Term_Defs.split i1 (session_plc ac)]) (i1 + 1) ac); monad_unfold; - rewrite E1, E2 in *; simpl in *; subst; eauto. - } - subst; clear E1 E2. - destruct (build_cvm t2 {| st_ev := e; st_trace := st_trace; st_evid := st_evid; st_config := st_config0 |}) eqn:E1; - destruct (build_cvm t2 {| st_ev := e; st_trace := st_trace0; st_evid := st_evid0; st_config := st_config0 |}) eqn:E2; - destruct r0, r; - invc H1; invc H2; simpl in *; - destruct u, u0. - pose proof (IHt2 _ _ _ _ _ _ _ _ E1 E2); simpl in *; subst; - rewrite H; eauto. - - destruct (build_cvm t1 {| st_ev := e; st_trace := (tr1 ++ [Term_Defs.split i1 (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]; st_evid := i1 + 1; st_config := ac |}) eqn:E1; - destruct (build_cvm t1 {| st_ev := e; st_trace := (tr2 ++ [Term_Defs.split i2 (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]; st_evid := i2 + 1; st_config := ac |}) eqn:E2; - destruct r, r0; invc H; invc H0; destruct u, u0, c, c0. - pose proof (IHt1 _ _ _ _ _ _ _ _ E1 E2); simpl in *; subst. - assert (st_config = st_config0). { - pose proof (sc_immut t1 e ((tr1 ++ [Term_Defs.split i1 (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]) (i1 + 1) ac); monad_unfold; - pose proof (sc_immut t1 e ((tr2 ++ [Term_Defs.split i2 (session_plc ac)]) ++ [cvm_thread_start l (session_plc ac) t2 (get_et e)]) (i2 + 1) ac); monad_unfold. - rewrite E1, E2 in *; simpl in *; subst; eauto. - } - subst; clear E1 E2; eauto. + induction t; intros; monad_simp; ffa using cvm_monad_unfold; + repeat match goal with + | u : unit |- _ => destruct u + | st : cvm_st |- _ => destruct st + | H1 : build_cvm ?t ?st1 = (?res1, ?st1'), + H2 : build_cvm ?t ?st2 = (?res2, ?st2'), + IH : context[build_cvm ?t _ = _ -> _] |- _ => + assert (Cvm_St.st_config st1 = Cvm_St.st_config st1') by ( + eapply sc_immut_better in H1; ffa); + assert (Cvm_St.st_config st2 = Cvm_St.st_config st2') by ( + eapply sc_immut_better in H2; ffa); + eapply IH in H1; [ | eapply H2]; ffa + end. Qed. Lemma cvm_errors_deterministic : forall t e tr1 tr2 i ac r1 r2 st1 st2, @@ -218,23 +122,8 @@ Lemma cvm_errors_deterministic : forall t e tr1 tr2 i ac r1 r2 st1 st2, st1.(st_evid) = st2.(st_evid)). Proof. induction t; intros; monad_simp. - - destruct a; monad_simp; invc H; invc H0; - simpl in *; intuition; - try (rewrite H; eauto); - try (invc H; eauto); - destruct (aspCb ac a (get_bits e)); - monad_simp; invc H1; invc H2; eauto; simpl in *; - try (rewrite H3; eauto); - repeat ff. - - ff; unfold doRemote_session' in *; - repeat (break_match; try monad_unfold; repeat find_rewrite; repeat find_injection; try congruence; eauto); - match goal with - | H1 : check_cvm_policy _ _ _ _ = _, - H2 : check_cvm_policy _ _ _ _ = _ |- _ => - eapply check_cvm_policy_same_outputs in H1; try eapply H2; eauto; - intuition; subst; simpl in *; subst; repeat find_rewrite; - repeat find_injection; eauto; try congruence - end. + - ffa. + - ffa using cvm_monad_unfold. - ff; eauto; repeat match goal with @@ -273,7 +162,7 @@ Lemma st_trace_irrel : forall t e e' e'' x x' y y' i i' i'' ac ac' ac'' res, Proof. intros; find_eapply_lem_hyp cvm_errors_deterministic; [ | eapply H]; intuition; simpl in *; eauto. -Defined. +Qed. Ltac dohi'' := @@ -292,111 +181,6 @@ Ltac dohi := do 2 (repeat dohi''; destruct_conjs; subst); repeat clear_triv. -(* States that the resulting evidence (st_ev) is unaffected by the initial trace. - This is a simple corollary of the Lemma hihi above. *) -Lemma trace_irrel_ev : forall t tr1 tr1' tr2 e e' i i' ac ac' res, - build_cvm t - {| st_ev := e; st_trace := tr1; st_evid := i; st_config := ac |} = - (res, {| st_ev := e'; st_trace := tr1'; st_evid := i'; st_config := ac' |}) -> - - st_ev - (execErr (build_cvm t) - {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) = e'. -Proof. - -intros. -destruct (build_cvm t {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) eqn:ff. -simpl. -vmsts. -simpl. -subst. -dohi. -df. -edestruct st_trace_irrel. -apply H. - -assert (r = res). -{ - eapply cvm_errors_deterministic. - apply Heqp. - apply H. -} -subst. - -apply Heqp. -intuition. -Defined. - -(* States that the resulting event id counter (st_evid) is unaffected by the initial trace. - This is a simple corollary of the Lemma hihi above. *) -Lemma trace_irrel_evid : forall t tr1 tr1' tr2 e e' i i' ac ac' res, - build_cvm t - {| st_ev := e; st_trace := tr1; st_evid := i; st_config := ac|} = - (res, {| st_ev := e'; st_trace := tr1'; st_evid := i'; st_config := ac' |}) -> - - st_evid - (execErr (build_cvm t) - {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) = i'. -Proof. - -intros. -destruct (build_cvm t {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) eqn:ff. -simpl. -vmsts. -simpl. -subst. -dohi. -df. -edestruct st_trace_irrel. -apply H. - -assert (r = res). -{ - eapply cvm_errors_deterministic. - apply Heqp. - apply H. -} -subst. - -apply Heqp. -intuition. -Defined. - - -(* States that the resulting evidence (st_ev) is unaffected by the initial trace. - This is a simple corollary of the Lemma hihi above. *) -Lemma trace_irrel_ac : forall t tr1 tr1' tr2 e e' i i' ac ac' res, - build_cvm t - {| st_ev := e; st_trace := tr1; st_evid := i; st_config := ac |} = - (res, {| st_ev := e'; st_trace := tr1'; st_evid := i'; st_config := ac' |}) -> - - st_config - (execErr (build_cvm t) - {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) = ac'. -Proof. - intros. - destruct (build_cvm t {| st_ev := e; st_trace := tr2; st_evid := i; st_config := ac |}) eqn:ff. - simpl. - vmsts. - simpl. - subst. - dohi. - df. - edestruct st_trace_irrel. - apply H. - - assert (r = res). - { - eapply cvm_errors_deterministic. - apply Heqp. - apply H. - } - subst. - - apply Heqp. - intuition. -Defined. - Ltac do_st_trace := match goal with | [H': context[{| st_ev := ?e; st_trace := ?tr; st_evid := ?i; st_config := ?ac |}] @@ -434,7 +218,7 @@ Lemma ccp_implies_cc: forall t st st' res, Proof. intros. solve_by_inversion. -Defined. +Qed. Lemma cc_implies_ccp: forall t st st' res, build_cvm t st = (res,st') -> @@ -443,7 +227,7 @@ Proof. intros. econstructor. tauto. -Defined. +Qed. Lemma ccp_iff_cc: forall t st st' res, build_cvm t st = (res,st') <-> @@ -453,7 +237,7 @@ Proof. split; intros; try (eapply cc_implies_ccp; eauto); try (eapply ccp_implies_cc; eauto). -Defined. +Qed. Ltac inv_term_coreP := match goal with @@ -469,7 +253,7 @@ Proof. intros. econstructor. eauto. -Defined. +Qed. Ltac do_term_to_core_redo := match goal with @@ -478,8 +262,6 @@ Ltac do_term_to_core_redo := eapply term_to_coreP_redo in H end. - - Lemma annoP_redo: forall t annt n n', anno t n = (n', annt) -> annoP annt t. @@ -488,7 +270,7 @@ Proof. econstructor. eexists. jkjke. -Defined. +Qed. Ltac do_anno_redo := match goal with @@ -512,7 +294,7 @@ Proof. intros. econstructor. jkjke. -Defined. +Qed. Ltac do_anno_indexed_redo := match goal with @@ -556,15 +338,10 @@ Ltac wrap_ccp_anno := try wrap_annopar; try wrap_anno; try wrap_anno_indexed; - try (unfold OptMonad_Coq.ret in * ); - try (unfold OptMonad_Coq.bind in * ); - try (unfold ErrorStMonad_Coq.bind in * ); - try (unfold ErrorStMonad_Coq.ret in * ); + cvm_monad_unfold; dd; try rewrite ccp_iff_cc in *. - - Ltac cumul_ih := match goal with | [H: context[(st_trace _ = _ ++ st_trace _)], diff --git a/src/IO_Stubs.v b/src/IO_Stubs.v index 01114a4..39c6e48 100644 --- a/src/IO_Stubs.v +++ b/src/IO_Stubs.v @@ -10,7 +10,7 @@ and evidence value results support specification of correctness properties for Appraisal. *) -Require Import Term_Defs ConcreteEvidence ErrorStMonad_Coq +Require Import Term_Defs ErrorStMonad_Coq Manifest_Admits Cvm_St String JSON. Require Import List. @@ -26,10 +26,10 @@ Definition make_JSON_FS_Location_Request (dir : FS_Location) (aspid : FS_Locatio Definition parallel_vm_thread (l:Loc) (t:Core_Term) (p:Plc) (e:EvC) : EvC. Admitted. Definition do_start_par_thread (loc:Loc) (t:Core_Term) (e:RawEv) : CVM unit := - ret tt. + err_ret tt. Definition do_wait_par_thread (loc:Loc) (t:Core_Term) (p:Plc) (e:EvC) : CVM EvC := - ret (parallel_vm_thread loc t p e). + err_ret (parallel_vm_thread loc t p e). Definition requester_bound (t:Term) (fromPl:Plc) (authTok:ReqAuthTok) : bool. Admitted. diff --git a/src/Impl_appraisal.v b/src/Impl_appraisal.v index 3781df4..a547853 100644 --- a/src/Impl_appraisal.v +++ b/src/Impl_appraisal.v @@ -6,26 +6,26 @@ Require Import ConcreteEvidence ErrorStMonad_Coq. Require Import ErrorStringConstants Appraisal_Defs AM_St. Require Import List. -Import ListNotations. +Import ListNotations ErrNotation. Definition peel_bs_am (ls:RawEv) : AM (BS * RawEv) := match ls with - | bs :: ls' => ret (bs, ls') + | bs :: ls' => err_ret (bs, ls') | _ => am_failm (am_error errStr_peel_bs_am) end. Fixpoint peel_n_am (n : nat) (ls : RawEv) : AM (RawEv * RawEv) := match n with - | 0 => ret ([], ls) + | 0 => err_ret ([], ls) | S n' => match ls with | [] => am_failm (am_error errStr_peel_n_am) | x :: ls' => v <- peel_n_am n' ls' ;; match v with - | (ls1, ls2) => ret (x :: ls1, ls2) + | (ls1, ls2) => err_ret (x :: ls1, ls2) end end end. @@ -33,25 +33,25 @@ Fixpoint peel_n_am (n : nat) (ls : RawEv) : AM (RawEv * RawEv) := Fixpoint gen_appraise_AM (et:Evidence) (ls:RawEv) : AM AppResultC := match et with - | mt => ret mtc_app + | mt => err_ret mtc_app | nn nid => v <- (peel_bs_am ls) ;; match v with (bs, _) => res <- checkNonce' nid bs ;; - ret (nnc_app nid res) + err_ret (nnc_app nid res) end | uu p fwd params et' => match fwd with - | COMP => ret mtc_app (* TODO hash check *) + | COMP => err_ret mtc_app (* TODO hash check *) | ENCR => v <- peel_bs_am ls ;; match v with (bs, ls') => decrypted_ls <- decrypt_bs_to_rawev' bs params et' ;; rest <- gen_appraise_AM et' decrypted_ls ;; - ret (eec_app p params passed_bs rest) + err_ret (eec_app p params passed_bs rest) (* TODO: consider encoding success/failure of decryption for bs param (instead of default_bs) *) end @@ -62,13 +62,13 @@ Fixpoint gen_appraise_AM (et:Evidence) (ls:RawEv) : AM AppResultC := (rawEv, ls') => v <- check_asp_EXTD' params p rawEv ls' ;; rest <- gen_appraise_AM et' ls' ;; - ret (ggc_app p params v rest) + err_ret (ggc_app p params v rest) end - | KILL => ret mtc_app (* Do we ever reach this case? *) + | KILL => err_ret mtc_app (* Do we ever reach this case? *) | KEEP => gen_appraise_AM et' ls (* Do we ever reach this case? *) end | ss et1 et2 => x <- gen_appraise_AM et1 (firstn (et_size et1) ls) ;; y <- gen_appraise_AM et2 (skipn (et_size et1) ls) ;; - ret (ssc_app x y) + err_ret (ssc_app x y) end. diff --git a/src/Interface_JSON.v b/src/Interface_JSON.v index d9eeafa..eb5bd39 100644 --- a/src/Interface_JSON.v +++ b/src/Interface_JSON.v @@ -1,4 +1,4 @@ -Require Import Interface_Types StructTactics Stringifiable Attestation_Session Term_Defs EqClass. +Require Import Interface_Types Stringifiable Attestation_Session Term_Defs. Require Export JSON List. Import ListNotations ResultNotation. diff --git a/src/Interface_Types.v b/src/Interface_Types.v index e967fe7..2692589 100644 --- a/src/Interface_Types.v +++ b/src/Interface_Types.v @@ -1,4 +1,4 @@ -Require Import JSON Term_Defs String Attestation_Session. +Require Import JSON Term_Defs Attestation_Session. Require Export Interface_Strings_Vars. diff --git a/src/LTS.v b/src/LTS.v index af8fb9c..90b4d56 100644 --- a/src/LTS.v +++ b/src/LTS.v @@ -14,7 +14,7 @@ University of California. See license.txt for details. *) Require Import List. Import List.ListNotations. Open Scope list_scope. -Require Import PeanoNat Lia Preamble Term_Defs Term. +Require Import PeanoNat Lia Preamble Term. (** * States *) @@ -321,7 +321,7 @@ Proof. induction H; auto. eapply lstar_tran; eauto. eapply lstar_silent_tran; eauto. -Defined. +Qed. Lemma lstar_stbsl: @@ -333,7 +333,7 @@ Proof. induction H; auto. eapply lstar_tran; eauto. eapply lstar_silent_tran; eauto. -Defined. +Qed. Lemma lstar_stbsr: forall st0 st1 j e tr, @@ -344,7 +344,7 @@ Proof. induction H; auto. eapply lstar_tran; eauto. eapply lstar_silent_tran; eauto. -Defined. +Qed. Lemma lstar_stbparl: forall st0 st1 st2 j tr, @@ -355,7 +355,7 @@ Proof. induction H; auto. eapply lstar_tran; eauto. eapply lstar_silent_tran; eauto. -Defined. +Qed. Lemma lstar_stbparr: forall st0 st1 st2 j tr, @@ -366,7 +366,7 @@ Proof. induction H; auto. eapply lstar_tran; eauto. eapply lstar_silent_tran; eauto. -Defined. +Qed. Lemma star_stbp: forall st0 st1 st2 st3 j, diff --git a/src/Main.v b/src/Main.v index 87c84ae..c665aaf 100644 --- a/src/Main.v +++ b/src/Main.v @@ -14,9 +14,7 @@ modify it under the terms of the BSD License as published by the University of California. See license.txt for details. *) -Require Import Preamble More_lists Term_Defs Term LTS Event_system Term_system Trace Defs. - -Require Import StructTactics. +Require Export Preamble More_lists Term LTS Event_system Term_system Trace Defs. Require Import List. Import List.ListNotations. @@ -87,7 +85,7 @@ Proof. try find_apply_lem_hyp shuffle_length; repeat find_apply_hyp_hyp; lia). -Defined. +Qed. Ltac inv_traceS := match goal with @@ -106,7 +104,7 @@ Proof. repeat find_apply_hyp_hyp; repeat find_apply_lem_hyp shuffle_length; try lia. -Defined. +Qed. Lemma step_silent_tr: forall st st' tr, diff --git a/src/ManCompSoundness.v b/src/ManCompSoundness.v index ea4b3c1..3e343b0 100644 --- a/src/ManCompSoundness.v +++ b/src/ManCompSoundness.v @@ -2,15 +2,13 @@ Namely, that the compiler outputs a collection of manifests that support execution of the input protocols. *) -Require Import Manifest Manifest_Generator ID_Type - Maps Term_Defs List Cvm_St Cvm_Impl ErrorStMonad_Coq StructTactics - Cvm_Monad EqClass Manifest_Admits Auto. -Require Import Manifest_Generator_Facts Eqb_Evidence Attestation_Session. +Require Import Manifest Manifest_Generator + Maps Term_Defs Cvm_Impl + Cvm_Monad Defs AM_Manager EqClass. +Require Import Manifest_Generator_Facts Attestation_Session. -Require Import Manifest_Generator_Helpers Session_Config_Compiler. -Require Import Helpers_CvmSemantics. - -Require Import Coq.Program.Tactics. +Require Import Manifest_Generator_Helpers Session_Config_Compiler ManCompSoundness_Helpers Manifest_Generator_Union. +Require Import Helpers_CvmSemantics Coq.Program.Tactics StructTactics. Import ListNotations. @@ -109,7 +107,7 @@ Fixpoint session_config_supports_exec (t : Term) (sc : Session_Config) : Prop := end. Ltac unfolds := - (* repeat monad_unfold; *) + (* repeat cvm_monad_unfold; *) repeat unfold manifest_generator, generate_ASP_dispatcher, aspid_manifest_update, sig_params, hsh_params, enc_params in *; @@ -130,7 +128,6 @@ Proof. Qed. Global Hint Resolve man_gen_aspid_in : core. -Require Import Manifest_Generator_Union Cvm_Run AM_Manager. (* @@ -205,17 +202,6 @@ Ltac kill_map_none := let H''' := fresh "H'" in eapply H4 in H1 as H'; destruct H'; find_rewrite; congruence - (* | H1 : In_set ?x ?l, - H3 : map_get (_ ?l' ?fn) ?x = None, - H4 : forall _ : _, In_set _ ?l -> _ - |- _ => - let H' := fresh "H'" in - let H'' := fresh "H'" in - let H''' := fresh "H'" in - eapply H4 in H1 as H'; - assert (H'' : fn x = true) by ff; - pose proof (filter_resolver _ _ _ H' H'') as H'''; - destruct H'''; find_rewrite; congruence *) end. Lemma never_change_sess_conf : forall t st res st', @@ -223,12 +209,8 @@ Lemma never_change_sess_conf : forall t st res st', st_config st = st_config st'. Proof. intros; - destruct st. - simpl; eauto. - edestruct sc_immut; eauto. - unfold execErr. - rewrite H. - simpl; eauto. + destruct st; + find_apply_lem_hyp sc_immut_better; simpl in *; ff. Qed. Local Hint Resolve never_change_sess_conf : core. @@ -246,11 +228,11 @@ Theorem well_formed_am_config_impl_executable : forall t sc, Proof. induction t; simpl in *; intuition; eauto. - destruct a; - try (simpl in *; monad_unfold; eauto; fail); (* NULL, CPY *) + try (simpl in *; cvm_monad_unfold; eauto; fail); (* NULL, CPY *) subst; simpl in *; try rewrite eqb_refl in *; repeat ( try break_match; - try monad_unfold; + try cvm_monad_unfold; try break_match try find_injection; try find_contradiction; @@ -290,7 +272,7 @@ Proof. repeat ( unfold remote_session, doRemote, doRemote_session', do_remote, check_cvm_policy in *; try break_match; - try monad_unfold; + try cvm_monad_unfold; try break_match try find_injection; try find_contradiction; @@ -303,14 +285,14 @@ Proof. repeat find_apply_hyp_hyp; repeat find_rewrite; congruence. - break_exists; intuition. eapply IHt1 in H1; intuition; eauto; - monad_unfold; break_exists; find_rewrite; eauto. + cvm_monad_unfold; break_exists; find_rewrite; eauto. find_eapply_lem_hyp sc_immut_better; find_rewrite. eapply IHt2 in H; intuition; eauto; break_exists; repeat find_rewrite; eauto. - subst; simpl in *; try rewrite eqb_refl in *; repeat ( try break_match; - try monad_unfold; + try cvm_monad_unfold; try break_match try find_injection; try find_contradiction; @@ -367,7 +349,7 @@ Proof. - subst; simpl in *; try rewrite eqb_refl in *; repeat ( try break_match; - try monad_unfold; + try cvm_monad_unfold; try break_match try find_injection; try find_contradiction; @@ -555,7 +537,6 @@ Proof. find_apply_hyp_hyp; break_exists; congruence. - break_exists; intuition; eauto. Qed. -Require Import ManCompSoundness_Helpers. Lemma places_decomp: forall t1 t2 p tp, In p (places' t2 (places' t1 [])) -> @@ -568,7 +549,8 @@ assert (In p (places' t2 []) \/ In p (places' t1 [])). { assert (In p (places' t1 []) \/ (~ In p (places' t1 []))). { - apply In_dec_tplc. + + apply In_dec_tplc. } door. + @@ -734,20 +716,16 @@ Proof. Qed. Lemma asdf_easy : forall t1 t2 tp absMan e, -map_get (manifest_generator' tp t2 - (manifest_generator' tp t1 e)) tp = Some absMan -> - -exists m', (* p', -In p' (places tp t1) /\ -*) -map_get (manifest_generator' tp t1 e) tp = Some m' /\ -manifest_subset m' absMan. + map_get (manifest_generator' tp t2 + (manifest_generator' tp t1 e)) tp = Some absMan -> + + exists m', (* p', + In p' (places tp t1) /\ + *) + map_get (manifest_generator' tp t1 e) tp = Some m' /\ + manifest_subset m' absMan. Proof. - intros. - eapply asdf. - eassumption. - ff. - eauto. + intros; eapply asdf; ff. Qed. Lemma manifest_supports_term_sub : forall m1 m2 t, @@ -757,8 +735,7 @@ Lemma manifest_supports_term_sub : forall m1 m2 t, Proof. intros. generalizeEverythingElse t. - induction t; simpl in *; intuition; eauto; - repeat ff. + induction t; simpl in *; intuition; eauto; ff. Qed. Lemma env_subset_man_subset : forall e1 e2 p m m', @@ -812,7 +789,7 @@ Proof. ff. assert (tp = p). { - eapply eqb_eq_plc; eauto. + rewrite String.eqb_eq in *; ff. } subst. @@ -844,8 +821,7 @@ Proof. destruct H0. ++ subst. - rewrite eqb_plc_refl in *. - solve_by_inversion. + rewrite String.eqb_refl in *; ff. ++ assert ((In t' (place_terms t1 tp p)) \/ (In t' (place_terms t2 tp p))). { @@ -876,7 +852,7 @@ Proof. unfold places in *. invc H2. +++++ - rewrite eqb_plc_refl in Heqb. + rewrite String.eqb_refl in Heqb. solve_by_inversion. +++++ eauto. @@ -898,7 +874,7 @@ Proof. eauto. invc H2. +++++ - rewrite eqb_plc_refl in *. + rewrite String.eqb_refl in *. solve_by_inversion. +++++ eassumption. @@ -915,7 +891,7 @@ Proof. ff. assert (tp = p). { - eapply eqb_eq_plc; eauto. + eapply String.eqb_eq; eauto. } subst. @@ -943,7 +919,7 @@ Proof. destruct H0. ++ subst. - rewrite eqb_plc_refl in *. + rewrite String.eqb_refl in *. solve_by_inversion. ++ assert ((In t' (place_terms t1 tp p)) \/ (In t' (place_terms t2 tp p))). @@ -976,7 +952,7 @@ Proof. unfold places in *. invc H2. +++++ - rewrite eqb_plc_refl in Heqb. + rewrite String.eqb_refl in Heqb. solve_by_inversion. +++++ eauto. @@ -998,7 +974,7 @@ Proof. eauto. invc H2. +++++ - rewrite eqb_plc_refl in *. + rewrite String.eqb_refl in *. solve_by_inversion. +++++ eassumption. @@ -1016,7 +992,7 @@ Proof. ff. assert (tp = p). { - eapply eqb_eq_plc; eauto. + eapply String.eqb_eq; eauto. } subst. @@ -1044,7 +1020,7 @@ Proof. destruct H0. ++ subst. - rewrite eqb_plc_refl in *. + rewrite String.eqb_refl in *. solve_by_inversion. ++ assert ((In t' (place_terms t1 tp p)) \/ (In t' (place_terms t2 tp p))). @@ -1077,7 +1053,7 @@ Proof. unfold places in *. invc H2. +++++ - rewrite eqb_plc_refl in Heqb. + rewrite String.eqb_refl in Heqb. solve_by_inversion. +++++ eauto. @@ -1099,7 +1075,7 @@ Proof. eauto. invc H2. +++++ - rewrite eqb_plc_refl in *. + rewrite String.eqb_refl in *. solve_by_inversion. +++++ eassumption. @@ -1163,8 +1139,6 @@ Proof. Unshelve. eapply default_uuid. Qed. -Require Import Manifest_Generator_Union. - Close Scope cop_ent_scope. Lemma map_get_some_impl_in : forall (A B : Type) `{EqClass A} (m : Maps.MapC A B) p v, @@ -2033,7 +2007,7 @@ Proof. unfold run_cvm_w_config, run_cvm, run_core_cvm; destruct a; simpl in *; eauto; repeat (break_match; subst; repeat find_rewrite; repeat find_injection; - simpl in *; intuition; eauto; try monad_unfold; try congruence). + simpl in *; intuition; eauto; try cvm_monad_unfold; try congruence). unfold generate_ASP_dispatcher, generate_ASP_dispatcher' in *; simpl in *; intuition. * unfold generate_ASP_dispatcher, generate_ASP_dispatcher' in *; simpl in *; intuition. ff; simpl in *. diff --git a/src/ManCompSoundness_Appraisal.v b/src/ManCompSoundness_Appraisal.v index 5d0bf22..62d0b4f 100644 --- a/src/ManCompSoundness_Appraisal.v +++ b/src/ManCompSoundness_Appraisal.v @@ -2,11 +2,11 @@ Namely, that the compiler outputs a collection of manifests that support appraisal execution over the input evidence. *) -Require Import Manifest Attestation_Session Session_Config_Compiler Manifest_Generator ID_Type - Maps Term_Defs List Cvm_St Cvm_Impl ErrorStMonad_Coq StructTactics - Cvm_Monad EqClass Manifest_Admits Auto. -Require Import Manifest_Generator_Facts Eqb_Evidence ManCompSoundness. -Require Import Manifest_Generator_Union. +Require Import Manifest Attestation_Session + Maps Term_Defs + Cvm_Monad AM_Monad Auto EqClass. +Require Import Manifest_Generator_Facts ManCompSoundness + Appraisal_Defs Manifest_Set Session_Config_Compiler AM_Manager Manifest_Generator Manifest_Generator_Union. Require Import Coq.Program.Tactics Lia. @@ -103,11 +103,10 @@ Lemma peel_n_am_immut : forall n ls st x st', peel_n_am n ls st = (x, st') -> st = st'. Proof. -induction n; intuition; repeat ff; eauto. + induction n; intuition; ffa using cvm_monad_unfold. Qed. Local Hint Resolve peel_n_am_immut : core. -Require Import Appraisal_Defs. Lemma firstn_works{A:Type}: forall (ls:list A) n, @@ -126,29 +125,28 @@ st = st'. Proof. intros. unfold decrypt_bs_to_rawev' in *. -monad_unfold. +cvm_monad_unfold. repeat (ff; try unfold am_falim in * ; eauto). Qed. Local Hint Resolve decrypt_amst_immut : core. Lemma peel_bs_am_works : forall ls st st' r, -length ls > 0 -> -peel_bs_am ls st = (r,st') -> -exists res, -r = resultC res. + length ls > 0 -> + peel_bs_am ls st = (r,st') -> + exists res, + r = resultC res. Proof. -intros. -destruct ls; ff. -eexists. eauto. + intros. + destruct ls; ffa using cvm_monad_unfold. Qed. Lemma peel_n_am_works : forall n ls st st' r, -length ls >= n -> -peel_n_am n ls st = (r,st') -> -exists res, -r = resultC res. + length ls >= n -> + peel_n_am n ls st = (r,st') -> + exists res, + r = resultC res. Proof. - induction n; intuition; repeat ff; eauto. + induction n; intuition; ffa using cvm_monad_unfold. assert (length l >= n) by lia. eauto. Qed. @@ -156,16 +154,15 @@ Lemma peel_n_am_res_spec : forall n ls st st' r0 r1, peel_n_am n ls st = (resultC (r0, r1),st') -> ls = r0 ++ r1 /\ length r0 = n. Proof. - induction n; intuition; repeat ff; eauto; - find_eapply_hyp_hyp; intuition; ff. + induction n; intuition; ffa using cvm_monad_unfold. Qed. Lemma peel_n_am_err_spec : forall n ls st st' s, peel_n_am n ls st = (errC s,st') -> length ls < n. Proof. - induction n; intuition; repeat ff; eauto; subst; - try find_eapply_hyp_hyp; lia. + induction n; intuition; ffa using cvm_monad_unfold; + try lia. Qed. Lemma has_nonces_cumul : forall et ls m, @@ -175,8 +172,6 @@ Proof. induction et; intros; ff. unfold has_nonces in *. ff. - intros. - ff. Qed. Lemma has_nonces_cumul' : forall et ls ls' m, @@ -184,26 +179,10 @@ has_nonces (nonce_ids_et' et ls) m -> has_nonces ls' m -> has_nonces (nonce_ids_et' et ls') m. Proof. - induction et; intros; ff. - - - unfold has_nonces in *. - ff. - intros. - ff. - - - unfold has_nonces in *. - ff. - intros. - ff. - eauto. - - - assert (has_nonces (nonce_ids_et' et1 ls) m). - eapply has_nonces_cumul. - eassumption. - - eapply IHet2. - eassumption. - eapply has_nonces_cumul; eauto. + induction et; intros; ffa using (intuition; unfold has_nonces in *). + - assert (has_nonces (nonce_ids_et' et1 ls) m) by ( + eapply has_nonces_cumul; eauto). + ffa. Qed. Lemma peel_bs_am_st_immut : forall ls st r st', @@ -220,7 +199,9 @@ Lemma checkNonce'_st_immut : forall n b st r st', checkNonce' n b st = (r, st') -> st = st'. Proof. - unfold checkNonce'; repeat (ff; intuition; eauto). + intuition. + unfold checkNonce' in *; + ffa using am_monad_unfold. Qed. Local Hint Resolve checkNonce'_st_immut : core. @@ -228,7 +209,9 @@ Lemma check_asp_EXTD' : forall a p r1 r2 st st' r, Appraisal_Defs.check_asp_EXTD' a p r1 r2 st = (r, st') -> st = st'. Proof. - unfold check_asp_EXTD'; repeat (ff; intuition; eauto). + intuition; + unfold check_asp_EXTD' in *; + ffa using am_monad_unfold. Qed. Local Hint Resolve check_asp_EXTD' : core. @@ -240,9 +223,9 @@ Proof. generalizeEverythingElse et. induction et; intros; simpl in *; intuition; eauto. - ff. - - repeat ff; simpl in *; eauto; - eapply peel_bs_am_st_immut in Heqp; subst; eauto. - - repeat (break_match; try unfold res_bind, ";;", ret, am_failm in *; + - ffa using cvm_monad_unfold. + all: find_apply_lem_hyp peel_bs_am_st_immut; subst; eauto. + - repeat (break_match; am_monad_unfold; simpl in *; subst; intuition; eauto; try find_injection; try congruence); eauto; repeat match goal with @@ -259,8 +242,7 @@ Proof. assert (a = a') by eauto; subst; eauto; clear H end. - - repeat ff; - repeat find_eapply_hyp_hyp; subst; eauto. + - ffa using cvm_monad_unfold. Qed. Theorem well_formed_am_config_impl_executable_app : forall et sc ls, @@ -278,26 +260,19 @@ Proof. generalizeEverythingElse et. induction et; intros; intuition; subst; eauto. - (* mt case *) - ff; eauto. + ffa using am_monad_unfold. - (* nn case *) - ff. - destruct r. + ffa using am_monad_unfold. + eapply peel_bs_am_contra; try eauto; try lia. - + repeat ff; intuition; eauto. - unfold has_nonces, Appraisal_Defs.checkNonce' in *. - repeat ff; intuition; eauto. + + unfold has_nonces, checkNonce' in *. + ffa using am_monad_unfold. assert (exists bs, map_get (am_nonceMap st) n = Some bs) by eauto. assert (st = a0). { intuition; eauto. - unfold am_failm in *. - ff. - eapply peel_bs_am_immut; eauto. } - subst. - unfold am_failm in *. - ff. - find_rewrite; break_exists; congruence. + break_exists. + ffa. - (* uu case *) simpl in *. @@ -306,7 +281,7 @@ Proof. try (left; repeat eexists; eauto; congruence); simpl in *; destruct_conjs; simpl in *; intuition; eauto; - monad_unfold; + am_monad_unfold; simpl in *; repeat break_let; assert (st = a) by eauto; subst; assert (exists res, r = resultC res) by ( @@ -316,8 +291,8 @@ Proof. break_match; intuition; eauto; repeat find_injection; repeat find_rewrite; eauto; unfold decrypt_bs_to_rawev' in *; - monad_unfold; repeat ff; eauto; - unfold am_failm, check_et_size, check_asp_EXTD in *; + am_monad_unfold; ffa using am_monad_unfold. + all: unfold am_failm, check_et_size, check_asp_EXTD in *; repeat find_injection; repeat find_rewrite; eauto; try congruence; try (find_apply_lem_hyp decrypt_prim_runtime; subst; eauto; congruence); eauto. * unfold session_config_subset in *; intuition; @@ -357,19 +332,12 @@ Proof. eassumption. } - (* - firstn_length_le: - forall [A : Type] (l : list A) [n : nat], - n <= length l -> length (firstn n l) = n - - *) - eapply firstn_works. lia. destruct_conjs. - monad_unfold. + cvm_monad_unfold. break_let. rewrite H10 in *. @@ -384,8 +352,8 @@ Proof. eassumption. 2: { - unfold session_config_subset in *; - destruct_conjs; repeat ff; intuition; eauto. + unfold session_config_subset in *; destruct_conjs; + intuition. } 2: { @@ -425,14 +393,9 @@ Proof. find_rewrite. ff. - - left. - eauto. - destruct_conjs. - invc H10. assert (H9 = a2). @@ -449,18 +412,15 @@ Proof. find_rewrite. - ff. - - right. eauto. + ffa. destruct_conjs. - monad_unfold. + cvm_monad_unfold. break_let. right. ff. - eauto. Qed. Fixpoint manifest_support_term_app (m : Manifest) (e : Evidence) : Prop := @@ -529,8 +489,6 @@ Fixpoint att_sess_supports_term_app (ats : Attestation_Session) (e : Evidence) att_sess_supports_term_app ats e2 end. -Require Import AM_Manager. - Theorem manifest_support_sc_impl_sc_exec: forall t absMan ats, well_formed_manifest absMan -> manifest_support_term_app absMan t -> @@ -587,10 +545,6 @@ Proof. intros. generalizeEverythingElse et. induction et; intros; ff; eauto. - - (* uu case *) - subst; ff; eauto. - - (* ss case *) - ff; eauto. Qed. Lemma manifest_generator_app_cumul' : forall et m1 cm m1', @@ -765,7 +719,7 @@ Proof. simpl in *; unfold manifest_generator_plcEvidence_list in *; simpl in *; ff; - unfold res_bind in *; repeat ff; eauto. + unfold res_bind in *; ffa using am_monad_unfold. Qed. Global Hint Resolve mangen_plcTerm_list_spec : core. @@ -825,11 +779,6 @@ Proof. ff. pose proof (mangen_plcEvidence_list_spec _ _ _ _ _ _ H Heqr0 H0). destruct (map_get (env_list_union l) p) eqn:E; ff. - - pose proof (H2 _ eq_refl). - clear H2 H4. - unfold env_list_union in E. - pose proof (manifest_part_of_fold_ind_impl_fold _ _ _ _ H3 H1 e_empty); break_exists; intuition; repeat find_rewrite; - try find_injection; eapply manifest_subset_trans; eauto. - unfold env_list_union in *. pose proof (manifest_part_of_fold_ind_impl_fold _ _ _ _ H3 H1 e_empty); break_exists; intuition; congruence. Qed. @@ -934,7 +883,7 @@ Proof. intros. unfold manifest_generator_app, res_bind, manifest_update_env_res in *; - repeat ff. + ffa using am_monad_unfold. unfold add_compat_map_manifest; destruct m; simpl in *; eauto. Qed. @@ -1160,7 +1109,7 @@ Proof. intros. unfold end_to_end_mangen, res_bind, manifest_update_env_res in *; - repeat ff. + ffa using cvm_monad_unfold. assert (forall k v', map_get (Maps.map_map (fun m : Manifest => add_compat_map_manifest m cm) @@ -1215,7 +1164,7 @@ Proof. pose proof (mangen_app_same_comp_map _ _ _ _ E _ _ H2). unfold manifest_generator_app, res_bind, manifest_update_env_res in *; - repeat ff. + ffa using cvm_monad_unfold. eapply man_gen_old_always_supports_app in Heqr0. find_rewrite. eapply manifest_supports_term_sub_app; eauto. diff --git a/src/ManCompSoundness_Helpers.v b/src/ManCompSoundness_Helpers.v index c720c2a..674edec 100644 --- a/src/ManCompSoundness_Helpers.v +++ b/src/ManCompSoundness_Helpers.v @@ -1,15 +1,9 @@ (* Helper Lemmas in support of Manifest Compiler Soundness proofs. *) -Require Import Term_Defs_Core Manifest Manifest_Generator Manifest_Generator_Helpers EqClass Manifest_Generator_Facts Manifest_Admits Eqb_Evidence. - -Require Import Params_Admits. +Require Import Term_Defs_Core Manifest_Generator_Helpers Eqb_Evidence. Require Import StructTactics Auto. -Require Import Coq.Program.Tactics. - -Require Import Coq.Program.Equality. - Require Import List. Import ListNotations. @@ -18,25 +12,25 @@ Lemma places'_cumul : forall t p ls, In p ls -> In p (places' t ls). Proof. - intros. - generalizeEverythingElse t. - induction t; intros; - try (destruct a); - ff; eauto. + intros. + generalizeEverythingElse t. + induction t; intros; + try (destruct a); + ff; eauto. Qed. Lemma In_dec_tplc : forall (p:Plc) ls, In p ls \/ ~ In p ls. Proof. - intros. - assert ({In p ls} + {~ In p ls}). - { - apply In_dec. - intros. - destruct (eq_plc_dec x y); eauto. - } - destruct H; eauto. + intros. + assert ({In p ls} + {~ In p ls}). + { + apply In_dec. + intros. + destruct (eq_plc_dec x y); eauto. + } + destruct H; eauto. Qed. @@ -45,49 +39,12 @@ Lemma places_app_cumul : forall p t ls ls', ~ In p ls -> In p (places' t ls'). Proof. - intros. - generalizeEverythingElse t. - induction t; intros; ff. - - (* asp case *) - congruence. - - (* at case *) - door; - eauto. - - (* lseq case *) - destruct (In_dec_tplc p (places' t1 ls)). - + - assert (In p (places' t1 ls')) by eauto. - apply places'_cumul. - eassumption. - + - assert (In p (places' t2 ls)) by eauto. - eapply IHt2. - eassumption. - eassumption. - - (* bseq case *) - - destruct (In_dec_tplc p (places' t1 ls)). - + - assert (In p (places' t1 ls')) by eauto. - apply places'_cumul. - eassumption. - + - assert (In p (places' t2 ls)) by eauto. - eapply IHt2. - eassumption. - eassumption. - - (* bpar case *) - - destruct (In_dec_tplc p (places' t1 ls)). - + - assert (In p (places' t1 ls')) by eauto. - apply places'_cumul. - eassumption. - + - assert (In p (places' t2 ls)) by eauto. - eapply IHt2. - eassumption. - eassumption. + intros. + generalizeEverythingElse t. + induction t; intros; ffa using intuition. + all: + destruct (In_dec_tplc p (places' t1 ls)); ffa; + eapply places'_cumul; eauto. Qed. Lemma top_plc_refl: forall t' p1, In t' (place_terms t' p1 p1). @@ -100,27 +57,14 @@ Proof. Qed. Lemma app_not_empty : forall A (l1 l2:list A), -l1 ++ l2 <> [] -> -l1 <> [] \/ l2 <> []. + l1 ++ l2 <> [] -> + l1 <> [] \/ l2 <> []. Proof. intros. destruct l1; - destruct l2. - - - ff. - congruence. - - - ff. - - - ff. - left. - unfold not. - intros. - congruence. - - - ff. - left. - congruence. + destruct l2; ff. + - left; intuition; ff. + - left; intuition; ff. Qed. @@ -267,7 +211,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } apply places'_cumul. @@ -285,7 +228,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } apply places'_cumul'. eauto. @@ -318,7 +260,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } apply places'_cumul. @@ -336,7 +277,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } @@ -371,7 +311,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } apply places'_cumul. @@ -389,7 +328,6 @@ repeat ff. solve_by_inversion. } door; ff. - congruence. } apply places'_cumul'. eauto. @@ -397,13 +335,8 @@ Qed. Lemma in_not_nil : forall A x (ls:list A), -In x ls -> -ls <> []. + In x ls -> + ls <> []. Proof. - intros. - destruct ls. - - - inversion H. - - - congruence. + intros; destruct ls; ff. Qed. \ No newline at end of file diff --git a/src/Manifest.v b/src/Manifest.v index 2f220c1..08365fc 100644 --- a/src/Manifest.v +++ b/src/Manifest.v @@ -5,11 +5,10 @@ https://github.com/ku-sldg/negotiation20/blob/master/src/Manifest/Manifest.v *) -Require Import ID_Type Term_Defs_Core Maps - Term_Defs EqClass ErrorStMonad_Coq JSON. +Require Import ID_Type Term_Defs_Core Maps. Require Export Manifest_Admits. -Require Import Manifest_Set String ErrorStringConstants. +Require Import Manifest_Set. Require Import List. Import ListNotations. diff --git a/src/Manifest_Generator.v b/src/Manifest_Generator.v index c662339..529b5ad 100644 --- a/src/Manifest_Generator.v +++ b/src/Manifest_Generator.v @@ -2,12 +2,9 @@ Includes separate (but similar) versions of the generator for both attestation (manifest_generator) and appraisal (manifest_generator_app) scenarios. *) -Require Import Term_Defs_Core Params_Admits Manifest Eqb_Evidence - Manifest_Generator_Helpers. +Require Import Term_Defs_Core Params_Admits Manifest. -Require Import ResultT String EqClass Maps StructTactics. - -Require Import Manifest_Union. +Require Import ResultT String Maps StructTactics. Require Export EnvironmentM Manifest_Set. diff --git a/src/Manifest_Generator_Facts.v b/src/Manifest_Generator_Facts.v index 3c5e67e..bea9fe5 100644 --- a/src/Manifest_Generator_Facts.v +++ b/src/Manifest_Generator_Facts.v @@ -2,7 +2,7 @@ Also included: manifest and environment subset definitions and associated properties. TODO: consider renaming some of these lemmas (e.g. fafafa, afafafa, ...) *) -Require Import Maps Term_Defs_Core Manifest Eqb_Evidence EqClass Manifest_Generator. +Require Import Maps Manifest EqClass Manifest_Generator Manifest_Union. Require Import Auto StructTactics. @@ -46,7 +46,7 @@ Qed. Global Hint Resolve manifest_subset_trans : core. Lemma manifest_subset_union_l : forall m1 m2, - manifest_subset m1 (Manifest_Union.manifest_union_asps m1 m2). + manifest_subset m1 (manifest_union_asps m1 m2). Proof. induction m1; destruct m2; simpl in *; intuition; eauto; unfold manifest_subset; simpl in *; intuition; eauto; @@ -55,7 +55,7 @@ Qed. Global Hint Resolve manifest_subset_union_l : core. Lemma manifest_subset_union_r : forall m1 m2, - manifest_subset m2 (Manifest_Union.manifest_union_asps m1 m2). + manifest_subset m2 (manifest_union_asps m1 m2). Proof. induction m1; destruct m2; simpl in *; intuition; eauto; unfold manifest_subset; simpl in *; intuition; eauto; @@ -212,7 +212,7 @@ Proof. Qed. *) Lemma manifest_union_asps_empty_r : forall m, - Manifest_Union.manifest_union_asps m empty_Manifest = m. + manifest_union_asps m empty_Manifest = m. Proof. destruct m; reflexivity. Qed. diff --git a/src/Manifest_Generator_Helpers.v b/src/Manifest_Generator_Helpers.v index 499309f..64a7e77 100644 --- a/src/Manifest_Generator_Helpers.v +++ b/src/Manifest_Generator_Helpers.v @@ -1,8 +1,8 @@ (* Helper functions used by the Manifest Generator implementation. *) -Require Import Term_Defs_Core Params_Admits Manifest Eqb_Evidence. +Require Import Term_Defs_Core Eqb_Evidence. -Require Import EqClass Maps StructTactics Auto. +Require Import EqClass StructTactics Auto. Require Export EnvironmentM Manifest_Set. diff --git a/src/Manifest_Generator_Union.v b/src/Manifest_Generator_Union.v index 95459d5..e279257 100644 --- a/src/Manifest_Generator_Union.v +++ b/src/Manifest_Generator_Union.v @@ -2,18 +2,14 @@ Uses the (as-yet-unverified) manifest environment union operation to merge manifests generated for combined Attestation and Appraisal scenarios. *) -Require Import Term_Defs_Core Params_Admits Manifest Eqb_Evidence - Manifest_Generator_Helpers Term_Defs ErrorStMonad_Coq. +Require Import Term_Defs_Core Manifest. -Require Import EqClass Maps StructTactics. +Require Import EqClass. -Require Import EnvironmentM Manifest_Set JSON Stringifiable. +Require Import EnvironmentM JSON Stringifiable. -Require Import Manifest_Union Manifest_Generator Cvm_St Cvm_Impl. +Require Import Manifest_Union Manifest_Generator. -Require Import Manifest Manifest_Generator_Facts. - -Require Import Coq.Program.Tactics. Require Import List. Import ListNotations. diff --git a/src/Manifest_JSON.v b/src/Manifest_JSON.v index a97ad7f..2e4cd8a 100644 --- a/src/Manifest_JSON.v +++ b/src/Manifest_JSON.v @@ -1,5 +1,5 @@ Require Import Stringifiable. -Require Import JSON Manifest Manifest_Set Term_Defs_Core Manifest_JSON_Vars List ErrorStringConstants EqClass Maps. +Require Import JSON Manifest Manifest_Set Term_Defs_Core Manifest_JSON_Vars List Maps. Import ListNotations ResultNotation. diff --git a/src/Manifest_Set.v b/src/Manifest_Set.v index 86ef61a..fab7aaa 100644 --- a/src/Manifest_Set.v +++ b/src/Manifest_Set.v @@ -1,10 +1,10 @@ (* Definition of the manifest_set datatype, its operations, and related properties. This datatype is used for "collection" manifest fields, and should act like a traditional mathematical set (e.g. cumulative, non-duplicating, ...) *) -Require Import List String. +Require Import List. -Require Import ID_Type Term_Defs_Core Maps - Term_Defs Manifest_Admits EqClass ErrorStMonad_Coq ErrorStringConstants JSON. +Require Import ID_Type + JSON. Import ListNotations. diff --git a/src/Manifest_Union.v b/src/Manifest_Union.v index 9e9afdf..ac1155f 100644 --- a/src/Manifest_Union.v +++ b/src/Manifest_Union.v @@ -1,7 +1,6 @@ (* Defining union operations for Manifests and Manifest Environments. *) -Require Import ID_Type Term_Defs_Core Maps String - Term_Defs Manifest_Admits EqClass ErrorStMonad_Coq. +Require Import ID_Type Term_Defs_Core Maps. Require Import Manifest Manifest_Set EnvironmentM. diff --git a/src/OptMonad_Coq.v b/src/OptMonad_Coq.v index 9cc65df..a8e7a2d 100644 --- a/src/OptMonad_Coq.v +++ b/src/OptMonad_Coq.v @@ -9,27 +9,21 @@ Author: Adam Petz, ampetz@ku.edu (* Generalized Option Monad *) Definition Opt (A : Type) : Type := (option A). (** S % type. *) -Definition ret {A : Type} (a : A) : Opt A := (Some a). +Definition opt_ret {A : Type} (a : A) : Opt A := (Some a). -Definition bind {A B : Type} (m : Opt A) (f : A -> Opt B) : Opt B := +Definition opt_bind {A B : Type} (m : Opt A) (f : A -> Opt B) : Opt B := match m with | Some v => f v | _ => None end. -Definition failm {A : Type} : Opt A := None. +Definition opt_failm {A : Type} : Opt A := None. -Definition runOpt {A} (h : Opt A) (default: A) : A := - match h with - Some v => v - | _ => default - end. +Module OptNotation. -Definition nop := ret tt. +Notation "a >> b" := (opt_bind a (fun _ => b)) (at level 50). -Notation "a >> b" := (bind a (fun _ => b)) (at level 50). - -Notation "x <- c1 ;; c2" := (@bind _ _ c1 (fun x => c2)) +Notation "x <- c1 ;; c2" := (@opt_bind _ _ c1 (fun x => c2)) (at level 100, c1 at next level, right associativity). Notation "e1 ;; e2" := (_ <- e1 ;; e2) @@ -37,15 +31,13 @@ Notation "e1 ;; e2" := (_ <- e1 ;; e2) Notation "' pat <- c1 ;; c2" := - (@bind _ _ c1 (fun x => match x with pat => c2 end)) + (@opt_bind _ _ c1 (fun x => match x with pat => c2 end)) (at level 100, pat pattern, c1 at next level, right associativity). -Definition when {A} (b : bool) (m : Opt A) : Opt unit := - if b then m ;; ret tt else nop. +End OptNotation. + +Import OptNotation. +Definition opt_when {A} (b : bool) (m : Opt A) : Opt unit := + if b then m ;; opt_ret tt else opt_ret tt. -Definition fromSome{A:Type} (default:A) (opt:Opt A): A := - match opt with - | Some x => x - | _ => default - end. diff --git a/src/Server_AM.v b/src/Server_AM.v index 606468d..6655d05 100644 --- a/src/Server_AM.v +++ b/src/Server_AM.v @@ -1,7 +1,7 @@ (* Implementation of a top-level Server (listener) thread for Server AMs in end-to-end Copland Attestation + Appraisal protocols. *) -Require Import String BS Attestation_Session Interface AM_Helpers AM_Json_Interfaces Manifest. -Require Import List ResultT AM_Manager. +Require Import String BS Interface AM_Json_Interfaces. +Require Import List AM_Manager. Import ListNotations. Open Scope string_scope. diff --git a/src/Session_Config_Compiler.v b/src/Session_Config_Compiler.v index db99349..0bcab96 100644 --- a/src/Session_Config_Compiler.v +++ b/src/Session_Config_Compiler.v @@ -1,6 +1,5 @@ Require Import Manifest Attestation_Session AM_Manager. -Require Import EqClass. -Require Import Term_Defs_Core ResultT ID_Type Manifest_Set Maps Interface. +Require Import Term_Defs_Core ID_Type Manifest_Set Maps Interface. Require Import IO_Stubs. Definition generate_ASP_dispatcher' (am : Manifest) (ats : Attestation_Session) (aspBin : FS_Location) (par : ASP_PARAMS) (rawEv : RawEv) : ResultT RawEv DispatcherErrors := diff --git a/src/Term.v b/src/Term.v index e678605..ffd1402 100644 --- a/src/Term.v +++ b/src/Term.v @@ -3,15 +3,13 @@ --The `events` relation --a denotational semantics for phrase events. --Lemmas/automation related to `events` *) -Require Import Defs Eqb_Evidence. -Require Import Preamble More_lists StructTactics. +Require Import Defs. +Require Import Preamble. Require Import Compare_dec Coq.Program.Tactics. -Require Import PeanoNat. Require Import Lia. -Require Import List. Import List.ListNotations. Require Export Term_Defs Anno_Term_Defs. @@ -27,7 +25,7 @@ Proof. intros. inversion H. tauto. -Defined. +Qed. Lemma wfr_at_pieces: forall t r p, well_formed_r_annt (aatt r p t) -> @@ -36,7 +34,7 @@ Proof. intros. inversion H. tauto. -Defined. +Qed. Lemma wfr_bseq_pieces: forall r s t1 t2, well_formed_r_annt (abseq r s t1 t2) -> @@ -45,7 +43,7 @@ Proof. intros. inversion H. tauto. -Defined. +Qed. Lemma wfr_bpar_pieces: forall r s t1 t2, well_formed_r_annt (abpar r s t1 t2) -> @@ -54,7 +52,7 @@ Proof. intros. inversion H. tauto. -Defined. +Qed. Ltac do_wf_pieces := match goal with @@ -78,7 +76,7 @@ Proof. induction t; try (intros H; simpl; inv H; simpl; repeat find_apply_hyp_hyp; lia). -Defined. +Qed. Lemma esize_nonempty: forall t, esize t > 0. Proof. @@ -86,7 +84,7 @@ Proof. induction t; intros; try (destruct a); (cbn; lia). -Defined. +Qed. Lemma wf_mono: forall t, well_formed_r_annt t -> @@ -97,7 +95,7 @@ Proof. pose (esize_nonempty t). lia. eauto. -Defined. +Qed. Ltac do_mono := (* let asdff := eapply anno_mono; eauto in *) @@ -112,7 +110,7 @@ Lemma asp_lrange_irrel: forall a i a0 a1 n n', Proof. intros. destruct a; ff. -Defined. +Qed. (** This predicate specifies when a term, a place, and some initial evidence is related to an event. In other words, it specifies the @@ -227,7 +225,7 @@ Proof. try (inv_wfr; simpl in *; auto; repeat find_apply_hyp_hyp; repeat (find_apply_lem_hyp well_formed_range_r); lia). -Defined. +Qed. Lemma at_range: forall x r i, diff --git a/src/Term_Defs.v b/src/Term_Defs.v index 180e4bc..80090e2 100644 --- a/src/Term_Defs.v +++ b/src/Term_Defs.v @@ -257,7 +257,3 @@ Inductive AM_Result := Definition empty_am_result := am_rawev []. -Definition policy_list_not_disclosed (t:Term) (p:Plc) (e:Evidence) (ls: list (Plc * ASP_ID)) : bool := (* true. *) - forallb (fun pr => negb (term_discloses_aspid_to_remote_enc_bool t p e (fst pr) (snd pr))) ls. - - diff --git a/src/Term_Defs_Core.v b/src/Term_Defs_Core.v index 68ef122..bf62748 100644 --- a/src/Term_Defs_Core.v +++ b/src/Term_Defs_Core.v @@ -630,8 +630,8 @@ Notation "@ p [ ph ]" := (attc p ph) (in custom core_copland_entry at level 50). Open Scope core_cop_ent_scope. Definition test2 := <{ __ -> {} }>. -Example test2ex : test2 = (lseqc (aspc CPYC) (aspc NULLC)). reflexivity. Defined. -Example test3 : <{ CLR -> {}}> = (lseqc (aspc CLEAR) (aspc NULLC)). reflexivity. Defined. +Example test2ex : test2 = (lseqc (aspc CPYC) (aspc NULLC)). reflexivity. Qed. +Example test3 : <{ CLR -> {}}> = (lseqc (aspc CLEAR) (aspc NULLC)). reflexivity. Qed. (** Raw Evidence representaiton: a list of binary (BS) values. *) Definition RawEv := list BS. diff --git a/src/Term_system.v b/src/Term_system.v index d576b55..ad7b27f 100644 --- a/src/Term_system.v +++ b/src/Term_system.v @@ -10,9 +10,9 @@ This proof script is free software: you can redistribute it and/or modify it under the terms of the BSD License as published by the University of California. See license.txt for details. *) -Require Import Preamble More_lists StructTactics Defs Term_Defs Term Event_system. +Require Import Preamble Defs Term Event_system. -Require Import Lia List PeanoNat. +Require Import Lia PeanoNat. (* Set Nested Proofs Allowed. @@ -80,7 +80,7 @@ Proof. try destruct a; (* asp params destruct *) repeat (econstructor; repeat rewrite evsys_range; auto); tauto). -Defined. +Qed. Ltac do_evin := match goal with @@ -110,7 +110,7 @@ Proof. repeat (find_rewrite; simpl in * ); (find_apply_lem_hyp Nat.succ_inj ) ; subst; auto; tauto. -Defined. +Qed. Ltac inv_sup := match goal with @@ -164,7 +164,7 @@ Proof. repeat inv_sup; auto; tauto). -Defined. +Qed. Lemma evsys_max_unique: forall t p e, diff --git a/src/Trace.v b/src/Trace.v index 006ca80..e4635b7 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -10,9 +10,7 @@ modify it under the terms of the BSD License as published by the University of California. See license.txt for details. *) -Require Import Preamble More_lists Defs Term_Defs Term Event_system Term_system StructTactics. - -Require Import Coq.Program.Tactics. +Require Import Preamble More_lists Defs Term Event_system Term_system. Require Import Lia. @@ -288,7 +286,7 @@ Proof. try rewrite app_length; simpl in *; try find_apply_lem_hyp shuffle_length; lia). -Defined. +Qed. (** The events in a trace correspond to the events associated with an annotated term, a place, and some evidence. *) @@ -814,4 +812,4 @@ Proof. eauto. + solve_by_inversion. -Defined. +Qed. diff --git a/src/tools/README.md b/src/tools/README.md new file mode 100644 index 0000000..5b57b9c --- /dev/null +++ b/src/tools/README.md @@ -0,0 +1,13 @@ +# Tools + +The following tools exist as general purpose tools +that could be used in a Coq development. + +- [find_all_deps](./find_all_deps.sh): This tool takes a single argument (the name of a Coq .v file) and returns an ordered list of the dependencies it **recursively** relies on. + +- [pretty_coq_deps](./pretty_coq_deps.sh): This tool takes a single argument (the name of a Coq .v file) and returns a list of the +dependencies it relies on **non-recursively**. + +- [test_all_files](./test_all_files.sh): This is just a testing tool for checking and validating the dependencies of all files in a directory (passed as the only argument) + +- [validate_all_deps](./validate_all_deps.sh): This tool takes an ordered list of dependencies and validates that each file in that list only depends on files that have previously appear in the list. Basically it is the dual of *find_all_deps*. \ No newline at end of file diff --git a/src/tools/find_all_deps.sh b/src/tools/find_all_deps.sh new file mode 100755 index 0000000..3ad6bf0 --- /dev/null +++ b/src/tools/find_all_deps.sh @@ -0,0 +1,88 @@ +#!/bin/bash +set -eu + +TOOLS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +# Function to find dependencies using BFS +find_dependencies_bfs() { + local file="$1" + local seen_files=("${@:2}") + local queue=("$file") + local seen=() + local result=() + + while [ ${#queue[@]} -gt 0 ]; do + # Dequeue the first element + local current="${queue[0]}" + queue=("${queue[@]:1}") + + # Check if the file has already been processed or is in the initial seen_files + if [[ " ${seen[@]} " =~ " ${current} " ]]; then + # echo -e "SEEN: Already seen $current:\n" + # We must need to reorder as something in seen depends on current + # So drop current from past seen and it will be added to front after + new_array=() + for val in "${seen[@]}"; do + [[ $val != $current ]] && new_array+=("$val") + done + seen=("${new_array[@]}") + unset new_array + fi + seen=("$current" "${seen[@]}") + + DEP_COM="$TOOLS_DIR/pretty_coq_deps.sh $current" + # Get direct dependencies of the current file + deps=$($DEP_COM) + + # Add new dependencies to the queue + for dep in $deps; do + if [[ " ${dep} " =~ " ${current} " ]]; then + # echo "SAW CURRENT FILE: $current, $dep" + continue + fi + # Only enqueue if not already seen + if [[ ! " ${queue[@]} " =~ " ${dep} " ]]; then + if [[ ! " ${seen[@]} " =~ " ${dep} " ]]; then + queue+=("$dep") + else + # We need to reorder seen as $current depends on $dep still + queue+=("$dep") + new_array=() + for val in "${seen[@]}"; do + [[ $val != $dep ]] && new_array+=("$val") + done + seen=("$dep" "${new_array[@]}") + unset new_array + fi + fi + done + done + + # Print the results + res_str="" + for file in "${seen[@]}"; do + if [[ -z "$file" ]]; then + continue + fi + res_str+="$file " + # echo "$file" + done + # res_str=$(printf "%s\n" "${seen[@]}") + echo "$res_str" +} + +# Check if a file is provided +if [ -z "$1" ]; then + echo "Usage: $0 [seen_files...]" + exit 1 +fi + +# Get the initial file and seen files +initial_file="$1" +shift +seen_files=("$@") + +# Start finding dependencies using BFS +find_dependencies_bfs "$initial_file" "${seen_files[@]}" + + diff --git a/src/tools/pretty_coq_deps.sh b/src/tools/pretty_coq_deps.sh new file mode 100755 index 0000000..259d698 --- /dev/null +++ b/src/tools/pretty_coq_deps.sh @@ -0,0 +1,10 @@ +#!/bin/bash +set -eu + +coqdep $1 | +awk -F ': ' '{print $2}' | +tr ' ' '\n' | +sed 's/\.\///g' | +sed 's/\(\w[\w_]*\)\.\(vio\|vo\)/\1.v/g' | +grep -v '^$' + diff --git a/src/tools/test_all_files.sh b/src/tools/test_all_files.sh new file mode 100755 index 0000000..3f5568b --- /dev/null +++ b/src/tools/test_all_files.sh @@ -0,0 +1,9 @@ +#!/bin/bash +set -eu + +TOOLS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +for f in $1/*.v; do + echo "Processing $f" + $TOOLS_DIR/find_all_deps.sh "$f" | $TOOLS_DIR/validate_all_deps.sh +done \ No newline at end of file diff --git a/src/tools/validate_all_deps.sh b/src/tools/validate_all_deps.sh new file mode 100755 index 0000000..15d9244 --- /dev/null +++ b/src/tools/validate_all_deps.sh @@ -0,0 +1,27 @@ +#!/bin/bash +set -eu + +TOOLS_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +files_list=($(cat)) +len=${#files_list[@]} +echo "Files list: ${files_list[@]}" + +# For file in files_list, ensure that $deps is only made of files +# from the previous elements of files_list +for((i=0; i<$len; i++)); do + cur_slice=("${files_list[@]:0:($i + 1)}") + cur_value=${files_list[$i]} + + # Get direct dependencies of the current file + DEP_COM="$TOOLS_DIR/pretty_coq_deps.sh $cur_value" + deps=$($DEP_COM) + + # Check if all dependencies are in previous files_list + for dep in $deps; do + if [[ ! " ${cur_slice[@]} " =~ " ${dep} " ]]; then + echo "ERROR: $dep not in previous files_list" + exit 1 + fi + done +done