Error with building ASN1*, while verifying ASN1.Spec.Interpreter.fst

[Black-Kamous]

Error was met while I'm running make in everparse/src/ASN1 directory with the code I downloaded from ASN1. The original error was something about typing.

Then I have read about the comment. And I tried to add proper converting function in ASN1.Spec.Interpreter.fst following the instructions in newer ASN1.Base.fst. e.g.

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_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 key_p_twin = 
      (let kc = ASN1_TERMINAL key_k in
      let p = dasn1_terminal_as_parser key_k in
      let _ = parser_asn1_ILC_twin_case_injective id #kc p in
      Mkparsertwin #asn1_strong_parser_kind #(asn1_terminal_t key_k) (parse_asn1_ILC id #kc p) (parse_asn1_ILC_twin id #kc p))
    in
    let key_p = Mkparsertwin?.p key_p_twin in
    let key_fp = Mkparsertwin?.fp key_p_twin in
    let supported_p = dasn1_ls_as_parser (asn1_terminal_t key_k) ls in
    (match ofb with
    | None -> 
      let suffix_p_twin = (Mkparsertwin #asn1_weak_parser_kind #(make_gen_choice_type (extract_types supported_p))
        (weaken asn1_weak_parser_kind (make_gen_choice_weak_parser key_p supported_p))
        (let _ = make_gen_choice_weak_parser_twin_and_then_cases_injective key_fp supported_p in
         fun id -> weaken asn1_weak_parser_kind (make_gen_choice_weak_parser_twin key_fp supported_p id)))
      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 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
         fun id -> weaken asn1_weak_parser_kind (make_gen_choice_with_fallback_weak_parser_twin key_fp supported_p fallback_p id))) 
      in
      make_asn1_sequence_any_parser itemtwins suffix_p_twin) 

After adding proper lk_ask or l_as_list there was no typing error, but I still get

* Error 19 at ASN1.Spec.Interpreter.fst(67,80-67,103):
  - Could not prove termination of this recursive call
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also ASN1.Spec.Interpreter.fst(64,2-97,60)

* Error 19 at ASN1.Spec.Interpreter.fst(104,23-104,48):
  - Could not prove termination of this recursive call
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also ASN1.Spec.Interpreter.fst(100,2-104,125)

Looks like 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) is not terminating. I'm quite new to F* and proof assistants, so I'm not sure how to fix it. I tried rewriting this function with asn1_gen_items_l instead of list asn1_gen_item_k, but still got this non-terminating problem.

By the way, I'm not sure if this is the right place to post issues about ASN1*, please tell me if there is a better place.
Thanks a lot!

[nikswamy]

Thank you so much for diving into this and fixing the positivity issues!

Would you mind opening a PR into the branch of PR #66. I'd be happy to take a closer look from there and see if I can fix the two termination issues you report.