LowParse: add support for non-injective parsers#258
Merged
tahina-pro merged 8 commits intoproject-everest:masterfrom Feb 24, 2026
Merged
LowParse: add support for non-injective parsers#258tahina-pro merged 8 commits intoproject-everest:masterfrom
tahina-pro merged 8 commits intoproject-everest:masterfrom
Conversation
…ivity Add a Boolean field parser_kind_injective to parser_kind so that parser_kind_prop enforces the injectivity property only when parser_kind_injective is true. The serializer refinement type now requires parser_kind_injective == true, ensuring serializers can only be constructed for injective parsers. Key changes: - LowParse.Spec.Base: Added parser_kind_injective field to parser_kind'. Made injective enforcement conditional in parser_kind_prop'. Strengthened no_lookahead_on_postcond to include consumed length equality. Updated glb to AND the injective fields. Added serializer_parser_injective lemma. - LowParse.Spec.Combinators: Made and_then_cases_injective conditional on (and_then_kind k k').parser_kind_injective. Made synth_injective conditional on k.parser_kind_injective. Required parser_kind_injective for serialize_tagged_union and serialize_dtuple2. - LowParse.Spec.BitSum: Added inj:bool parameter to weaken_parse_bitsum_cases_kind' to avoid nested quantifier SMT issues. Used Classical.impl_intro with named lemmas for injectivity proofs. Added serializer_parser_injective loops in serialize_bitsum_cases and serialize_bitsum. - LowParse.Low.Base.Spec: Removed gaccessor_injective from gaccessor_prop', keeping only gaccessor_no_lookahead. Added k2.parser_kind_subkind == Some ParserStrong precondition to gaccessor_compose. Proved gaccessor_compose_no_lookahead using parse_strong_prefix. - LowParse.Low.Combinators: Updated gaccessor/accessor variants (fst_then, then_fst, then_snd) with ParserStrong constraints. Made validate_filter_and_then's and_then_cases_injective conditional. - LowParse.Spec.List: Made parse_list_bare_injective conditional on k.parser_kind_injective. Changed parse_list_kind to take inj:bool. - LowParse.Spec.Recursive: Fixed parse_recursive_payload_kind calls to pass inj argument. - LowParse.Spec.VLData: Made and_then_cases_injective conditional in parse_vldata_gen_eq_def. - LowParse.SLow.Combinators: Made parse32_and_then's and_then_cases_injective conditional. - LowParse.Low.Writers.Instances: Added k2.parser_kind_injective == true to swrite_weaken precondition. - LowParse.Pulse.Combinators: Added k2.parser_kind_injective == true to all s2 serializer parameters for serialize_dtuple2 compatibility. All files in src/lowparse and src/lowparse/pulse verify successfully.
accessor_compose no longer takes a unit argument after the parser_kind_injective refactoring. Update LowParseExample3.Aux.fst to remove the extra () arguments from accessor_compose calls.
accessor_compose no longer takes a unit argument after the parser_kind_injective refactoring. Update the QD code generator (src/qd/rfc_fstar_compiler.ml) to stop emitting the extra () argument in generated accessor_compose calls. Also remove the now-unnecessary compose_needs_unit parameter from write_accessor helper functions. Fix hand-written test files in tests/sample0/ accordingly.
- ASN1.Base.fst: Add parser_kind_injective = true to asn1_strong_parser_kind and asn1_weak_parser_kind. - ASN1.Spec.Content.INTEGER.fst: Add parser_kind_injective = true to parse_untagged_bounded_integer_kind and parse_integer_payload_kind. - ASN1.Spec.Automata.fst: Add parser_kind_injective = true to automata_default_parser_kind. - ASN1.Spec.Choice.fst: Propagate parser_kind_injective field in sanitify_parser_kind. - ASN1.Spec.Set.fst: Add k.parser_kind_injective == true precondition to repr_order_prop_intro, tot_parse_byte_sorted_list_aux_correct, tot_parse_byte_sorted_list_correct, and tot_parse_byte_sorted_list. Pass inj argument to parse_list_kind. - ASN1.Spec.Interpreter.fst: Add k.parser_kind_injective == true to parse_non_empty_list. Inline kc = ASN1_TERMINAL key_k to avoid variable escape. Add assert_norm for is_weaker_than checks on and_then_kind.
Add parser_kind_injective = true to parse_content_kind and parse_raw_data_item_kind record literals in CBOR.Spec.Raw.EverParse.fst.
- Added parser_kind_injective = true to parser_kind_prop in EverParse3d.Kinds.fst (all 3d parser kinds are injective, since parser_kind is abstract) - Added parser_kind_injective = true to kind_nlist_default, kind_nlist Some branch, and parse_string_kind record literals - Fixed kind_all_zeros to pass true to parse_list_kind - Updated parse_list_kind calls in EverParse3d.Prelude.fst and EverParse3d.Actions.Base.fst to pass k.LP.parser_kind_injective - Added k.parser_kind_injective == true to parse_nlist_total_fixed_size_kind_correct requires clause
Replace the overly restrictive k2.parser_kind_subkind == Some ParserStrong precondition on gaccessor_compose and related functions with the weaker k2.parser_kind_injective == true. This restores the previous expressivity of gaccessors in LowParse.Low. Key changes: - Add gaccessor_injective back to gaccessor_prop' (conjunction with gaccessor_no_lookahead), so gaccessor constructors must prove both - Change gaccessor_compose, gaccessor_compose_eq, accessor_compose to require k2.parser_kind_injective == true instead of ParserStrong - Add gaccessor_compose_injective proof (uses injective_precond + no_lookahead of intermediate parser p2) - Update gaccessor_compose_no_lookahead proof to use injective_precond - Change gaccessor_fst_then, gaccessor_then_fst, gaccessor_then_snd and their accessor variants to use parser_kind_injective == true - Add gaccessor_snd_injective call to gaccessor_snd construction - Add _injective lemma calls to gaccessor constructions in: LowParse.Low.Combinators (tagged_union_payload) LowParse.Low.Sum (sum_payload, dsum_payload, dsum_unknown_payload) LowParse.Low.IfThenElse (ifthenelse_payload) LowParse.Low.VLGen (bounded_vlgen_payload, vlgen_payload) - Add parser_kind_injective == true to LowParse.Repr.fsti strong_parser_kind
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Commits of this PR have been entirely AI-generated (including a rebase) by GitHub Copilot CLI 0.406.0 using Claude Opus 4.5 and 4.6, running from tahina-pro/quackyducky@b390b2c (which has AI skills duplicated and adapted from F* and Pulse.)
So far the
injectivecondition inparser_kind_prophas been unconditionally required for allparserspecifications. This PR now adds a new Boolean field toparser_kindand makesinjectiveconditional on the value of that field. Then, it allows non-injective parsers on many existing combinators, includingparse_filter,parse_synth, and (non-dependent and dependent) pairs, sums, and bitfields.At this point, serializer specifications (and thus PulseParse), Low* accessors, and 3D still require injective parsers. (Of course, so do QuackyDucky and ASN.1*, which are designed for proving non-malleability anyway.)