Upgrade to F* Universes #244
Conversation
tahina-pro
force-pushed
the
_nik_smt_univs_2025
branch
from
adc3989 to
f771f78
Compare
|
Hi @nikswamy , @gebner and @mtzguido ! Blocking issues
Can anyone please help me there? Thanks in advance! Other lessons learned
Current statusApart from the blocking issues above:
|
| # TODO: remove this once map serializers are implemented | ||
| RUN := $(filter-out Basic1 BenchMap,$(RUN)) | ||
|
|
There was a problem hiding this comment.
This change is to be reverted once generic CDDL map serializers are implemented.
Those two tests, Basic1 and BenchMap, serialize nonempty tables, which https://github.com/project-everest/everparse/pull/244/changes#r2760178949 currently disables.
| @@ -548,6 +556,8 @@ let impl_serialize_array_group_valid_zero_or_more_true_intro_length | |||
| ((x1 + x2) + (x3 + x4) == (x1 + (x2 + x3)) + x4) | |||
| = () | |||
|
|
|||
| #push-options "--z3rlimit 32" | |||
|
|
|||
| let impl_serialize_array_group_valid_zero_or_more_true_intro | |||
| (l: list Cbor.cbor) | |||
| (#t: array_group None) | |||
| @@ -581,9 +591,9 @@ let impl_serialize_array_group_valid_zero_or_more_true_intro | |||
| ag_serializable_zero_or_more_append ps1 l1 [x]; | |||
| assert (ps.ag_serializable (List.Tot.append l1 [x])); | |||
| ag_spec_zero_or_more_serializer_append ps1 l1 [x]; | |||
| assert (let ps = ag_spec_zero_or_more ps1 in | |||
| assume (let ps = ag_spec_zero_or_more ps1 in | |||
| (ps.ag_serializer [x] <: list cbor) == List.Tot.append (ps1.ag_serializer x) []) | |||
| by (FStar.Tactics.trefl ()); // FIXME: WHY WHY WHY? | |||
| ; // by (FStar.Tactics.trefl ()); // FIXME: WHY WHY WHY? | |||
| List.Tot.append_l_nil (ps1.ag_serializer x); | |||
| assert ((ps.ag_serializer [x] <: list cbor) == ps1.ag_serializer x); | |||
| assert ((ps.ag_size [x] <: nat) == ps1.ag_size x); | |||
| @@ -597,11 +607,11 @@ let impl_serialize_array_group_valid_zero_or_more_true_intro | |||
| assert (ps.ag_serializable (x :: l2) == ps.ag_serializable l2); | |||
| if ps.ag_serializable l2 | |||
| then begin | |||
| assert ( | |||
| assume ( | |||
| let ps = ag_spec_zero_or_more ps1 in | |||
| (ps.ag_serializer (x :: l2) <: list cbor) == List.Tot.append (ps1.ag_serializer x) (ps.ag_serializer l2) | |||
| ) | |||
| by (FStar.Tactics.trefl ()); // FIXME: WHY WHY WHY? | |||
| ; // by (FStar.Tactics.trefl ()); // FIXME: WHY WHY WHY? | |||
There was a problem hiding this comment.
These assumes are to be removed and replaced with a generic implementation of array group serializers - where the signature of the serializer implementation uses a generic CBOR parser specification instead of the deterministic serializer specification.
| inline_for_extraction noextract [@@noextract_to "krml"] | ||
| fn admit_as_abort_true | ||
| (_: unit) | ||
| returns res: bool | ||
| ensures pure (res == true) | ||
| { | ||
| admit () // Karamel should extract as KRML_ABORT | ||
| } |
There was a problem hiding this comment.
This function extracts to KRML_EABORT. Indeed, if admit () is used with unit return type, then it is erased at extraction. That's why we use an informative return type, here bool.
This function is to be removed once this file is replaced with generic map group serializers.
| @@ -687,6 +761,11 @@ let map_of_list_is_append_serializable_elim' | |||
| )) | |||
There was a problem hiding this comment.
This assume is to be removed once this file is replaced with generic map group serializers.
| @@ -711,17 +790,24 @@ let map_of_list_is_append_serializable_singleton | |||
| (sp.mg_serializable m ==> ( | |||
| sp.mg_serializer m == cbor_map_singleton (sp1.serializer k) (sp2.serializer v) | |||
| )))) | |||
| = let sp = mg_zero_or_more_match_item sp1 sp2 except in | |||
| = admit () | |||
| (* | |||
There was a problem hiding this comment.
This admit is to be removed once this file is replaced with generic map group serializers.
| @@ -776,7 +862,7 @@ let impl_serialize_map_group_valid_map_zero_or_more_snoc_aux | |||
| cbor_map_union l (sp.mg_serializer (map_of_list_snoc key_eq m1 k v)) == cbor_map_union (cbor_map_union l (sp.mg_serializer m1)) (cbor_map_singleton (sp1.serializer k) (sp2.serializer v)) /\ | |||
| cbor_map_length (sp.mg_serializer (map_of_list_snoc key_eq m1 k v)) == cbor_map_length (sp.mg_serializer m1) + 1 | |||
| )))) | |||
| = | |||
| = admit(); | |||
There was a problem hiding this comment.
This admit is to be removed once this file is replaced with generic map group serializers.
| @@ -858,7 +944,7 @@ let impl_serialize_map_group_valid_map_zero_or_more_snoc_disjoint1 | |||
| sp.mg_serializable m1' /\ | |||
| cbor_map_disjoint (sp.mg_serializer m1') (sp.mg_serializer m2) <==> cbor_map_disjoint (sp.mg_serializer m1) (sp.mg_serializer m2) | |||
| )) | |||
| = | |||
| = admit(); | |||
There was a problem hiding this comment.
This admit is to be removed once this file is replaced with generic map group serializers.
| cbor_map_length (cbor_map_union l (sp.mg_serializer m1)) + cbor_map_length (sp.mg_serializer m2') == cbor_map_length (cbor_map_union l (sp.mg_serializer m1')) + cbor_map_length (sp.mg_serializer m2) | ||
| )) | ||
| = | ||
| = admit(); |
There was a problem hiding this comment.
(for impl_serialize_map_group_valid_map_zero_or_more_snoc_length1)
This admit is to be removed once this file is replaced with generic map group serializers.
| )) | ||
| )) | ||
| = impl_serialize_map_group_valid_map_zero_or_more_snoc_aux sp1 key_eq sp2 except l m1 k v m2 len; | ||
| = admit(); |
There was a problem hiding this comment.
(for impl_serialize_map_group_valid_map_zero_or_more_snoc')
This admit is to be removed once this file is replaced with generic map group serializers.
| b == (res && not (FStar.StrongExcludedMiddle.strong_excluded_middle (m2 == Map.empty _ _))) | ||
| ) | ||
| ) { | ||
| let ignore = admit_as_abort_true (); (); (* Pulse OOM |
There was a problem hiding this comment.
(for impl_serialize_map_group_valid_map_zero_or_more_iterator_gen)
This is an admit that extracts to KRML_EABORT. Without it, Pulse seems to go out of memory when typechecking the loop body. Instead of putting the admit on the whole combinator, it is enough to put it into the loop body, so that empty tables can still be serialized properly, which is necessary for EverCOSE.
This is to be removed once this file is replaced with generic map group serializers.
3 participants
FStarLang/FStar#3699 makes many EverParse proofs fail. This PR, authored by @nikswamy, fixes such proofs. Thanks a lot Nik!
Some remaining admits in this PR are slated to be overwritten once EverCDDL serialization is generalized beyond deterministically encoded CBOR.