Adding a dependency tracking tool and doing some cleanup

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.
 
 

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) 

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,100 +16,54 @@ 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.
 
 
 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 * .
+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 *).

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.

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.

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,20 +23,22 @@ 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) 
   end.
 
 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))