work on chacha spec

kth-step · Nov 25, 2024 · 9738430 · 9738430
1 parent 66065ab
commit 9738430
Show file tree

Hide file tree

Showing 3 changed files with 122 additions and 3 deletions.
diff --git a/examples/riscv/chacha/chacha_specScript.sml b/examples/riscv/chacha/chacha_specScript.sml
@@ -309,6 +309,16 @@ Definition chacha_quarterround_end_addr_def:
  chacha_quarterround_end_addr : word64 = 0x108b4w
 End
 
+(* second quarterround *)
+
+Definition chacha_other_quarterround_init_addr_def:
+  chacha_other_quarterround_init_addr : word64 = 0x108b4w
+End
+
+Definition chacha_other_quarterround_end_addr_def:
+ chacha_other_quarterround_end_addr : word64 = 0x108c8w
+End
+
 (* --------------- *)
 (* BSPEC contracts *)
 (* --------------- *)
@@ -428,12 +438,16 @@ val bspec_chacha_quarterround_pre_other_tm = bslSyntax.bandl [
   ``BExp_BinPred
     BIExp_Equal
     (BExp_Den (BVar "x22" (BType_Imm Bit64)))
-    (BExp_Const (Imm64 pre_x22))``  
+    (BExp_Const (Imm64 pre_x22))``,
+  ``BExp_BinPred
+    BIExp_Equal
+    (BExp_Den (BVar "x28" (BType_Imm Bit64)))
+    (BExp_Const (Imm64 pre_x28))``  
 ];
 
 Definition bspec_chacha_quarterround_pre_other_def:
  bspec_chacha_quarterround_pre_other (pre_x8:word64) (pre_x10:word64) 
-  (pre_x15:word64) (pre_x22:word64) : bir_exp_t =
+  (pre_x15:word64) (pre_x22:word64) (pre_x28:word64) : bir_exp_t =
   ^bspec_chacha_quarterround_pre_other_tm
 End
 
@@ -483,7 +497,8 @@ End
 (* (snd o dest_eq o concl) (EVAL ``bspec_chacha_quarterround_exp_2 "x10" pre_x10 pre_x22 pre_x26 (16w:word32)``) *)
 
 val bspec_chacha_quarterround_post_tm = bslSyntax.bandl [
-  (snd o dest_eq o concl) (EVAL ``bspec_chacha_quarterround_exp_1 "x20" pre_x10 pre_x22``),
+  (snd o dest_eq o concl)
+   (EVAL ``bspec_chacha_quarterround_exp_1 "x20" pre_x10 pre_x22``),
   (snd o dest_eq o concl)
    (EVAL ``bspec_chacha_quarterround_exp_2 "x10" pre_x10 pre_x22 pre_x26 (16w:word32)``)
 ];
@@ -495,4 +510,72 @@ Definition bspec_chacha_quarterround_post_def:
   ^bspec_chacha_quarterround_post_tm
 End
 
+(*
+        <|bb_label :=
+            BL_Address_HC (Imm64 0x108B4w) "01C5043B (addw s0,a0,t3)";
+          bb_statements :=
+            [BStmt_Assign (BVar "x8" (BType_Imm Bit64))
+               (BExp_Cast BIExp_SignedCast
+                  (BExp_Cast BIExp_LowCast
+                     (BExp_BinExp BIExp_Plus
+                        (BExp_Den (BVar "x28" (BType_Imm Bit64)))
+                        (BExp_Den (BVar "x10" (BType_Imm Bit64)))) Bit32)
+                  Bit64)];
+          bb_last_statement :=
+            BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x108B8w)))|>;
+        <|bb_label :=
+            BL_Address_HC (Imm64 0x108B8w) "008B4B33 (xor s6,s6,s0)";
+          bb_statements :=
+            [BStmt_Assign (BVar "x22" (BType_Imm Bit64))
+               (BExp_BinExp BIExp_Xor
+                  (BExp_Den (BVar "x8" (BType_Imm Bit64)))
+                  (BExp_Den (BVar "x22" (BType_Imm Bit64))))];
+          bb_last_statement :=
+            BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x108BCw)))|>;
+        <|bb_label :=
+            BL_Address_HC (Imm64 0x108BCw) "00CB179B (slliw a5,s6,0xc)";
+          bb_statements :=
+            [BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+               (BExp_Cast BIExp_SignedCast
+                  (BExp_BinExp BIExp_LeftShift
+                     (BExp_Cast BIExp_LowCast
+                        (BExp_Den (BVar "x22" (BType_Imm Bit64))) Bit32)
+                     (BExp_Const (Imm32 12w))) Bit64)];
+          bb_last_statement :=
+            BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x108C0w)))|>;
+        <|bb_label :=
+            BL_Address_HC (Imm64 0x108C0w) "014B5B1B (srliw s6,s6,0x14)";
+          bb_statements :=
+            [BStmt_Assign (BVar "x22" (BType_Imm Bit64))
+               (BExp_Cast BIExp_SignedCast
+                  (BExp_BinExp BIExp_RightShift
+                     (BExp_Cast BIExp_LowCast
+                        (BExp_Den (BVar "x22" (BType_Imm Bit64))) Bit32)
+                     (BExp_Const (Imm32 20w))) Bit64)];
+          bb_last_statement :=
+            BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x108C4w)))|>;
+        <|bb_label := BL_Address_HC (Imm64 0x108C4w) "0167E7B3 (or a5,a5,s6)";
+          bb_statements :=
+            [BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+               (BExp_BinExp BIExp_Or
+                  (BExp_Den (BVar "x15" (BType_Imm Bit64)))
+                  (BExp_Den (BVar "x22" (BType_Imm Bit64))))];
+          bb_last_statement :=
+            BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x108C8w)))|>;
+*)
+
+val bspec_chacha_quarterround_post_other_tm = bslSyntax.bandl [
+  (snd o dest_eq o concl)
+   (EVAL ``bspec_chacha_quarterround_exp_1 "x8" pre_x28 pre_x10``),
+  (snd o dest_eq o concl)
+   (EVAL ``bspec_chacha_quarterround_exp_2 "x15" pre_x15 pre_x10 pre_x22 (12w:word32)``)
+];
+
+Definition bspec_chacha_quarterround_post_other_def:
+ bspec_chacha_quarterround_post_other (pre_x8:word64)
+  (pre_x10:word64) (pre_x15:word64) (pre_x22:word64) (pre_x28:word64)
+  : bir_exp_t =
+  ^bspec_chacha_quarterround_post_other_tm
+End
+
 val _ = export_theory ();
diff --git a/examples/riscv/chacha/chacha_symb_exec_quarterroundScript.sml b/examples/riscv/chacha/chacha_symb_exec_quarterroundScript.sml
@@ -97,4 +97,14 @@ val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem chacha_quarterround_symb_analysis_thm = symb_analysis_thm
 
+val symb_analysis_thm =
+ bir_symb_analysis_thm
+  bir_chacha_prog_def
+  chacha_other_quarterround_init_addr_def [chacha_other_quarterround_end_addr_def]
+  bspec_chacha_quarterround_pre_other_def chacha_birenvtyl_def;
+
+val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
+
+Theorem chacha_other_quarterround_symb_analysis_thm = symb_analysis_thm
+
 val _ = export_theory ();
diff --git a/examples/riscv/chacha/chacha_symb_transf_quarterroundScript.sml b/examples/riscv/chacha/chacha_symb_transf_quarterroundScript.sml
@@ -40,4 +40,30 @@ Proof
  rw [bspec_cont_thm]
 QED
 
+(* second quarterround *)
+
+val bspec_cont_thm =
+ bir_symb_transfer_thm
+  bir_chacha_prog_def
+  chacha_other_quarterround_init_addr_def chacha_other_quarterround_end_addr_def
+  bspec_chacha_quarterround_pre_other_def bspec_chacha_quarterround_post_other_def
+  chacha_birenvtyl_def chacha_prog_vars_list_def
+  chacha_other_quarterround_symb_analysis_thm NONE chacha_prog_vars_thm;
+
+val init_addr_tm = (snd o dest_eq o concl) chacha_other_quarterround_init_addr_def;
+val end_addr_tm = (snd o dest_eq o concl) chacha_other_quarterround_end_addr_def;
+val bspec_pre_tm = (lhs o snd o strip_forall o concl) bspec_chacha_quarterround_pre_other_def;
+val bspec_post_tm = (lhs o snd o strip_forall o concl) bspec_chacha_quarterround_post_other_def;
+
+Theorem bspec_cont_chacha_other_quarterround:
+ 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 ();