Merge pull request #217 from kth-step/get-contract-thm-fix

make get_arch_contract_thm output idiomatic theorems

Author: palmskog

examples/arm8/incr/incr_propScript.sml

@@ -39,7 +39,7 @@ val _ = new_theory "incr_prop";
 
 val arm8_cont_incr_thm =
  get_arm8_contract_thm
-  bspec_cont_incr
+  bspec_cont_incr incr_init_addr_def [incr_end_addr_def]
   bir_incr_progbin_def
   arm8_incr_pre_def arm8_incr_post_def
   bir_incr_prog_def
@@ -53,7 +53,6 @@ Theorem arm8_cont_incr:
   (arm8_incr_pre pre_x0)
   (arm8_incr_post pre_x0)
 Proof
- rw [incr_init_addr_def,incr_end_addr_def] >>
  ACCEPT_TAC arm8_cont_incr_thm
 QED
 
@@ -62,6 +61,7 @@ QED
 (* ------------------------ *)
 
 val readable_thm = computeLib.RESTR_EVAL_RULE [``arm8_weak_trs``] arm8_cont_incr;
+
 Theorem arm8_cont_incr_full = GEN_ALL readable_thm;
 
 val _ = export_theory ();

examples/arm8/isqrt/isqrt_propScript.sml

@@ -39,7 +39,7 @@ val _ = new_theory "isqrt_prop";
 
 val arm8_cont_isqrt_1_thm =
  get_arm8_contract_thm
-  bspec_cont_isqrt_1
+  bspec_cont_isqrt_1 isqrt_init_addr_1_def [isqrt_end_addr_1_def]
   bir_isqrt_progbin_def
   arm8_isqrt_pre_1_def arm8_isqrt_post_1_def
   bir_isqrt_prog_def
@@ -53,13 +53,12 @@ Theorem arm8_cont_isqrt_1:
   (arm8_isqrt_pre_1 pre_x0)
   (arm8_isqrt_post_1 pre_x0)
 Proof
- rw [isqrt_init_addr_1_def,isqrt_end_addr_1_def] >>
  ACCEPT_TAC arm8_cont_isqrt_1_thm
 QED
 
 val arm8_cont_isqrt_2_thm =
  get_arm8_contract_thm
-  bspec_cont_isqrt_2
+  bspec_cont_isqrt_2 isqrt_init_addr_2_def [isqrt_end_addr_2_def]
   bir_isqrt_progbin_def
   arm8_isqrt_pre_2_def arm8_isqrt_post_2_def
   bir_isqrt_prog_def
@@ -73,13 +72,12 @@ Theorem arm8_cont_isqrt_2:
   (arm8_isqrt_pre_2 pre_x1 pre_x3)
   (arm8_isqrt_post_2 pre_x1 pre_x3)
 Proof
- rw [isqrt_init_addr_2_def,isqrt_end_addr_2_def] >>
  ACCEPT_TAC arm8_cont_isqrt_2_thm
 QED
 
 val arm8_cont_isqrt_3_thm =
  get_arm8_contract_thm
-  bspec_cont_isqrt_3
+  bspec_cont_isqrt_3 isqrt_init_addr_3_def [isqrt_end_addr_3_loop_def, isqrt_end_addr_3_ret_def]
   bir_isqrt_progbin_def
   arm8_isqrt_pre_3_def arm8_isqrt_post_3_def
   bir_isqrt_prog_def
@@ -93,7 +91,6 @@ Theorem arm8_cont_isqrt_3:
   (arm8_isqrt_pre_3 pre_x1 pre_x2 pre_x3)
   (arm8_isqrt_post_3 pre_x1 pre_x2 pre_x3)
 Proof
- rw [isqrt_init_addr_3_def,isqrt_end_addr_3_loop_def,isqrt_end_addr_3_ret_def] >>
  ACCEPT_TAC arm8_cont_isqrt_3_thm
 QED
 

examples/arm8/max/max_propScript.sml

@@ -39,7 +39,7 @@ val _ = new_theory "max_prop";
 
 val arm8_cont_max_thm =
  get_arm8_contract_thm
-  bspec_cont_max
+  bspec_cont_max max_init_addr_def [max_end_addr_def]
   bir_max_progbin_def
   arm8_max_pre_def arm8_max_post_def
   bir_max_prog_def
@@ -53,7 +53,6 @@ Theorem arm8_cont_max:
   (arm8_max_pre pre_x0 pre_x1)
   (arm8_max_post pre_x0 pre_x1)
 Proof
- rw [max_init_addr_def,max_end_addr_def] >>
  ACCEPT_TAC arm8_cont_max_thm
 QED
 

examples/arm8/swap/swap_propScript.sml

@@ -39,7 +39,7 @@ val _ = new_theory "swap_prop";
 
 val arm8_cont_swap_thm =
  get_arm8_contract_thm
-  bspec_cont_swap
+  bspec_cont_swap swap_init_addr_def [swap_end_addr_def]
   bir_swap_progbin_def
   arm8_swap_pre_def arm8_swap_post_def
   bir_swap_prog_def
@@ -53,7 +53,6 @@ Theorem arm8_cont_swap:
   (arm8_swap_pre pre_x0 pre_x1 pre_x0_deref pre_x1_deref)
   (arm8_swap_post pre_x0 pre_x1 pre_x0_deref pre_x1_deref)
 Proof
- rw [swap_init_addr_def,swap_end_addr_def] >>
  ACCEPT_TAC arm8_cont_swap_thm
 QED
 
@@ -62,6 +61,7 @@ QED
 (* ----------------------- *)
 
 val readable_thm = computeLib.RESTR_EVAL_RULE [``arm8_weak_trs``] arm8_cont_swap;
+
 Theorem arm8_cont_swap_full = GEN_ALL readable_thm;
 
 val _ = export_theory ();

examples/riscv/incr/incr_propScript.sml

@@ -39,7 +39,7 @@ val _ = new_theory "incr_prop";
 
 val riscv_cont_incr_thm =
  get_riscv_contract_thm
-  bspec_cont_incr
+  bspec_cont_incr incr_init_addr_def [incr_end_addr_def]
   bir_incr_progbin_def
   riscv_incr_pre_def riscv_incr_post_def
   bir_incr_prog_def
@@ -53,7 +53,6 @@ Theorem riscv_cont_incr:
   (riscv_incr_pre pre_x10)
   (riscv_incr_post pre_x10)
 Proof
- rw [incr_init_addr_def,incr_end_addr_def] >>
  ACCEPT_TAC riscv_cont_incr_thm
 QED
 
@@ -62,6 +61,7 @@ QED
 (* ------------------------ *)
 
 val readable_thm = computeLib.RESTR_EVAL_RULE [``riscv_weak_trs``] riscv_cont_incr;
+
 Theorem riscv_cont_incr_full = GEN_ALL readable_thm;
 
 val _ = export_theory ();

examples/riscv/swap/swap_propScript.sml

@@ -33,22 +33,15 @@ open swap_symb_transfTheory;
 
 val _ = new_theory "swap_prop";
 
-(* --------------------- *)
-(* Auxiliary definitions *)
-(* --------------------- *)
-
-val progbin_tm = (fst o dest_eq o concl) bir_swap_progbin_def;
-val riscv_pre_tm = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_swap_pre_def;
-val riscv_post_tm = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_swap_post_def;
-
 (* ---------------------------------- *)
 (* Backlifting BIR contract to RISC-V *)
 (* ---------------------------------- *)
 
 val riscv_cont_swap_thm =
- get_riscv_contract
-  bspec_cont_swap
-  progbin_tm riscv_pre_tm riscv_post_tm
+ get_riscv_contract_thm
+  bspec_cont_swap swap_init_addr_def [swap_end_addr_def]
+  bir_swap_progbin_def
+  riscv_swap_pre_def riscv_swap_post_def
   bir_swap_prog_def
   [bspec_swap_pre_def]
   bspec_swap_pre_def swap_riscv_pre_imp_bspec_pre_thm
@@ -60,7 +53,6 @@ Theorem riscv_cont_swap:
   (riscv_swap_pre pre_x10 pre_x11 pre_x10_deref pre_x11_deref)
   (riscv_swap_post pre_x10 pre_x11 pre_x10_deref pre_x11_deref)
 Proof
- rw [swap_init_addr_def,swap_end_addr_def] >>
  ACCEPT_TAC riscv_cont_swap_thm
 QED
 
@@ -69,6 +61,7 @@ QED
 (* ------------------------ *)
 
 val readable_thm = computeLib.RESTR_EVAL_RULE [``riscv_weak_trs``] riscv_cont_swap;
+
 Theorem riscv_cont_swap_full = GEN_ALL readable_thm;
 
 val _ = export_theory ();

examples/riscv/swap/swap_symb_transfScript.sml

@@ -13,35 +13,22 @@ open swap_symb_execTheory;
 
 val _ = new_theory "swap_symb_transf";
 
-(* --------------------- *)
-(* Auxiliary definitions *)
-(* --------------------- *)
-
-val init_addr_tm = (snd o dest_eq o concl) swap_init_addr_def;
-val end_addr_tm = (snd o dest_eq o concl) swap_end_addr_def;
-
-val bspec_pre_tm = (lhs o snd o strip_forall o concl) bspec_swap_pre_def;
-val bspec_post_tm = (lhs o snd o strip_forall o concl) bspec_swap_post_def;
-
 (* ------------------------------- *)
 (* BIR symbolic execution analysis *)
 (* ------------------------------- *)
 
 val bspec_cont_thm =
- bir_symb_transfer init_addr_tm end_addr_tm bspec_pre_tm bspec_post_tm
-  bir_swap_prog_def swap_birenvtyl_def
-  bspec_swap_pre_def bspec_swap_post_def swap_prog_vars_list_def
+ bir_symb_transfer_thm
+  bir_swap_prog_def
+  swap_init_addr_def swap_end_addr_def
+  bspec_swap_pre_def bspec_swap_post_def
+  swap_birenvtyl_def swap_prog_vars_list_def
   swap_symb_analysis_thm NONE swap_prog_vars_thm;
 
-Theorem bspec_cont_swap:
- bir_cont bir_swap_prog bir_exp_true
-  (BL_Address (Imm64 ^init_addr_tm)) {BL_Address (Imm64 ^end_addr_tm)} {}
-  ^bspec_pre_tm
-  (\l. if l = BL_Address (Imm64 ^end_addr_tm)
-       then ^bspec_post_tm
-       else bir_exp_false)
-Proof
- rw [bir_swap_prog_def,bspec_cont_thm]
-QED
+val _ = show_tags := true;
+
+val _ = Portable.pprint Tag.pp_tag (tag bspec_cont_thm);
+
+Theorem bspec_cont_swap = bspec_cont_thm
 
 val _ = export_theory ();

examples/riscv/test-riscv.sml

@@ -39,7 +39,7 @@ val _ = print_and_check_thm
 val _ = print_and_check_thm
   "swap BSPEC contract theorem"
   bspec_cont_swap
-  ``bir_cont (bir_swap_prog : 'a bir_program_t)
+  ``bir_cont (bir_swap_prog : 'obs_type bir_program_t)
     bir_exp_true (BL_Address (Imm64 0x10488w))
     {BL_Address (Imm64 0x1049cw)} {}
     (bspec_swap_pre pre_x10 pre_x11 pre_x10_deref pre_x11_deref)

src/tools/backlifter/bir_backlifterLib.sig

@@ -6,13 +6,13 @@ sig
   val get_arm8_contract : thm -> term -> term -> term ->
     thm -> thm list -> thm -> thm -> thm list -> thm -> thm -> thm;
 
-  val get_arm8_contract_thm : thm -> thm -> thm -> thm ->
+  val get_arm8_contract_thm : thm -> thm -> thm list -> thm -> thm -> thm ->
     thm -> thm list -> thm -> thm -> thm list -> thm -> thm -> thm;
 
   val get_riscv_contract : thm -> term -> term -> term ->
     thm -> thm list -> thm -> thm -> thm list -> thm -> thm -> thm;
 
-  val get_riscv_contract_thm : thm -> thm -> thm -> thm ->
+  val get_riscv_contract_thm : thm -> thm -> thm list -> thm -> thm -> thm ->
     thm -> thm list -> thm -> thm -> thm list -> thm -> thm -> thm;
 
 end

src/tools/backlifter/bir_backlifterLib.sml

@@ -119,6 +119,82 @@ open bir_inst_liftingHelpersLib;
     arch_contract_thm
   end;
 
+  fun get_arch_contract_thm arch_cont
+   arch_lift_contract_thm arch_wf_varset_def arch_vars_def bir_post_bir_to_arch_def
+   bir_ct init_addr_def end_addr_defs prog_bin_def arch_pre_def arch_post_def bir_prog_def bir_pre_defs
+   bir_pre1_def arch_pre_imp_bir_pre_thm bir_post_defs
+   arch_post_imp_bir_post_thm bir_is_lifted_prog_thm =
+  let
+    val prog_bin = (fst o dest_eq o concl) prog_bin_def;
+    val arch_pre = (fst o dest_comb o lhs o snd o strip_forall o concl) arch_pre_def;
+    val arch_post = (fst o dest_comb o lhs o snd o strip_forall o concl) arch_post_def;
+    val init_addr = (fst o dest_eq o concl) init_addr_def;
+    val end_addrs = pred_setSyntax.mk_set (map (fst o dest_eq o concl) end_addr_defs);
+    val word_from_address = bir_immSyntax.dest_Imm64 o bir_programSyntax.dest_BL_Address;
+    val bir_prog = get_bir_cont_prog bir_ct;
+    val l = word_from_address (get_bir_cont_start_label bir_ct);
+    val ls_set = get_bir_cont_ilist bir_ct;
+    val ls = pred_setSyntax.mk_set (map word_from_address (pred_setSyntax.strip_set ls_set));
+    val add_lift_thm =
+      ISPECL [bir_prog,
+	      prog_bin,
+	      l,
+	      ls,
+	      (((el 2) o snd o strip_comb o concl) bir_is_lifted_prog_thm),
+	      arch_pre, arch_post,
+	      get_bir_cont_pre bir_ct,
+	      get_bir_cont_post bir_ct] arch_lift_contract_thm;
+    (* Prove the arch triple by supplying the antecedents of lift_contract_thm *)
+    val arch_contract_thm = prove (
+      ``^arch_cont ^prog_bin ^init_addr ^end_addrs ^arch_pre ^arch_post``,
+
+    once_rewrite_tac (init_addr_def :: end_addr_defs) >>
+    irule add_lift_thm >>
+    REPEAT STRIP_TAC >| [
+      (* 1. Prove that the union of variables in the program and precondition are a well-founded variable
+       *    set *)
+      rewrite_tac [bir_prog_def] >>
+      CONV_TAC (bir_convLib.bir_vars_of_program_CONV) >>
+      rewrite_tac ([arch_wf_varset_def, arch_vars_def]@bir_pre_defs) >>
+      CONV_TAC (bir_convLib.bir_vars_of_exp_CONV) >>
+      CONV_TAC (
+        LAND_CONV (pred_setLib.UNION_CONV bir_convLib.bir_var_EQ_CONV) THENC
+        holba_convLib.SUBSET_CONV bir_convLib.bir_var_EQ_CONV
+      ),
+      (* 2. Starting address exists in program *)
+      rewrite_tac [bir_prog_def] >>
+      CONV_TAC (
+        bir_convLib.bir_labels_of_program_CONV THENC
+        RAND_CONV holba_convLib.LIST_TO_SET_CONV THENC
+        pred_setLib.IN_CONV bir_convLib.bir_label_EQ_CONV
+      ),
+
+      (* 3. Provide translation of the arch precondition to the BIR precondition *)
+      FULL_SIMP_TAC std_ss [bir_pre1_def, arch_pre_imp_bir_pre_thm],
+
+      (* 4. Provide translation of the arch postcondition to BIR postcondition *)
+      ASSUME_TAC (Q.ISPEC `{BL_Address (Imm64 ml') | ml' IN ^ls}` arch_post_imp_bir_post_thm) >>
+      FULL_SIMP_TAC std_ss bir_post_defs >>
+      FULL_SIMP_TAC (std_ss++pred_setLib.PRED_SET_ss) [bir_post_bir_to_arch_def] >>
+      FULL_SIMP_TAC std_ss [],
+
+      (* 5. Provide the lifter theorem of the program *)
+      FULL_SIMP_TAC std_ss [bir_is_lifted_prog_thm],
+
+      (* 6. Provide the BIR triple in the requisite format *)
+      ASSUME_TAC bir_ct >>
+      `{BL_Address (Imm64 ml') | ml' IN ^ls} = ^ls_set` suffices_by (
+              FULL_SIMP_TAC std_ss []
+      ) >>
+      FULL_SIMP_TAC (std_ss++pred_setLib.PRED_SET_ss) [pred_setTheory.EXTENSION] >>
+      METIS_TAC []
+    ]
+    );
+
+  in
+    arch_contract_thm
+  end;
+
   fun get_arm8_contract bir_ct prog_bin arm8_pre arm8_post bir_prog_def bir_pre_defs
     bir_pre1_def arm8_pre_imp_bir_pre_thm bir_post_defs
     arm8_post_imp_bir_post_thm bir_is_lifted_prog_thm =
@@ -128,18 +204,16 @@ open bir_inst_liftingHelpersLib;
     bir_pre_defs bir_pre1_def arm8_pre_imp_bir_pre_thm bir_post_defs
     arm8_post_imp_bir_post_thm bir_is_lifted_prog_thm;
 
-  fun get_arm8_contract_thm bir_ct progbin_def arm8_pre_def arm8_post_def bir_prog_def bir_pre_defs
+  fun get_arm8_contract_thm bir_ct init_addr_def end_addr_defs prog_bin_def
+    arm8_pre_def arm8_post_def bir_prog_def bir_pre_defs
     bir_pre1_def arm8_pre_imp_bir_pre_thm bir_post_defs
     arm8_post_imp_bir_post_thm bir_is_lifted_prog_thm =
-      let
-        val prog_bin = (fst o dest_eq o concl) progbin_def;
-        val arm8_pre = (fst o dest_comb o lhs o snd o strip_forall o concl) arm8_pre_def;
-        val arm8_post = (fst o dest_comb o lhs o snd o strip_forall o concl) arm8_post_def;
-      in
-        get_arm8_contract bir_ct prog_bin arm8_pre arm8_post bir_prog_def bir_pre_defs
-          bir_pre1_def arm8_pre_imp_bir_pre_thm bir_post_defs
-          arm8_post_imp_bir_post_thm bir_is_lifted_prog_thm
-      end;
+   get_arch_contract_thm ``arm8_cont`` arm8_lift_contract_thm
+    arm8_wf_varset_def arm8_vars_def bir_post_bir_to_arm8_def
+    bir_ct init_addr_def end_addr_defs prog_bin_def
+    arm8_pre_def arm8_post_def bir_prog_def
+    bir_pre_defs bir_pre1_def arm8_pre_imp_bir_pre_thm bir_post_defs
+    arm8_post_imp_bir_post_thm bir_is_lifted_prog_thm;
 
   fun get_riscv_contract bir_ct prog_bin riscv_pre riscv_post bir_prog_def bir_pre_defs
     bir_pre1_def riscv_pre_imp_bir_pre_thm bir_post_defs
@@ -150,18 +224,16 @@ open bir_inst_liftingHelpersLib;
     bir_pre_defs bir_pre1_def riscv_pre_imp_bir_pre_thm bir_post_defs
     riscv_post_imp_bir_post_thm bir_is_lifted_prog_thm;
 
-  fun get_riscv_contract_thm bir_ct progbin_def riscv_pre_def riscv_post_def bir_prog_def bir_pre_defs
+  fun get_riscv_contract_thm bir_ct init_addr_def end_addr_defs prog_bin_def
+    riscv_pre_def riscv_post_def bir_prog_def bir_pre_defs
     bir_pre1_def riscv_pre_imp_bir_pre_thm bir_post_defs
     riscv_post_imp_bir_post_thm bir_is_lifted_prog_thm =
-      let
-        val prog_bin = (fst o dest_eq o concl) progbin_def;
-        val riscv_pre = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_pre_def;
-        val riscv_post = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_post_def;
-      in
-        get_riscv_contract bir_ct prog_bin riscv_pre riscv_post bir_prog_def bir_pre_defs
-          bir_pre1_def riscv_pre_imp_bir_pre_thm bir_post_defs
-          riscv_post_imp_bir_post_thm bir_is_lifted_prog_thm
-      end;
+   get_arch_contract_thm ``riscv_cont`` riscv_lift_contract_thm
+    riscv_wf_varset_def riscv_vars_def bir_post_bir_to_riscv_def
+    bir_ct init_addr_def end_addr_defs prog_bin_def
+    riscv_pre_def riscv_post_def bir_prog_def
+    bir_pre_defs bir_pre1_def riscv_pre_imp_bir_pre_thm bir_post_defs
+    riscv_post_imp_bir_post_thm bir_is_lifted_prog_thm;
 
   end
 end