restore ASN.1 proofs

EverParse.fst.config.json

@@ -1,16 +1,19 @@
 {
     "fstar_exe": "fstar.exe",
     "options": [
-      "--max_fuel", "0",
+      "--initial_fuel", "0",
+      "--max_fuel", "2",
+      "--initial_ifuel", "2",
       "--max_ifuel", "2",
       "--initial_ifuel", "2"
     ],
     "include_dirs": [
-      "./src/lowparse", 
+      "./src/lowparse",
       "${KRML_HOME}/krmllib",
       "${KRML_HOME}/krmllib/obj",
       "./src/3d",
-      "./src/3d/prelude"
+      "./src/3d/prelude",
+      "./src/ASN1"
     ]
   }
 

src/ASN1/ASN1.Base.fst

@@ -1,5 +1,4 @@
 module ASN1.Base
-
 open LowParse.Tot.Base
 open LowParse.Tot.Combinators
 
@@ -60,11 +59,19 @@ type asn1_boolean_t = bool
 
 type asn1_integer_t (bound : pos) = integer_in_interval bound
 
+let rec pow2_mono (n m:nat)
+: Lemma
+  (requires n < m)
+  (ensures pow2 n < pow2 m)
+= if n + 1 = m then () else pow2_mono n (m - 1)
+let pow2_le (n:nat {n < 8}) : Lemma (pow2 n < 256) = pow2_mono n 8
+
 //Bitstring is represented as an array of bytes and 0~7 unused bits
 type asn1_bitstring_t = 
 | BYTES_WITH_UNUSEDBITS :
   unused : U8.t {0 <= (U8.v unused) /\ (U8.v unused) <= 7} ->
-  b : B.bytes {(U8.v unused = 0) \/ 
+  b : B.bytes {let _ = pow2_le (U8.v unused) in
+               (U8.v unused = 0) \/ 
                ((U8.v unused > 0) /\ B.length b > 0 /\ 
                 FStar.UInt.mod (U8.v (B.index b ((B.length b) - 1))) (pow2 (U8.v unused)) = 0)} -> asn1_bitstring_t
 //TODO: use bit op
@@ -309,9 +316,9 @@ let idlookup_with_fallback_t (#key : eqtype) (id : key) (lc : list (key & Type))
     let _ = List.assoc_memP_none id lc in
     fb
 
-let make_gen_choice_type (#key : eqtype) (lc : list (key & Type)) = (id : key) & (idlookup_t id lc)
+let make_gen_choice_type (#key : eqtype) (lc : list (key & Type)) = id : key & idlookup_t id lc
 
-let make_gen_choice_type_with_fallback (#key : eqtype) (lc : list (key & Type)) (fb : Type) = (id : key) & (idlookup_with_fallback_t id lc fb)
+let make_gen_choice_type_with_fallback (#key : eqtype) (lc : list (key & Type)) (fb : Type) = id : key & idlookup_with_fallback_t id lc fb
 
 let isNonEmpty (#t : Type) (l : list t)
 = match l with

src/ASN1/ASN1.Spec.Content.UTF8STRING.fst

@@ -1,5 +1,4 @@
 module ASN1.Spec.Content.UTF8STRING
-
 open ASN1.Base
 open ASN1.Spec.Automata
 
@@ -184,7 +183,7 @@ let utf8_cp_bp : automata_bare_parser_param utf8_cp_cp = {
     fun _ -> parser_kind_prop_equiv parse_u8_kind parse_u8
 }
 
-#push-options "--z3rlimit 64 --fuel 4 --ifuel 1 --split_queries"
+#push-options "--z3rlimit 64 --fuel 4 --ifuel 1" // --split_queries"
 
 let lemma_update_term_inj2 
   (state : utf8_cp_s)

src/ASN1/ASN1.Spec.IdentifierU32.fst

@@ -267,8 +267,6 @@ let parse_asn1_identifier_loop_immediate_terminate
 = let _ = in_bound_32 i state in
   parse_ret (update_state state buf)
 
-#push-options "--print_implicits --query_stats"
-
 let parse_cast
   (t : eqtype)
   (p1 : t -> Type0)

src/ASN1/ASN1.Spec.Interpreter.fst

@@ -1,5 +1,4 @@
 module ASN1.Spec.Interpreter
-
 include LowParse.Tot.Base
 include LowParse.Tot.Combinators
 include LowParse.Tot.List
@@ -41,6 +40,44 @@ let parse_non_empty_set
 : asn1_weak_parser (non_empty_list t)
 = (parse_asn1_set_of p) `parse_filter` isNonEmpty
 
+let auto_asn1_sequence_t_core_equiv #id_decs (items:asn1_gen_items_l id_decs)
+: Lemma
+  (ensures asn1_sequence_t_core items == asn1_sequence_t (l_as_list items))
+  [SMTPat (asn1_sequence_t (l_as_list items))]
+= asn1_sequence_t_core_equiv items
+
+let auto_asn1_sequence_t_core_equiv' (items:list asn1_gen_item_k)
+: Lemma 
+  (ensures asn1_sequence_t_core (list_as_l items) == asn1_sequence_t items)
+  [SMTPat (asn1_sequence_t items)]
+= asn1_sequence_t_core_equiv' items
+
+let auto_asn1_any_t_equiv (#t:eqtype) (ls:list (t & asn1_gen_items_lk))
+: Lemma
+  (ensures asn1_any_t_core t ls == asn1_any_t t (t_lk_as_t_k ls))
+  [SMTPat (asn1_any_t_core t ls)]
+= asn1_any_t_equiv ls
+
+let auto_asn1_any_t_equiv' (#t:eqtype) (ls:list (t & asn1_gen_items_k))
+: Lemma
+  (ensures asn1_any_t_core t (t_k_as_t_lk ls) == asn1_any_t t ls)
+  [SMTPat (asn1_any_t t ls)]
+= asn1_any_t_equiv' ls
+
+let auto_asn1_sequence_any_t_equiv #id_decs (items : asn1_gen_items_l id_decs) (suffix_t : Type)
+: Lemma
+  (ensures asn1_sequence_any_t_core items suffix_t ==
+           asn1_sequence_any_t (l_as_list items) suffix_t)
+  [SMTPat (asn1_sequence_any_t_core items suffix_t)]
+= asn1_sequence_any_t_equiv items suffix_t
+
+let auto_asn1_sequence_any_t_equiv' (items : list asn1_gen_item_k) (suffix_t : Type)
+: Lemma
+  (ensures asn1_sequence_any_t_core (list_as_l items) suffix_t ==
+           asn1_sequence_any_t items suffix_t)
+  [SMTPat (asn1_sequence_any_t items suffix_t)]
+= asn1_sequence_any_t_equiv' items suffix_t
+
 let rec dasn1_terminal_as_parser (k : asn1_terminal_k) : asn1_weak_parser (asn1_terminal_t k)  =
   parse_debug #(asn1_terminal_t k) #(asn1_weak_parser_kind) "asn1_terminal_as_parser"
   (match k with
@@ -57,16 +94,23 @@ let rec dasn1_terminal_as_parser (k : asn1_terminal_k) : asn1_weak_parser (asn1_
   | ASN1_GENERALIZEDTIME -> parse_asn1_GENERALIZEDTIME
   | ASN1_PREFIXED_TERMINAL id k -> weaken asn1_weak_parser_kind (parse_asn1_ILC id #(ASN1_TERMINAL k) (dasn1_terminal_as_parser k)))
 
+and dasn1_sequence_as_parser #id_decs (ls:asn1_gen_items_l id_decs)
+: Tot (lp : list gen_decorated_parser_twin {List.map (Mkgendcparser?.d) lp == l_as_list ls }) (decreases ls)
+= match ls with
+  | ASN1_GEN_ITEMS_NIL -> []
+  | ASN1_GEN_ITEMS_CONS s d hd _ tl ->
+    dasn1_decorated_as_parser_twin hd :: dasn1_sequence_as_parser tl
+
 and dasn1_content_as_parser (k : asn1_content_k) : Tot (asn1_weak_parser (asn1_content_t k)) (decreases k) =
   match k with
   | ASN1_RESTRICTED_TERMINAL k' is_valid -> weaken _ ((dasn1_terminal_as_parser k') `parse_filter` is_valid)
   | ASN1_TERMINAL k' -> dasn1_terminal_as_parser k'
-  | ASN1_SEQUENCE gitems -> make_asn1_sequence_parser (dasn1_sequence_as_parser (dfst (lk_as_k gitems)))
+  | ASN1_SEQUENCE gitems -> make_asn1_sequence_parser (dasn1_sequence_as_parser (dsnd gitems))
   | ASN1_SEQUENCE_OF k' -> parse_non_empty_list (dasn1_as_parser k')
   | ASN1_SET_OF k' -> parse_non_empty_set (dasn1_as_parser k')
   | ASN1_PREFIXED k' -> weaken _ (dasn1_as_parser k')
   | ASN1_ANY_DEFINED_BY id_decs_prefix prefix id key_k ls ofb pf pf' -> 
-    let itemtwins = dasn1_sequence_as_parser (l_as_list prefix) in
+    let itemtwins = dasn1_sequence_as_parser prefix in //(l_as_list prefix) in
     let key_p_twin = 
       (let kc = ASN1_TERMINAL key_k in
       let p = dasn1_terminal_as_parser key_k in
@@ -85,7 +129,11 @@ and dasn1_content_as_parser (k : asn1_content_k) : Tot (asn1_weak_parser (asn1_c
       in
       make_asn1_sequence_any_parser itemtwins suffix_p_twin
     | Some gitems -> 
-      let fallback_p = Mkgenparser _ (parse_debug "parse_any_fallback" (make_asn1_sequence_parser (dasn1_sequence_as_parser (dfst (lk_as_k gitems))))) in
+      let fallback_p = 
+        Mkgenparser _
+          (parse_debug "parse_any_fallback"
+            (make_asn1_sequence_parser
+              (dasn1_sequence_as_parser (dsnd gitems)))) in
       let suffix_p_twin = (Mkparsertwin #asn1_weak_parser_kind #(make_gen_choice_type_with_fallback (extract_types supported_p) (Mkgenparser?.t fallback_p))
         (weaken asn1_weak_parser_kind (make_gen_choice_with_fallback_weak_parser key_p supported_p fallback_p))
         (let _ = make_gen_choice_with_fallback_weak_parser_twin_and_then_cases_injective key_fp supported_p fallback_p in
@@ -98,7 +146,7 @@ and dasn1_ls_as_parser (t : eqtype) (ls : list (t * asn1_gen_items_lk)) : Tot (l
   | [] -> [] 
   | h :: tl -> 
     let (x, y) = h in
-    (x, Mkgenparser _ (make_asn1_sequence_parser (dasn1_sequence_as_parser (dfst (lk_as_k y))))) :: (dasn1_ls_as_parser t tl)
+    (x, Mkgenparser _ (make_asn1_sequence_parser (dasn1_sequence_as_parser (dsnd y)))) :: (dasn1_ls_as_parser t tl)
 
 and dasn1_lc_as_parser (lc : list (asn1_id_t & asn1_content_k)) : Tot (lp : list (asn1_id_t & (gen_parser asn1_strong_parser_kind)) {asn1_lc_t lc == extract_types lp})  (decreases lc) =
   match lc with
@@ -130,26 +178,27 @@ and dasn1_as_parser_twin (#s : _) (k : asn1_k s) : Tot (asn1_strong_parser (asn1
     (parse_debug "ASN1_ANY" (parse_asn1_anyILC), 
      parse_debugf "ASN1_ANY_f" (parse_asn1_anyILC_twin))
 
-and dasn1_decorated_as_parser_twin (item : asn1_gen_item_k) : Tot (gp : gen_decorated_parser_twin {Mkgendcparser?.d gp == item}) =
-  match item with
-  | (| _, _, dk |) -> match dk with
-                    | ASN1_PLAIN_ILC k -> 
-                      let (p, fp) = dasn1_as_parser_twin k in
-                      Mkgendcparser item p fp
-                    | ASN1_OPTION_ILC k -> 
-                      let (p, fp) = dasn1_as_parser_twin k in
-                      Mkgendcparser item p fp
-                    | ASN1_DEFAULT_TERMINAL id #k defv ->
-                      let p = dasn1_terminal_as_parser k in
-                      Mkgendcparser item (parse_asn1_ILC id #(ASN1_TERMINAL k) p) (parse_asn1_ILC_twin id #(ASN1_TERMINAL k) p)
-                    | ASN1_DEFAULT_RESTRICTED_TERMINAL id #k is_valid defv ->
-                      let p : asn1_weak_parser (asn1_decorated_pure_t item) = weaken _ ((dasn1_terminal_as_parser k) `parse_filter` is_valid) in
-                      Mkgendcparser item (parse_asn1_ILC id #(ASN1_RESTRICTED_TERMINAL k is_valid) p) (parse_asn1_ILC_twin id #(ASN1_RESTRICTED_TERMINAL k is_valid) p)
+and dasn1_decorated_as_parser_twin 
+  (#s : FStar.Set.set asn1_id_t)
+  (#d : asn1_decorator)
+  (dk:asn1_decorated_k s d)
+: Tot (gp : gen_decorated_parser_twin {Mkgendcparser?.d gp == (| s, d, dk |) })
+      (decreases dk)
+= let item : asn1_gen_item_k = (| s, d, dk |) in
+  match dk with
+  | ASN1_PLAIN_ILC k -> 
+    let (p, fp) = dasn1_as_parser_twin k in
+    Mkgendcparser item p fp
+  | ASN1_OPTION_ILC k -> 
+    let (p, fp) = dasn1_as_parser_twin k in
+    Mkgendcparser item p fp
+  | ASN1_DEFAULT_TERMINAL id #k defv ->
+    let p = dasn1_terminal_as_parser k in
+    Mkgendcparser item (parse_asn1_ILC id #(ASN1_TERMINAL k) p) (parse_asn1_ILC_twin id #(ASN1_TERMINAL k) p)
+  | ASN1_DEFAULT_RESTRICTED_TERMINAL id #k is_valid defv ->
+    let p : asn1_weak_parser (asn1_decorated_pure_t item) = weaken _ ((dasn1_terminal_as_parser k) `parse_filter` is_valid) in
+    Mkgendcparser item (parse_asn1_ILC id #(ASN1_RESTRICTED_TERMINAL k is_valid) p) (parse_asn1_ILC_twin id #(ASN1_RESTRICTED_TERMINAL k is_valid) p)
 
-and dasn1_sequence_as_parser (items : list asn1_gen_item_k) : Tot (lp : list gen_decorated_parser_twin {List.map (Mkgendcparser?.d) lp == items}) (decreases items) =
-  match items with
-  | [] -> []
-  | hd :: tl -> (dasn1_decorated_as_parser_twin hd) :: (dasn1_sequence_as_parser tl)
 
 let rec asn1_terminal_as_parser (k : asn1_terminal_k) : asn1_weak_parser (asn1_terminal_t k)  =
   match k with
@@ -170,12 +219,12 @@ and asn1_content_as_parser (k : asn1_content_k) : Tot (asn1_weak_parser (asn1_co
   match k with
   | ASN1_RESTRICTED_TERMINAL k' is_valid -> weaken _ ((asn1_terminal_as_parser k') `parse_filter` is_valid)
   | ASN1_TERMINAL k' -> asn1_terminal_as_parser k'
-  | ASN1_SEQUENCE gitems -> make_asn1_sequence_parser (asn1_sequence_as_parser (dfst (lk_as_k gitems)))
+  | ASN1_SEQUENCE gitems -> make_asn1_sequence_parser (asn1_sequence_as_parser (dsnd gitems))
   | ASN1_SEQUENCE_OF k' -> parse_non_empty_list (asn1_as_parser k')
   | ASN1_SET_OF k' -> parse_non_empty_set (asn1_as_parser k')
   | ASN1_PREFIXED k' -> weaken _ (asn1_as_parser k')
   | ASN1_ANY_DEFINED_BY id_decs_prefix prefix id key_k ls ofb pf pf' -> 
-    let itemtwins = asn1_sequence_as_parser (l_as_list prefix) in
+    let itemtwins = asn1_sequence_as_parser prefix in
     let key_p_twin = 
       (let kc = ASN1_TERMINAL key_k in
       let p = asn1_terminal_as_parser key_k in
@@ -194,7 +243,7 @@ and asn1_content_as_parser (k : asn1_content_k) : Tot (asn1_weak_parser (asn1_co
       in
       make_asn1_sequence_any_parser itemtwins suffix_p_twin
     | Some gitems -> 
-      let fallback_p = Mkgenparser _ (make_asn1_sequence_parser (asn1_sequence_as_parser (dfst (lk_as_k gitems)))) in
+      let fallback_p = Mkgenparser _ (make_asn1_sequence_parser (asn1_sequence_as_parser (dsnd gitems))) in
       let suffix_p_twin = (Mkparsertwin #asn1_weak_parser_kind #(make_gen_choice_type_with_fallback (extract_types supported_p) (Mkgenparser?.t fallback_p))
         (weaken asn1_weak_parser_kind (make_gen_choice_with_fallback_weak_parser key_p supported_p fallback_p))
         (let _ = make_gen_choice_with_fallback_weak_parser_twin_and_then_cases_injective key_fp supported_p fallback_p in
@@ -207,7 +256,7 @@ and asn1_ls_as_parser (t : eqtype) (ls : list (t * asn1_gen_items_lk)) : Tot (lp
   | [] -> [] 
   | h :: tl -> 
     let (x, y) = h in
-    (x, Mkgenparser _ (make_asn1_sequence_parser (asn1_sequence_as_parser (dfst (lk_as_k y))))) :: (asn1_ls_as_parser t tl)
+    (x, Mkgenparser _ (make_asn1_sequence_parser (asn1_sequence_as_parser (dsnd y)))) :: (asn1_ls_as_parser t tl)
 
 and asn1_lc_as_parser (lc : list (asn1_id_t & asn1_content_k)) : Tot (lp : list (asn1_id_t & (gen_parser asn1_strong_parser_kind)) {asn1_lc_t lc == extract_types lp})  (decreases lc) =
   match lc with
@@ -236,24 +285,28 @@ and asn1_as_parser_twin (#s : _) (k : asn1_k s) : Tot (asn1_strong_parser (asn1_
     let _ = parse_asn1_anyILC_twin_and_then_cases_injective () in
     (parse_asn1_anyILC, parse_asn1_anyILC_twin)
 
-and asn1_decorated_as_parser_twin (item : asn1_gen_item_k) : Tot (gp : gen_decorated_parser_twin {Mkgendcparser?.d gp == item}) =
-  match item with
-  | (| _, _, dk |) -> match dk with
-                    | ASN1_PLAIN_ILC k -> 
-                      let (p, fp) = asn1_as_parser_twin k in
-                      Mkgendcparser item p fp
-                    | ASN1_OPTION_ILC k -> 
-                      let (p, fp) = asn1_as_parser_twin k in
-                      Mkgendcparser item p fp
-                    | ASN1_DEFAULT_TERMINAL id #k defv ->
-                      let p = asn1_terminal_as_parser k in
-                      Mkgendcparser item (parse_asn1_ILC id #(ASN1_TERMINAL k) p) (parse_asn1_ILC_twin id #(ASN1_TERMINAL k) p)
-                    | ASN1_DEFAULT_RESTRICTED_TERMINAL id #k is_valid defv ->
-                      let p : asn1_weak_parser (asn1_decorated_pure_t item) = weaken _ ((asn1_terminal_as_parser k) `parse_filter` is_valid) in
-                      Mkgendcparser item (parse_asn1_ILC id #(ASN1_RESTRICTED_TERMINAL k is_valid) p) (parse_asn1_ILC_twin id #(ASN1_RESTRICTED_TERMINAL k is_valid) p)
-
-and asn1_sequence_as_parser (items : list asn1_gen_item_k) : Tot (lp : list gen_decorated_parser_twin {List.map (Mkgendcparser?.d) lp == items}) (decreases items) =
-  match items with
-  | [] -> []
-  | hd :: tl -> (asn1_decorated_as_parser_twin hd) :: (asn1_sequence_as_parser tl)
+and asn1_decorated_as_parser_twin #s #d (dk:asn1_decorated_k s d) 
+: Tot (gp : gen_decorated_parser_twin {Mkgendcparser?.d gp == (| s, d, dk |) })
+      (decreases dk)
+= let item = (| s, d, dk |) in
+  match dk with
+  | ASN1_PLAIN_ILC k -> 
+    let (p, fp) = asn1_as_parser_twin k in
+    Mkgendcparser item p fp
+  | ASN1_OPTION_ILC k -> 
+    let (p, fp) = asn1_as_parser_twin k in
+    Mkgendcparser item p fp
+  | ASN1_DEFAULT_TERMINAL id #k defv ->
+    let p = asn1_terminal_as_parser k in
+    Mkgendcparser item (parse_asn1_ILC id #(ASN1_TERMINAL k) p) (parse_asn1_ILC_twin id #(ASN1_TERMINAL k) p)
+  | ASN1_DEFAULT_RESTRICTED_TERMINAL id #k is_valid defv ->
+    let p : asn1_weak_parser (asn1_decorated_pure_t item) = weaken _ ((asn1_terminal_as_parser k) `parse_filter` is_valid) in
+    Mkgendcparser item (parse_asn1_ILC id #(ASN1_RESTRICTED_TERMINAL k is_valid) p) (parse_asn1_ILC_twin id #(ASN1_RESTRICTED_TERMINAL k is_valid) p)
 
+and asn1_sequence_as_parser 
+  #id_decs (ls:asn1_gen_items_l id_decs)
+: Tot (lp : list gen_decorated_parser_twin {List.map (Mkgendcparser?.d) lp == l_as_list ls }) (decreases ls)
+= match ls with
+  | ASN1_GEN_ITEMS_NIL -> []
+  | ASN1_GEN_ITEMS_CONS s d dk _ tl ->
+    asn1_decorated_as_parser_twin dk :: asn1_sequence_as_parser tl

src/ASN1/ASN1.Spec.Time.fst

@@ -136,7 +136,7 @@ let rec is_valid_digit_range
     is_valid_digit (B.index b (U32.v (U32.add s l'))) &&
     is_valid_digit_range b s l'
 
-#push-options "--fuel 8 --split_queries"
+#push-options "--fuel 8 --split_queries always"
 
 let is_valid_yymmdd
   (b : B.bytes)

src/ASN1/ASN1.Syntax.fst

@@ -1,5 +1,4 @@
 module ASN1.Syntax
-
 open ASN1.Base
 
 module U32 = FStar.UInt32
@@ -23,10 +22,8 @@ let mk_oid (l : list (UInt.uint_t 32)) : Pure (asn1_oid_t)
   (requires asn1_OID_wf (List.map U32.uint_to_t l))
   (ensures fun _ -> True)
 = List.map U32.uint_to_t l
-
 let mk_oid_app (oid : asn1_oid_t) (x : UInt.uint_t 32) : asn1_oid_t
-= norm[zeta;iota;delta;primops;nbe] (List.append oid [U32.uint_to_t x])
-
+= norm [zeta;iota;delta;primops;nbe] (List.append oid [U32.uint_to_t x])
 let op_Slash_Plus = mk_oid_app
 
 // for choices
@@ -107,8 +104,9 @@ let op_Hat_Colon (#s : Set.set asn1_id_t)
 noextract
 let seq_tac () =  T.norm[iota;zeta;delta;primops;simplify]; T.smt()
 
-let mk_gen_items (items : list asn1_gen_item_k) (pf : squash (asn1_sequence_k_wf (List.map proj2_of_3 items))) : asn1_gen_items_k
-= (| items, pf |)
+let mk_gen_items (items : list asn1_gen_item_k) (pf : squash (asn1_sequence_k_wf (List.map proj2_of_3 items)))
+: asn1_gen_items_lk
+= k_as_lk (| items, pf |)
 
 // constants
 
@@ -145,7 +143,7 @@ let asn1_utf8string = ASN1_ILC utf8string_id (ASN1_TERMINAL ASN1_UTF8STRING)
 let sequence_id = mk_constant_constructed_id 16
 
 let asn1_sequence (items : list asn1_gen_item_k) (pf : squash (asn1_sequence_k_wf (List.map proj2_of_3 items)))
-= ASN1_ILC sequence_id (ASN1_SEQUENCE (| items, pf |))
+= ASN1_ILC sequence_id (ASN1_SEQUENCE (k_as_lk (| items, pf |) ))
 
 let asn1_sequence_of (#s) (item : asn1_k s) = ASN1_ILC sequence_id (ASN1_SEQUENCE_OF item)
 
@@ -192,22 +190,22 @@ let asn1_any = ASN1_ANY_ILC
 let asn1_any_oid_prefix
   (prefix : list asn1_gen_item_k)
   (name : string)
-  (supported : list (asn1_oid_t * asn1_gen_items_k)) 
+  (supported : list (asn1_oid_t * asn1_gen_items_lk)) 
   (pf_wf : squash (asn1_any_prefix_k_wf (Set.singleton oid_id) (List.map proj2_of_3 prefix)))
   (pf_sup : squash (List.noRepeats (List.map fst supported)))
-= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY prefix oid_id ASN1_OID supported None pf_wf pf_sup)
+= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY _ (list_as_l prefix) oid_id ASN1_OID supported None pf_wf pf_sup)
 
 let asn1_any_oid
   (name : string)
-  (supported : list (asn1_oid_t * asn1_gen_items_k)) 
+  (supported : list (asn1_oid_t * asn1_gen_items_lk)) 
   (pf_wf : squash (asn1_any_prefix_k_wf (Set.singleton oid_id) (List.map proj2_of_3 [])))
   (pf_sup : squash (List.noRepeats (List.map fst supported)))
-= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY [] oid_id ASN1_OID supported None pf_wf pf_sup)
+= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY _ (list_as_l []) oid_id ASN1_OID supported None pf_wf pf_sup)
 
 let asn1_any_oid_with_fallback
   (name : string)
-  (supported : list (asn1_oid_t * asn1_gen_items_k)) 
-  (fallback : asn1_gen_items_k)
+  (supported : list (asn1_oid_t * asn1_gen_items_lk)) 
+  (fallback : asn1_gen_items_lk)
   (pf_wf : squash (asn1_any_prefix_k_wf (Set.singleton oid_id) (List.map proj2_of_3 [])))
   (pf_sup : squash (List.noRepeats (List.map fst supported)))
-= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY [] oid_id ASN1_OID supported (Some fallback) pf_wf pf_sup)
+= ASN1_ILC sequence_id (ASN1_ANY_DEFINED_BY _ (list_as_l []) oid_id ASN1_OID supported (Some fallback) pf_wf pf_sup)