ASN1* : Provably Correct Non-Malleable Parsing for ASN.1 DER

[FVRobbin]

Need directions on improving code quality

[ghost]

All CLA requirements met.

[nikswamy]

Hi @FVRobbin hi @tahina-pro

The definition of asn1_content_k is not provably strictly positive. The version of F* that was used to check this code initially had a bug in the positivity checker that was skipping positivity checks in refinement types. This has since been fixed: See F* PR FStarLang/FStar#2827

A rough summary of the situation can be seen in this Coq definition:

Variable SomePred : List Bool -> Prop.

Inductive T :=
  | MkT : 
     forall (l:List (Bool * T)),
     SomePred (map fst l) ->
     T.

This is rejected by Coq's strict positivity checker too. Arguably, this type is benign and should be accepted, but positivity checkers in all dependently typed languages, including Coq and F*, and very syntactic, and this definition is not admissible.

This type T is the essence of the style used in the definition of asn1_content_k. For example, this part:

and asn1_gen_items_k : Type = items : list (asn1_gen_item_k) & squash (asn1_sequence_k_wf (List.map proj2_of_3 items))

The good news is that it is possible to rephrase the definition of asn1_content_k so that it is provably strictly positive. I have done this in my most recent commit to this branch, where, I decoupled the id and decorator from the decorated type, like so:

+let id_dec = Set.set asn1_id_t & asn1_decorator
+let id_decs = list id_dec
...
-and asn1_gen_item_k : Type = s : Set.set asn1_id_t & d : asn1_decorator & asn1_decorated_k s d

-and asn1_gen_items_k : Type = items : list (asn1_gen_item_k) & squash (asn1_sequence_k_wf (List.map proj2_of_3 items))

+and asn1_gen_items_l : id_decs -> Type0 =
+  | ASN1_GEN_ITEMS_NIL : asn1_gen_items_l []
+  | ASN1_GEN_ITEMS_CONS : s:Set.set asn1_id_t -> d:asn1_decorator -> asn1_decorated_k s d ->
+                          tl:id_decs -> asn1_gen_items_l tl -> asn1_gen_items_l ((s, d)::tl)
+
+and asn1_gen_items_lk : Type = (id_decs:id_decs { asn1_sequence_k_wf id_decs } & asn1_gen_items_l id_decs)

I can still define types of the previous style:

let asn1_gen_item_k : Type = s : Set.set asn1_id_t & d : asn1_decorator & asn1_decorated_k s d
let asn1_gen_items_k : Type = items : list (asn1_gen_item_k) & squash (asn1_sequence_k_wf (List.map proj2_of_3 items))

with functions to go back and forth:

+let lk_as_k (lk:asn1_gen_items_lk) : asn1_gen_items_k
+let k_as_lk (k:asn1_gen_items_k)  : asn1_gen_items_lk

But, this change is pervasive and it impacts the whole development.

For example, I had to change the type interpretation to work with these new definitions, but then I was able to prove lemmas to show that the new definitions are equivalent to the old-style ones.

E.g., I defined

+and asn1_sequence_t_core #id_decs (items:asn1_gen_items_l id_decs) : Tot Type (decreases items) =

But, I also proved:

+let rec asn1_sequence_t (items:list asn1_gen_item_k) =
+  match items with
+  | [] -> unit
+  | [hd] ->
+    asn1_decorated_t hd
+  | hd::tl ->
+    asn1_decorated_t hd & asn1_sequence_t tl
+
+let rec 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))
...
+let rec 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)

So, that's where things stand in ASN1.Base.fst right now.

A couple of questions:

• If you have any feedback about this revised style of definition, that would be most welcome. I considered various alternatives, and this seemed the most straightforward. But, you may have other ideas.

• I think the change to restore the rest of the code is fairly mechanical, following the style I used in revising the type denotation. But, I might be missing some subtlety somewhere. @FVRobbin, you might be way faster than me in propagating this change.

It would be great to sort this out, restore this code with respect to F* master, and then merge this PR, so it doesn't fall off the CI train again.

[nikswamy]

I restored the proofs, thanks @Black-Kamous!

I would like to merge this PR, but @tahina-pro, I'm not sure why some of the checks above are failing.