basic symbolic execution for poly1305 U8TO32 subroutine

examples/riscv/poly1305/poly1305_specScript.sml

@@ -0,0 +1,72 @@
+open HolKernel boolLib Parse bossLib;
+
+open markerTheory;
+
+open wordsTheory;
+
+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 bir_predLib;
+open bir_smtLib;
+
+open bir_symbTheory birs_auxTheory;
+open HolBACoreSimps;
+open bir_program_transfTheory;
+
+open total_program_logicTheory;
+open total_ext_program_logicTheory;
+open symb_prop_transferTheory;
+
+open jgmt_rel_bir_contTheory;
+
+open pred_setTheory;
+
+open program_logicSimps;
+
+open bir_env_oldTheory;
+open bir_program_varsTheory;
+
+val _ = new_theory "poly1305_spec";
+
+(* ---------------- *)
+(* Block boundaries *)
+(* ---------------- *)
+
+(* U8TO32 *)
+
+Definition poly1305_u8to32_init_addr_def:
+ poly1305_u8to32_init_addr : word64 = 0x10488w
+End
+
+Definition poly1305_u8to32_end_addr_def:
+ poly1305_u8to32_end_addr : word64 = 0x104b4w
+End
+
+(* --------------- *)
+(* BSPEC contracts *)
+(* --------------- *)
+
+val bspec_poly1305_u8to32_pre_tm = bslSyntax.bandl [
+  mem_addrs_aligned_prog_disj_bir_tm mem_params_standard "x10",
+  ``BExp_BinPred
+    BIExp_Equal
+    (BExp_Den (BVar "x15" (BType_Imm Bit64)))
+    (BExp_Const (Imm64 pre_x15))``
+];
+
+Definition bspec_poly1305_u8to32_pre_def:
+ bspec_poly1305_u8to32_pre (pre_x15:word64) : bir_exp_t =
+  ^bspec_poly1305_u8to32_pre_tm
+End
+
+val _ = export_theory ();

examples/riscv/poly1305/poly1305_symb_execScript.sml

@@ -0,0 +1,35 @@
+open HolKernel Parse boolLib bossLib;
+
+open wordsTheory;
+
+open bir_symbLib;
+
+open poly1305Theory poly1305_specTheory;
+
+val _ = new_theory "poly1305_symb_exec";
+
+(* --------------------------- *)
+(* Symbolic analysis execution *)
+(* --------------------------- *)
+
+val _ = show_tags := true;
+
+(* ------ *)
+(* U8TO32 *)
+(* ------ *)
+
+val (bsysprecond_thm, symb_analysis_thm) =
+ bir_symb_analysis_thm
+  bir_poly1305_prog_def
+  poly1305_u8to32_init_addr_def [poly1305_u8to32_end_addr_def]
+  bspec_poly1305_u8to32_pre_def poly1305_birenvtyl_def;
+
+val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
+
+Theorem poly1305_u8to32_bsysprecond_thm = bsysprecond_thm
+
+val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
+
+Theorem poly1305_u8to32_symb_analysis_thm = symb_analysis_thm
+
+val _ = export_theory ();