CakeML-exportable architectural functions for VSS, updates to VSS arc…

…hitecture
kth-step · Dec 19, 2024 · 9c5edb9 · 9c5edb9
1 parent 806c191
commit 9c5edb9
Show file tree

Hide file tree

Showing 14 changed files with 1,193 additions and 184 deletions.
diff --git a/hol/cake_export/Holmakefile b/hol/cake_export/Holmakefile
@@ -1,7 +1,7 @@
 # includes
 # ----------------------------------
 
-CAKEMLDIR = #Your CakeML installation here
+CAKEMLDIR = ../../../../../installed-git-repos/cakeml
 
 DEPENDENCIES   = .. \
  $(CAKEMLDIR)/misc \

diff --git a/...rt/p4_exec_sem_wrapper_cakeProgScript.sml → ..._export/p4_conditional_cakeProgScript.sml b/...rt/p4_exec_sem_wrapper_cakeProgScript.sml → ..._export/p4_conditional_cakeProgScript.sml
@@ -1,6 +1,6 @@
 open HolKernel boolLib Parse bossLib;
 
-val _ = new_theory "p4_exec_sem_wrapper_cakeProg";
+val _ = new_theory "p4_conditional_cakeProg";
 
 open p4Syntax;
 open bitstringSyntax numSyntax;
@@ -18,7 +18,7 @@ open p4_exec_sem_v1model_cakeProgTheory;
 open fromSexpTheory;
 
 intLib.deprecate_int();
-val _ = (max_print_depth := 100);
+val _ = (max_print_depth := 1000);
 
 val _ = translation_extends "p4_exec_sem_v1model_cakeProg";
 
@@ -282,6 +282,6 @@ val prog =
     ^(get_ml_prog_state() |> get_prog)”
   |> EVAL |> concl |> rhs;
 
-val _ = astToSexprLib.write_ast_to_file "test3.sexp" prog;
+val _ = astToSexprLib.write_ast_to_file "conditional_test.sexp" prog;
 
 val _ = export_theory ();
diff --git a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml
@@ -200,6 +200,7 @@ Definition v1model_packet_in_extract'_def:
   (varn # p4$v # lval option) list list # status) option) = v1model_packet_in_extract_gen v1model_ascope_lookup v1model_ascope_update v1model_ascope_update_v_map
 End
 
+(* TODO: Move to p4_exec_sem_arch_cakeProg, since it's not architecture-specific *)
 (* TODO: Note that this does not distinguish failing from finishing *)
 Definition arch_multi_exec'_def:
  (arch_multi_exec' actx ((aenv, g_scope_list, arch_frame_list, status):'a astate) 0 =