Open Black-Kamous opened 1 week ago
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.
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.
After adding proper
lk_ask
orl_as_list
there was no typing error, but I still getLooks 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 withasn1_gen_items_l
instead oflist 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!