backlifting kernel_trap works

examples/riscv/kernel-trap/kernel_trap_entry_propScript.sml

@@ -30,7 +30,44 @@ open kernel_trapTheory;
 open kernel_trap_specTheory;
 open kernel_trap_entry_symb_transfTheory;
 
-val _ = new_theory "kernel_trap_prop";
+val _ = new_theory "kernel_trap_entry_prop";
+
+(* ------------------------------------- *)
+(* Connecting RISC-V and BSPEC contracts *)
+(* ------------------------------------- *)
+
+Theorem kernel_trap_entry_riscv_pre_imp_bspec_pre_thm:
+ bir_pre_riscv_to_bir
+  (riscv_kernel_trap_entry_pre pre_mscratch pre_mepc pre_mcause
+    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
+    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
+    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
+    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
+  (bspec_kernel_trap_entry_pre pre_mscratch pre_mepc pre_mcause
+    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
+    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
+    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
+    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
+Proof
+ cheat
+QED
+
+Theorem kernel_trap_entry_riscv_post_imp_bspec_post_thm:
+ !ls. bir_post_bir_to_riscv
+   (riscv_kernel_trap_entry_post pre_mscratch pre_mepc pre_mcause
+    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
+    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
+    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
+    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
+   (\l. (bspec_kernel_trap_entry_post pre_mscratch pre_mepc pre_mcause
+    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
+    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
+    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
+    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31))
+   ls
+Proof
+ cheat
+QED
 
 (* --------------------- *)
 (* Auxiliary definitions *)

examples/riscv/kernel-trap/kernel_trap_return_propScript.sml

@@ -0,0 +1,124 @@
+open HolKernel boolLib Parse bossLib;
+
+open markerTheory;
+
+open bir_programSyntax bir_program_labelsTheory;
+open bir_immTheory bir_valuesTheory bir_expTheory;
+open bir_tsTheory bir_bool_expTheory bir_programTheory;
+
+open bir_riscv_backlifterTheory;
+open bir_backlifterLib;
+open bir_compositionLib;
+
+open bir_lifting_machinesTheory;
+open bir_typing_expTheory;
+open bir_htTheory;
+
+open total_program_logicTheory;
+open total_ext_program_logicTheory;
+
+open jgmt_rel_bir_contTheory;
+
+open pred_setTheory;
+
+open program_logicSimps;
+
+open bir_env_oldTheory;
+open bir_program_varsTheory;
+
+open kernel_trapTheory;
+open kernel_trap_specTheory;
+open kernel_trap_return_symb_transfTheory;
+
+val _ = new_theory "kernel_trap_return_prop";
+
+(* ------------------------------------- *)
+(* Connecting RISC-V and BSPEC contracts *)
+(* ------------------------------------- *)
+
+Theorem kernel_trap_return_riscv_pre_imp_bspec_pre_thm:
+ bir_pre_riscv_to_bir
+  (riscv_kernel_trap_return_pre pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem)
+  (bspec_kernel_trap_return_pre pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem)
+Proof
+ cheat
+QED
+
+Theorem kernel_trap_return_riscv_post_imp_bspec_post_thm:
+ !ls. bir_post_bir_to_riscv
+   (riscv_kernel_trap_return_post pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem)
+   (\l. (bspec_kernel_trap_return_post pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem))
+   ls
+Proof
+ cheat
+QED
+
+(* --------------------- *)
+(* Auxiliary definitions *)
+(* --------------------- *)
+
+val progbin_tm = (fst o dest_eq o concl) bir_kernel_trap_progbin_def;
+val riscv_pre_tm = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_kernel_trap_return_pre_def;
+val riscv_post_tm = (fst o dest_comb o lhs o snd o strip_forall o concl) riscv_kernel_trap_return_post_def;
+
+(* ---------------------------------- *)
+(* Backlifting BIR contract to RISC-V *)
+(* ---------------------------------- *)
+
+val riscv_cont_kernel_trap_return_thm =
+ get_riscv_contract
+  bspec_cont_kernel_trap_return
+  progbin_tm riscv_pre_tm riscv_post_tm
+  bir_kernel_trap_prog_def
+  [bspec_kernel_trap_return_pre_def]
+  bspec_kernel_trap_return_pre_def kernel_trap_return_riscv_pre_imp_bspec_pre_thm
+  [bspec_kernel_trap_return_post_def] kernel_trap_return_riscv_post_imp_bspec_post_thm
+  bir_kernel_trap_riscv_lift_THM;
+
+Theorem riscv_cont_kernel_trap_return:
+ riscv_cont bir_kernel_trap_progbin kernel_trap_return_init_addr {kernel_trap_return_end_addr}
+ (riscv_kernel_trap_return_pre pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem)
+ (riscv_kernel_trap_return_post pre_mscratch pre_x10 pre_mepc_mem pre_x1_mem
+      pre_x2_mem pre_x3_mem pre_x4_mem pre_x5_mem pre_x6_mem pre_x7_mem
+      pre_x8_mem pre_x9_mem pre_x10_mem pre_x11_mem pre_x12_mem pre_x13_mem
+      pre_x14_mem pre_x15_mem pre_x16_mem pre_x17_mem pre_x18_mem pre_x19_mem
+      pre_x20_mem pre_x21_mem pre_x22_mem pre_x23_mem pre_x24_mem pre_x25_mem
+      pre_x26_mem pre_x27_mem pre_x28_mem pre_x29_mem pre_x30_mem pre_x31_mem)
+Proof
+ rw [kernel_trap_return_init_addr_def,kernel_trap_return_end_addr_def] >>
+ ACCEPT_TAC riscv_cont_kernel_trap_return_thm
+QED
+
+(* ------------------------ *)
+(* Unfolded RISC-V contract *)
+(* ------------------------ *)
+
+val readable_thm = computeLib.RESTR_EVAL_RULE [``riscv_weak_trs``] riscv_cont_kernel_trap_return;
+Theorem riscv_cont_kernel_trap_return_full = GEN_ALL readable_thm;
+
+val _ = export_theory ();

examples/riscv/kernel-trap/kernel_trap_specScript.sml

@@ -1408,41 +1408,4 @@ Definition bspec_kernel_trap_return_post_def:
  ^bspec_kernel_trap_return_post_tm
 End
 
-(* ------------------------------------- *)
-(* Connecting RISC-V and BSPEC contracts *)
-(* ------------------------------------- *)
-
-Theorem kernel_trap_entry_riscv_pre_imp_bspec_pre_thm:
- bir_pre_riscv_to_bir
-  (riscv_kernel_trap_entry_pre pre_mscratch pre_mepc pre_mcause
-    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
-    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
-    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
-    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
-  (bspec_kernel_trap_entry_pre pre_mscratch pre_mepc pre_mcause
-    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
-    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
-    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
-    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
-Proof
- cheat
-QED
-
-Theorem kernel_trap_entry_riscv_post_imp_bspec_post_thm:
- !ls. bir_post_bir_to_riscv
-   (riscv_kernel_trap_entry_post pre_mscratch pre_mepc pre_mcause
-    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
-    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
-    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
-    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31)
-   (\l. (bspec_kernel_trap_entry_post pre_mscratch pre_mepc pre_mcause
-    pre_mhartid pre_mtval pre_x1 pre_x2 pre_x3 pre_x4 pre_x5 pre_x6
-    pre_x7 pre_x8 pre_x9 pre_x10 pre_x11 pre_x12 pre_x13 pre_x14
-    pre_x15 pre_x16 pre_x17 pre_x18 pre_x19 pre_x20 pre_x21 pre_x22
-    pre_x23 pre_x24 pre_x25 pre_x26 pre_x27 pre_x28 pre_x29 pre_x30 pre_x31))
-   ls
-Proof
- cheat
-QED
-
 val _ = export_theory ();

src/theory/tools/backlifter/bir_riscv_backlifterScript.sml

@@ -244,7 +244,22 @@ Definition riscv_vars_def:
   (BVar "tmp_MEM8" (BType_Mem Bit64 Bit8));
 
   (BVar "tmp_PC" (BType_Imm Bit64));
-  (BVar "tmp_COND" (BType_Imm Bit1))
+  (BVar "tmp_COND" (BType_Imm Bit1));
+
+  (BVar "mhartid" (BType_Imm Bit64));
+  (BVar "tmp_mhartid" (BType_Imm Bit64));
+  (BVar "MPRV" (BType_Imm Bit8));
+  (BVar "tmp_MPRV" (BType_Imm Bit8));
+  (BVar "mscratch" (BType_Imm Bit64));
+  (BVar "tmp_mscratch" (BType_Imm Bit64));
+  (BVar "mepc" (BType_Imm Bit64));
+  (BVar "tmp_mepc" (BType_Imm Bit64));
+  (BVar "mcause" (BType_Imm Bit64));
+  (BVar "tmp_mcause" (BType_Imm Bit64));
+  (BVar "mtval" (BType_Imm Bit64));
+  (BVar "tmp_mtval" (BType_Imm Bit64));
+  (BVar "mip" (BType_Imm Bit64));
+  (BVar "tmp_mip" (BType_Imm Bit64))
  }
 End
 
@@ -1139,6 +1154,38 @@ Proof
       bir_immTheory.type_of_bool2b]
 QED
 
+Theorem default_riscv_bir_state_MCSRS_read_tmp[local]:
+ !ms.
+  bir_env_read (BVar "tmp_mhartid" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mhartid)) /\
+  bir_env_read (BVar "tmp_MPRV" (BType_Imm Bit8)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm8 (w2w (ms.c_MCSR ms.procID).mstatus.MPRV))) /\
+  bir_env_read (BVar "tmp_mscratch" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mscratch)) /\
+  bir_env_read (BVar "tmp_mepc" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mepc)) /\
+  bir_env_read (BVar "tmp_mcause" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 $ reg'mcause (ms.c_MCSR ms.procID).mcause)) /\
+  bir_env_read (BVar "tmp_mtval" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mtval)) /\
+  bir_env_read (BVar "tmp_mip" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 $ reg'mip  (ms.c_MCSR ms.procID).mip))
+Proof
+  rw [default_riscv_bir_state_def,
+      default_riscv_bir_env_CSRS_def,
+      default_riscv_bir_env_CSRS_tmp_def,
+      default_riscv_bir_env_GPRS_def,
+      default_riscv_bir_env_GPRS_tmp_def,
+      default_riscv_bir_env_FPRS_def,
+      bir_envTheory.bir_env_read_UPDATE,
+      bir_envTheory.bir_var_name_def,
+      bir_envTheory.bir_env_lookup_UPDATE,
+      bir_envTheory.bir_var_type_def,
+      bir_valuesTheory.type_of_bir_val_def,
+      type_of_bir_imm_def,
+      bir_immTheory.type_of_bool2b]
+QED
+
 Theorem default_riscv_bir_state_MCSRS_lookup_type[local]:
   !ms.
   bir_env_lookup_type "mhartid" (default_riscv_bir_state ms).bst_environ =
@@ -1267,6 +1314,7 @@ FULL_SIMP_TAC std_ss [bir_lifting_machinesTheory.riscv_bmr_rel_EVAL,
  bir_env_oldTheory.bir_env_var_is_declared_def,bir_envTheory.bir_var_name_def] >>
 fs [
   default_riscv_bir_state_MCSRS_read,
+  default_riscv_bir_state_MCSRS_read_tmp,
   default_riscv_bir_state_MCSRS_lookup_type,
   default_riscv_bir_state_MCSRS_lookup_type_tmp,
   default_riscv_bir_state_GPRS_read,