Fix (untested)

kth-step · Oct 19, 2024 · bfcde33 · bfcde33
1 parent 087eb8a
commit bfcde33
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 25 deletions.
diff --git a/examples/riscv/chacha/chacha_symb_exec_ivsetupScript.sml b/examples/riscv/chacha/chacha_symb_exec_ivsetupScript.sml
@@ -18,16 +18,12 @@ val _ = show_tags := true;
 (* ivsetup *)
 (* ------- *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_chacha_prog_def
   chacha_ivsetup_init_addr_def [chacha_ivsetup_end_addr_def]
   bspec_chacha_ivsetup_pre_def chacha_birenvtyl_def;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
-
-Theorem chacha_ivsetup_bsysprecond_thm = bsysprecond_thm
-
 val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem chacha_ivsetup_symb_analysis_thm = symb_analysis_thm

diff --git a/examples/riscv/chacha/chacha_symb_exec_keysetupScript.sml b/examples/riscv/chacha/chacha_symb_exec_keysetupScript.sml
@@ -18,16 +18,12 @@ val _ = show_tags := true;
 (* keysetup *)
 (* -------- *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_chacha_prog_def
   chacha_keysetup_init_addr_def [chacha_keysetup_end_addr_def]
   bspec_chacha_keysetup_pre_def chacha_birenvtyl_def;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
-
-Theorem chacha_keysetup_bsysprecond_thm = bsysprecond_thm
-
 val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem chacha_keysetup_symb_analysis_thm = symb_analysis_thm

diff --git a/examples/riscv/ifelse/ifelse_symb_execScript.sml b/examples/riscv/ifelse/ifelse_symb_execScript.sml
@@ -14,16 +14,12 @@ val _ = new_theory "ifelse_symb_exec";
 
 val _ = show_tags := true;
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_ifelse_prog_def
   ifelse_init_addr_def [ifelse_end_addr_def]
   bspec_ifelse_pre_def ifelse_birenvtyl_def;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
-
-Theorem ifelse_bsysprecond_thm = bsysprecond_thm
-
 val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem ifelse_symb_analysis_thm = symb_analysis_thm

diff --git a/examples/riscv/poly1305-inlined/poly1305_symb_execScript.sml b/examples/riscv/poly1305-inlined/poly1305_symb_execScript.sml
@@ -18,16 +18,12 @@ val _ = show_tags := true;
 (* init *)
 (* ------ *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_poly1305_prog_def
   poly1305_init_init_addr_def [poly1305_init_end_addr_def]
   bspec_poly1305_init_pre_def poly1305_birenvtyl_def;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
-
-Theorem poly1305_init_bsysprecond_thm = bsysprecond_thm
-
 val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem poly1305_init_symb_analysis_thm = symb_analysis_thm

diff --git a/examples/riscv/poly1305/poly1305_symb_execScript.sml b/examples/riscv/poly1305/poly1305_symb_execScript.sml
@@ -18,16 +18,12 @@ val _ = show_tags := true;
 (* U8TO32 *)
 (* ------ *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val 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