Preliminary XSA model

hol/p4_from_json/p4_arch_auxScript.sml

@@ -33,4 +33,10 @@ Definition v1model_add_ctrl_def:
   add_ctrl_gen astate
 End
 
+Definition xsa_add_ctrl_def:
+ xsa_add_ctrl (astate:xsa_ascope astate) =
+  add_ctrl_gen astate
+End
+
+
 val _ = export_theory ();

hol/p4_from_json/petr4_get_arch.sh

@@ -7,6 +7,9 @@ elif grep -q "#include \"very_simple_model.p4\"" "$1"; then
     echo "vss"
 elif grep -q "#include <v1model.p4>" "$1"; then
     echo "v1model"
+# TODO: Fix
+elif grep -q "#include <xsa.p4>" "$1"; then
+    echo "xsa"
 else
     echo "none"
 fi

hol/p4_from_json/petr4_to_hol4p4.sml

@@ -4,7 +4,7 @@ open PPBackEnd optionSyntax pairSyntax numSyntax listSyntax stringLib;
 open parse_jsonTheory;
 open petr4_to_hol4p4Theory p4_arch_auxTheory;
 
-open excluded petr4_to_hol4p4Syntax p4Syntax p4_vssLib p4_ebpfLib p4_v1modelLib;
+open excluded petr4_to_hol4p4Syntax p4Syntax p4_vssLib p4_ebpfLib p4_v1modelLib p4_xsaLib;
 
 (* For EVAL *)
 open ASCIInumbersLib;
@@ -18,6 +18,8 @@ fun parse_arch arch_str =
  then SOME ebpf
  else if arch_str = "v1model"
  then SOME v1model
+ else if arch_str = "xsa"
+ then SOME xsa
  else NONE
 ;
 
@@ -26,6 +28,7 @@ fun arch_to_term arch_opt =
    SOME vss => mk_some arch_vss_NONE_tm
  | SOME ebpf => mk_some arch_ebpf_NONE_tm
  | SOME v1model => mk_some arch_v1model_NONE_tm
+ | SOME xsa => mk_some arch_xsa_NONE_tm
  | NONE => mk_none ``:arch_t``
 ;
 
@@ -36,6 +39,8 @@ fun ascope_of_arch arch_opt_tm =
  then "``:ebpf_ascope``"
  else if is_arch_v1model $ dest_some arch_opt_tm
  then "``:v1model_ascope``"
+ else if is_arch_xsa $ dest_some arch_opt_tm
+ then "``:xsa_ascope``"
  else "``:'a``"
 ;
 
@@ -46,6 +51,8 @@ fun astr_of_arch arch_opt_tm =
  then "ebpf"
  else if is_arch_v1model $ dest_some arch_opt_tm
  then "v1model"
+ else if is_arch_xsa $ dest_some arch_opt_tm
+ then "xsa"
  else raise Fail ("Unknown architecture: "^(term_to_string arch_opt_tm))
 ;
 
@@ -57,6 +64,8 @@ fun astate_of_arch arch_opt_tm =
  then SOME "ebpf_ascope astate"
  else if is_arch_v1model $ dest_some arch_opt_tm
  then SOME "v1model_ascope astate"
+ else if is_arch_xsa $ dest_some arch_opt_tm
+ then SOME "xsa_ascope astate"
  else NONE
 ;
 
@@ -68,6 +77,8 @@ fun actx_of_arch arch_opt_tm =
  then SOME "ebpf_ascope actx"
  else if is_arch_v1model $ dest_some arch_opt_tm
  then SOME "v1model_ascope actx"
+ else if is_arch_xsa $ dest_some arch_opt_tm
+ then SOME "xsa_ascope actx"
  else NONE
 ;
 
@@ -639,6 +650,20 @@ fun v1model_add_ffblocks_to_ab_list ab_list_tm =
  end
 ;
 
+fun xsa_add_ffblocks_to_ab_list ab_list_tm =
+ let
+  val (ab_list, ab_list_ty) = dest_list ab_list_tm
+  val ab_list' = [``arch_block_inp``,
+                  (el 1 ab_list), (* TODO *)
+                  ``arch_block_ffbl "postparser"``,
+                  (el 2 ab_list), (* TODO *)
+                  (el 3 ab_list), (* TODO *)
+                  ``arch_block_out``]
+ in
+  (mk_list (ab_list', ab_list_ty))
+ end
+;
+
 fun vss_add_param_vars_to_v_map init_v_map tau =
  let
   val uninit_H_val_tm = eval_rhs “arb_from_tau ^tau”
@@ -794,6 +819,50 @@ fun output_hol4p4_vals outstream output_extra_maps valname stfname_opt (ftymap,
       end
      else raise Fail ("Could not initialise control plane configuration for "^valname)
     end
+
+   else if (is_arch_xsa $ dest_some arch_opt_tm) then
+    let
+     val fmap' = eval_rhs ``AUPDATE_LIST ^xsa_func_map ^fmap``
+     val tparams = eval_rhs “(\ (tau1, tau2). (arb_from_tau tau1, arb_from_tau tau2)) ^(mk_pair (dest_xsa_pkg_pipe $ dest_some $ dest_arch_xsa $ dest_some arch_opt_tm))”
+     val xsa_input_f = “xsa_input_f ^tparams”
+     val actx =
+      rhs $ concl $ SIMP_CONV list_ss [] $
+       list_mk_pair [xsa_add_ffblocks_to_ab_list ab_list_tm, pblock_map, xsa_ffblock_map,
+		     xsa_input_f, xsa_output_f,
+		     xsa_copyin_pbl, xsa_copyout_pbl, xsa_apply_table_f,
+		     xsa_ext_map, fmap']
+     val init_ctrl_opt = eval_rhs ``xsa_init_ctrl ^pblock_map ^tbl_updates_tm``;
+(*
+     val _ = print ("pblock_map :"^((term_to_string pblock_map)^"\n"))
+     val _ = print ("tbl_updates :"^((term_to_string tbl_updates_tm)^"\n"))
+*)
+    in
+     if is_some init_ctrl_opt
+     then
+      let
+       val init_ctrl = dest_some init_ctrl_opt
+       (* ctrl is initialised from the onset, whereas extern objects are initialised at the
+        * start of the pipeline with xsa_input_f *)
+       val ascope = list_mk_pair [xsa_init_counter,
+				  xsa_init_ext_obj_map,
+				  xsa_init_v_map,
+				  init_ctrl]
+       (* ab index, input list, output list, ascope *)
+       (* Note: Input is added later elsewhere *)
+       val aenv = list_mk_pair [term_of_int 0,
+				mk_list ([], ``:in_out``),
+				mk_list ([], ``:in_out``), ascope]
+       (* aenv, global scope, arch_frame_list, status *)
+       val astate = list_mk_pair [aenv,
+				  mk_list ([``^(gscope_init_vars):scope``], scope_ty),
+				  arch_frame_list_empty_tm,
+				  status_running_tm]
+      in
+       SOME (actx, astate)
+      end
+     else raise Fail ("Could not initialise control plane configuration for "^valname)
+    end
+
    else if (is_none arch_opt_tm) then
     (* TODO *)
     NONE

hol/p4_from_json/petr4_to_hol4p4Script.sml

@@ -265,12 +265,19 @@ Datatype:
   v1model_pkg_V1Switch tau tau
 End
 
+(* TODO: Fix name *)
+Datatype:
+ xsa_pkg_t =
+  xsa_pkg_pipe tau tau
+End
+
 (* The option type signifies whether the top-level package has been recognized yet *)
 Datatype:
  arch_t =
     arch_vss (vss_pkg_t option)
   | arch_ebpf (ebpf_pkg_t option)
   | arch_v1model (v1model_pkg_t option)
+  | arch_xsa (xsa_pkg_t option)
 End
 
 
@@ -3636,6 +3643,17 @@ Definition petr4_parse_element_def:
          | NONE => NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Invalid block in top-level package instantiation"))
        | SOME (arch_v1model _) =>
         NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Duplicate top-level package instantiations")
+       (* XSA: Only one top-level package exists *)
+       | SOME (arch_xsa NONE) =>
+        (case get_arch_block_pbl_name (EL 0 ab_list') of
+         | SOME pbl_name =>
+          (case ALOOKUP pblock_map pbl_name of
+           | SOME (pblock, argtys) =>
+            SOME_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, SOME (arch_xsa (SOME (xsa_pkg_pipe (EL 1 argtys) (EL 2 argtys)))), ab_list', action_list, extfun_list, ttymap)
+           | _ => NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Unknown programmable block in top-level package instantiation: "++pbl_name))
+         | NONE => NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Invalid block in top-level package instantiation"))
+       | SOME (arch_xsa _) =>
+        NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Duplicate top-level package instantiations")
 
        | _ => NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) ("Unexpected top-level package instantiation"))
      | NONE_msg msg => NONE_dbg (tyenv, enummap, vtymap, ftymap, blftymap, fmap, bltymap, ptymap, gscope, pblock_map, tbl_entries_map, arch_pkg_opt, ab_list, action_list, extfun_list, ttymap) msg)
@@ -3821,6 +3839,18 @@ Definition v1model_init_ctrl_def:
    init_ctrl_gen init_tbl_map' tbl_updates
 End
 
+Definition xsa_init_ctrl_def:
+ xsa_init_ctrl pblock_map tbl_updates =
+  let
+   init_tbl_map = (FLAT (MAP (\ (pblock_name, pblock). case pblock of
+                      | (pbl_type, params, b_func_map, decl_list, state_map, tbl_map) => ZIP ((MAP FST tbl_map), REPLICATE (LENGTH tbl_map) [])) pblock_map)):xsa_ctrl
+  in
+  let
+   init_tbl_map' = FILTER_DUPLICATES init_tbl_map
+  in
+   init_ctrl_gen init_tbl_map' tbl_updates
+End
+
 
 (* Replaces the default action of a table. Used when parsing STF specifications *)
 Definition p4_replace_tbl_default_def:

hol/p4_from_json/petr4_to_hol4p4Syntax.sml

@@ -13,6 +13,7 @@ val (SOME_msg_tm, mk_SOME_msg, dest_SOME_msg, is_SOME_msg) =
 val (NONE_msg_tm, mk_NONE_msg, dest_NONE_msg, is_NONE_msg) =
   syntax_fns1 "petr4_to_hol4p4" "NONE_msg";
 
+
 val (arch_vss_tm, mk_arch_vss, dest_arch_vss, is_arch_vss) =
   syntax_fns1 "petr4_to_hol4p4" "arch_vss";
 
@@ -21,6 +22,7 @@ val arch_vss_NONE_tm = mk_arch_vss $ mk_none ``:vss_pkg_t``;
 val (vss_pkg_VSS_tm, mk_vss_pkg_VSS, dest_vss_pkg_VSS, is_vss_pkg_VSS) =
   syntax_fns1 "petr4_to_hol4p4" "vss_pkg_VSS";
 
+
 val (arch_ebpf_tm, mk_arch_ebpf, dest_arch_ebpf, is_arch_ebpf) =
   syntax_fns1 "petr4_to_hol4p4" "arch_ebpf";
 
@@ -29,6 +31,7 @@ val arch_ebpf_NONE_tm = mk_arch_ebpf $ mk_none ``:ebpf_pkg_t``;
 val (ebpf_pkg_ebpfFilter_tm, mk_ebpf_pkg_ebpfFilter, dest_ebpf_pkg_ebpfFilter, is_ebpf_pkg_ebpfFilter) =
   syntax_fns1 "petr4_to_hol4p4" "ebpf_pkg_ebpfFilter";
 
+
 val (arch_v1model_tm, mk_arch_v1model, dest_arch_v1model, is_arch_v1model) =
   syntax_fns1 "petr4_to_hol4p4" "arch_v1model";
 
@@ -37,4 +40,13 @@ val arch_v1model_NONE_tm = mk_arch_v1model $ mk_none ``:v1model_pkg_t``;
 val (v1model_pkg_V1Switch_tm, mk_v1model_pkg_V1Switch, dest_v1model_pkg_V1Switch, is_v1model_pkg_V1Switch) =
   syntax_fns2 "petr4_to_hol4p4" "v1model_pkg_V1Switch";
 
+
+val (arch_xsa_tm, mk_arch_xsa, dest_arch_xsa, is_arch_xsa) =
+  syntax_fns1 "petr4_to_hol4p4" "arch_xsa";
+
+val arch_xsa_NONE_tm = mk_arch_xsa $ mk_none ``:xsa_pkg_t``;
+
+val (xsa_pkg_pipe_tm, mk_xsa_pkg_pipe, dest_xsa_pkg_pipe, is_xsa_pkg_pipe) =
+  syntax_fns2 "petr4_to_hol4p4" "xsa_pkg_pipe";
+
 end

hol/p4_xsaLib.sig

@@ -0,0 +1,30 @@
+signature p4_xsaLib =
+sig
+  include Abbrev
+
+val xsa_arch_ty : hol_type
+
+val xsa_init_global_scope : term
+val xsa_init_ext_obj_map : term
+val xsa_init_counter : term
+val xsa_init_v_map : term
+
+val xsa_packet_in_map : term
+val xsa_packet_out_map : term
+
+val xsa_input_f : term
+val xsa_output_f : term
+val xsa_is_drop_port : term
+
+val xsa_copyin_pbl : term
+val xsa_copyout_pbl : term
+
+val xsa_apply_table_f : term
+
+val xsa_ffblock_map : term
+val xsa_ext_map : term
+val xsa_func_map : term
+
+val dest_xsa_ascope : term -> term * term * term * term
+
+end

hol/p4_xsaLib.sml

@@ -0,0 +1,83 @@
+structure p4_xsaLib :> p4_xsaLib = struct
+
+open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+open listSyntax numSyntax pairSyntax;
+
+open p4Syntax p4_coreLib;
+
+open p4Theory p4_coreTheory p4_xsaTheory;
+
+val xsa_arch_ty = ``:xsa_ascope``;
+
+(* Architectural constants *)
+(* TODO: Nothing other than enumeration types? *)
+val xsa_init_global_scope = ``[]:scope``;
+
+val xsa_init_ext_obj_map = “[]:(num, xsa_sum_v_ext) alist”;
+
+val xsa_init_counter = rhs $ concl $ EVAL “LENGTH ^xsa_init_ext_obj_map”;
+
+val xsa_init_v_map = ``^core_init_v_map:(string, v) alist``;
+
+(*******************************************)
+(* Architectural context (generic externs) *)
+
+val xsa_objectless_map =
+ ``[("mark_to_drop", ([("standard_metadata", d_inout)], xsa_mark_to_drop));
+    ("verify", ([("condition", d_in); ("err", d_in)], xsa_verify))]``;
+
+val xsa_packet_in_map =
+ ``[("extract", ([("this", d_in); ("headerLvalue", d_out)], xsa_packet_in_extract));
+    ("lookahead", ([("this", d_in); ("targ1", d_in)], xsa_packet_in_lookahead));
+    ("advance", ([("this", d_in); ("bits", d_in)], xsa_packet_in_advance))]``;
+
+val xsa_packet_out_map =
+ ``[("emit", ([("this", d_in); ("data", d_in)], xsa_packet_out_emit))]``;
+
+(*************************)
+(* Architectural context *)
+
+(* Input function term *)
+val xsa_input_f = ``xsa_input_f``;
+
+(* Output function term *)
+val xsa_output_f = ``xsa_output_f``;
+val xsa_is_drop_port = ``xsa_is_drop_port``;
+
+(* Programmable block input function term *)
+val xsa_copyin_pbl = ``xsa_copyin_pbl``;
+
+(* Programmable block output function term *)
+val xsa_copyout_pbl = ``xsa_copyout_pbl``;
+
+(* Programmable block output function term *)
+val xsa_apply_table_f = ``xsa_apply_table_f``;
+
+(* Fixed-function block map *)
+val xsa_ffblock_map = ``[("postparser", ffblock_ff xsa_postparser)]``;
+
+(* Extern (object) function map *)
+val xsa_ext_map =
+ ``((^(inst [``:'a`` |-> xsa_arch_ty] core_ext_map))
+    ++ [("", (NONE, (^xsa_objectless_map)));
+        ("packet_in", (NONE, (^xsa_packet_in_map)));
+        ("packet_out", (NONE, (^xsa_packet_out_map)))])``;
+
+(* Function map *)
+val xsa_func_map = core_func_map;
+
+(*****************)
+(* Miscellaneous *)
+
+fun dest_xsa_ascope xsa_ascope =
+ let
+  val (ext_counter, xsa_ascope') = dest_pair xsa_ascope
+  val (ext_obj_map, xsa_ascope'') = dest_pair xsa_ascope'
+  val (v_map, ctrl) = dest_pair xsa_ascope''
+ in
+  (ext_counter, ext_obj_map, v_map, ctrl)
+ end
+;
+
+end