Optimize simpl_assertion

[QinshiWang]

simpl_assertion is a tactic used to automatically unfold and evaluate Coq functions defined by Verifiable P4 that manipulate the assertions, including read/write, member accessing, local variable and extern predicate filtering, etc. For example, a predicate generated after applying a program logic rule looks like

clear_window, clear_index_1, hash_index_1, hash_index_2,
hash_index_3, api_1, api_2, api_3, api_4 : Sval
-----------
(MEM
     (eval_write_var
        (eval_write_vars
           [(["ds_md"],
            ValBaseStruct
              [("win_1",
               ValBaseStruct
                 [("api", P4Bit_ 8); ("index_1", P4Bit_ index_w);
                 ("index_2", P4Bit_ index_w);
                 ("index_3", P4Bit_ index_w); 
                 ("rw_1", P4Bit_ 8); ("rw_2", P4Bit_ 8);
                 ("rw_3", P4Bit_ 8)])])]
           (filter_in
              [(["act_set_clear_win_1"; "api_1"], Typed.In);
              (["act_set_clear_win_1"; "api_2"], Typed.In);
              (["act_set_clear_win_1"; "api_3"], Typed.In);
              (["act_set_clear_win_1"; "api_4"], Typed.In)])
           [api_1; api_2; api_3; api_4]) ["ds_md"]
        (update
           (str {| P4String.tags := NoInfo; str := "win_1" |})
           (update
              (str {| P4String.tags := NoInfo; str := "index_1" |})
              (get
                 (str
                    {|
                      P4String.tags := NoInfo;
                      str := "clear_index_1"
                    |})
                 (ValBaseStruct
                    [("win_1",
                     ValBaseStruct
                       [("api", P4Bit_ 8);
                       ("index_1", P4Bit_ index_w);
                       ("index_2", P4Bit_ index_w);
                       ("index_3", P4Bit_ index_w);
                       ("rw_1", P4Bit_ 8); 
                       ("rw_2", P4Bit_ 8); 
                       ("rw_3", P4Bit_ 8)])]))
              (get
                 (str
                    {| P4String.tags := NoInfo; str := "win_1" |})
                 (ValBaseStruct
                    [("win_1",
                     ValBaseStruct
                       [("api", P4Bit_ 8);
                       ("index_1", P4Bit_ index_w);
                       ("index_2", P4Bit_ index_w);
                       ("index_3", P4Bit_ index_w);
                       ("rw_1", P4Bit_ 8); 
                       ("rw_2", P4Bit_ 8); 
                       ("rw_3", P4Bit_ 8)])])))
           (ValBaseStruct
              [("win_1",
               ValBaseStruct
                 [("api", P4Bit_ 8); ("index_1", P4Bit_ index_w);
                 ("index_2", P4Bit_ index_w);
                 ("index_3", P4Bit_ index_w); 
                 ("rw_1", P4Bit_ 8); ("rw_2", P4Bit_ 8);
                 ("rw_3", P4Bit_ 8)])]))) (EXT []))

In this assertion, functions like eval_write_var, filter_in, update, get, str are defined to process programs and assertions. After running simpl_assertion, it is simplified to

(MEM
     [(["ds_md"],
      ValBaseStruct
        [("win_1",
         ValBaseStruct
           [("api", P4Bit_ 8); ("index_1", ValBaseNull);
           ("index_2", P4Bit_ index_w);
           ("index_3", P4Bit_ index_w); ("rw_1", P4Bit_ 8);
           ("rw_2", P4Bit_ 8); ("rw_3", P4Bit_ 8)])]);
     (["act_set_clear_win_1"; "api_1"], api_1);
     (["act_set_clear_win_1"; "api_2"], api_2);
     (["act_set_clear_win_1"; "api_3"], api_3);
     (["act_set_clear_win_1"; "api_4"], api_4)] 
     (EXT []))

The current implementation of simpl_assertion is

Ltac simpl_assertion :=
  cbn [
    (* First, most basic definitions for comparison. *)
    bool_rect bool_rec Bool.bool_dec Ascii.ascii_rect Ascii.ascii_rec Ascii.ascii_dec sumbool_rect
    sumbool_rec string_rect string_rec string_dec EquivUtil.StringEqDec EquivDec.equiv_dec EquivDec.list_eqdec
    in_dec path_eq_dec list_eq_dec Datatypes.list_rec list_rect negb is_left id

    is_some isSome

    P4String.str

    app find find

    fst snd force map lift_option

    lift_option_kv kv_map option_map List.filter

    AList.set AList.set_some AList.get

    filter_in Semantics.is_in flat_map

    eval_write_vars fold_left eval_write_var AList.set_some combine

    Members.update Members.get

    exclude

    ext_exclude eq_rect Result.Result.forallb Result.Result.andb].

The main problem is that cbn is not a straightforward evaluation tactic, so it is much slower than cbv to perform the same computation. But we cannot use cbv in this case, because cbv also tries beta-reduction in the inner terms. In the above example, simpl_assertion takes 0.229s.