proof of postcondition for whole quarter round

examples/riscv/chacha/chacha_specScript.sml

@@ -4,6 +4,8 @@ open markerTheory;
 
 open wordsTheory;
 
+open pairTheory;
+
 open bir_programSyntax bir_program_labelsTheory;
 open bir_immTheory bir_valuesTheory bir_expTheory;
 open bir_tsTheory bir_bool_expTheory bir_programTheory;
@@ -674,6 +676,73 @@ Definition bspec_chacha_quarter_round_pre_def:
   ^bspec_chacha_quarter_round_pre_tm
 End
 
+Definition bspec_chacha_line_bir_exp_fst_def:
+ bspec_chacha_line_bir_exp_fst pre_a_exp pre_b_exp : bir_exp_t =
+  BExp_BinExp BIExp_Plus pre_a_exp pre_b_exp
+End
+
+Definition bspec_chacha_line_bir_exp_snd_def:
+ bspec_chacha_line_bir_exp_snd pre_a_exp pre_d_exp (s:word32) : bir_exp_t =
+   BExp_BinExp BIExp_Or
+     (BExp_BinExp BIExp_LeftShift 
+      (BExp_BinExp BIExp_Xor pre_a_exp pre_d_exp)
+     (BExp_Const (Imm32 s)))
+     (BExp_BinExp BIExp_RightShift
+      (BExp_BinExp BIExp_Xor pre_a_exp pre_d_exp)
+      (BExp_Const (Imm32 (32w-s))))
+End
+
+Definition bspec_chacha_quarter_round_bir_exprs_def:
+ bspec_chacha_quarter_round_bir_exprs pre_a_exp pre_b_exp pre_c_exp pre_d_exp
+  : bir_exp_t # bir_exp_t # bir_exp_t # bir_exp_t =
+  let a = pre_a_exp in
+  let b = pre_b_exp in
+  let c = pre_c_exp in
+  let d = pre_d_exp in
+
+  let a = bspec_chacha_line_bir_exp_fst a b in
+  let d = bspec_chacha_line_bir_exp_snd a d 16w in
+
+  let c = bspec_chacha_line_bir_exp_fst c d in
+  let b = bspec_chacha_line_bir_exp_snd c b 12w in
+
+  let a = bspec_chacha_line_bir_exp_fst a b in
+  let d = bspec_chacha_line_bir_exp_snd a d 8w in
+
+  let c = bspec_chacha_line_bir_exp_fst c d in
+  let b = bspec_chacha_line_bir_exp_snd c b 7w in
+
+  (a,b,c,d)
+End
+
+val bspec_chacha_quarter_round_post_tm =
+ let
+   val bir_exprs = (snd o dest_eq o concl)
+    (EVAL ``bspec_chacha_quarter_round_bir_exprs 
+     (BExp_Const (Imm32 pre_a)) (BExp_Const (Imm32 pre_b))
+     (BExp_Const (Imm32 pre_c)) (BExp_Const (Imm32 pre_d))``);
+   val (a_exp, bir_exprs) = dest_pair bir_exprs;
+   val (b_exp, bir_exprs) = dest_pair bir_exprs;
+   val (c_exp, d_exp) = dest_pair bir_exprs;
+ in
+   bslSyntax.bandl [
+    (snd o dest_eq o concl)
+     (EVAL ``bspec_var_equal_32_lowcast_64 "x20" ^a_exp``),
+    (snd o dest_eq o concl)
+     (EVAL ``bspec_var_equal_32_lowcast_64 "x21" ^b_exp``),
+    (snd o dest_eq o concl)
+     (EVAL ``bspec_var_equal_32_lowcast_64 "x8" ^c_exp``),
+    (snd o dest_eq o concl)
+     (EVAL ``bspec_var_equal_32_lowcast_64 "x22" ^d_exp``)
+   ]
+ end;
+
+Definition bspec_chacha_quarter_round_post_def:
+ bspec_chacha_quarter_round_post (pre_a:word32) (pre_b:word32)
+  (pre_c:word32) (pre_d:word32) : bir_exp_t =
+  ^bspec_chacha_quarter_round_post_tm
+End
+
 (* ----- *)
 
 Definition bspec_chacha_line_exp_1_imm32:

examples/riscv/chacha/chacha_symb_transf_quarterroundScript.sml

@@ -16,6 +16,8 @@ val _ = new_theory "chacha_symb_transf_quarterround";
 (* BIR symbolic execution analysis *)
 (* ------------------------------- *)
 
+(* first line *)
+
 val bspec_cont_thm =
  bir_symb_transfer_thm
   bir_chacha_prog_def
@@ -66,4 +68,30 @@ Proof
  rw [bspec_cont_thm]
 QED
 
+(* first quarter round *)
+
+val bspec_cont_thm =
+ bir_symb_transfer_thm
+  bir_chacha_prog_def
+  chacha_quarter_round_init_addr_def chacha_quarter_round_end_addr_def
+  bspec_chacha_quarter_round_pre_def bspec_chacha_quarter_round_post_def
+  chacha_birenvtyl_def chacha_prog_vars_list_def
+  chacha_quarter_round_symb_analysis_thm NONE chacha_prog_vars_thm;
+
+val init_addr_tm = (snd o dest_eq o concl) chacha_quarter_round_init_addr_def;
+val end_addr_tm = (snd o dest_eq o concl) chacha_quarter_round_end_addr_def;
+val bspec_pre_tm = (lhs o snd o strip_forall o concl) bspec_chacha_quarter_round_pre_def;
+val bspec_post_tm = (lhs o snd o strip_forall o concl) bspec_chacha_quarter_round_post_def;
+
+Theorem bspec_cont_chacha_quarter_round:
+ bir_cont bir_chacha_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 [bspec_cont_thm]
+QED
+
 val _ = export_theory ();