Port LowParse combinators to Pulse#271
Merged
tahina-pro merged 122 commits intoproject-everest:masterfrom Apr 3, 2026
Merged
Conversation
Define parsing combinators that use pts_to_parsed (parser-only) instead of
pts_to_serialized (which requires a serializer and parser injectivity).
PulseParse.Base (extended):
- leaf_reader/reader types using pts_to_parsed
- leaf_reader_of_reader, reader_of_leaf_reader conversions
- leaf_reader_of_serialized, reader_of_serialized bridges
- read_parsed_from_validator_success (requires ParserStrong)
- ifthenelse_reader, reader_ext utilities
PulseParse.Combinators (new):
- Ghost lemmas: pts_to_parsed_synth_{intro,elim,trade,l2r,r2l,l2r_trade}
- Ghost lemmas: pts_to_parsed_filter_{intro,elim,elim_trade}
- Read: read_synth, read_synth', read_filter with helper types
- Validate: validate_filter, validate_filter', validate_dtuple2
- Jump: jump_dtuple2
- Ret/empty: leaf_read_ret, read_ret, leaf_read_empty, read_empty
PulseParse.BitSum (new):
- read_bitsum' (composition of read_filter and read_synth)
PulseParse.VCList (new):
- Ghost: pts_to_parsed_nlist_1_{intro,elim}, pts_to_parsed_nlist_ext
- Split: nlist_hd_tl, nlist_hd, nlist_tl
- Note: sub-slices have half permission (pm /. 2.0R) due to
non-injective pts_to_parsed_intro
PulseParse.Recursive (new, stub):
- All Recursive combinators require serialize_recursive_param and cannot
be ported without a complete redesign of the recursive infrastructure.
Combinators that cannot be rewritten without serializers:
- Writers (l2r_write_*, l2r_leaf_writer): write serialized bytes
- Size (compute_remaining_size): compute serialized byte lengths
- Copy/Gather: need serializer injectivity
- zero_copy_parse: returns trade to pts_to_serialized
- peek_trade_gen/validate_filter_gen: need serializer for sub-slice creation
- split_dtuple2/nondep_then (Combinators): tied to serializer byte sequences
- read_dtuple2: depends on split_dtuple2
- All Recursive operations: inseparable from serialize_recursive_param
Technical notes:
- pts_to_parsed_synth_{elim,l2r,r2l,l2r_trade} require synth_injective f
(stronger than the Pulse counterparts) because without known bytes we
need injectivity to recover the pre-image from parse_synth results
- read_parsed_from_validator_success requires ParserStrong to use
parse_strong_prefix for sub-slice correctness
- VCList nlist_hd_tl produces sub-slices at pm /. 2.0R because
pts_to_parsed_intro for non-injective parsers halves permission
Skipped modules:
- LowParse.Pulse.Int (per user request)
- LowParse.Pulse.Endianness (no serializer usage)
- LowParse.Pulse.SeqBytes (all operations write serialized data)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Port validator combinators from LowParse.Low.* to Pulse validators in
LowParse.PulseParse.*, replacing LowParse.Low.Base.validator (Low*/Stack)
with LowParse.Pulse.Base.validator (Pulse/stt). All verified with
make lowparse, no admit() or assume except FStar.SizeT.fits_u64
(taken as squash parameter where needed).
New files:
- LowParse.PulseParse.FLData.fst: validate_fldata, jump_fldata
Validates fixed-length data by splitting the input slice at the
expected boundary, running the inner validator on the prefix, and
checking the consumed length matches exactly.
- LowParse.PulseParse.List.fst: validate_list
Validates parse_list (zero-or-more elements until end of input).
Uses a while loop with invariant tracking Some?-equivalence of
parse_list at the original vs current offset. Requires
ParserStrong and parser_kind_low > 0.
- LowParse.PulseParse.Option.fst: validate_option
Validates parse_option: tries the inner validator; on success
returns true (Some case), on failure resets offset and returns
true (None case — parse_option always succeeds).
- LowParse.PulseParse.VLData.fst: validate_vldata_gen,
validate_bounded_vldata', validate_bounded_vldata
Validates variable-length data with a bounded-integer length prefix.
Reads the length prefix via leaf_reader, checks the filter predicate,
then splits the input at the payload boundary and validates the
payload, checking consumed == declared length. Takes a
PPB.leaf_reader for parse_bounded_integer as parameter.
Extended files:
- LowParse.PulseParse.Combinators.fst (+167 lines):
* validate_false: always fails (parse_false returns None)
* validate_strengthen: strengthen parser kind (delegates to validate_ext)
* validate_lift_parser: lift thunked parser (delegates to validate_ext)
* validate_filter_ret: filter on parse_ret without needing a reader
* validate_filter_and_then: validate filter then dependent parse,
requires ParserStrong and a leaf_reader for the first parser
* validate_synth: validate through synth (requires synth_injective)
* validate_nondep_then: sequential validation of two parsers
* validate_compose_context: re-index a parser family
- LowParse.PulseParse.VCList.fst (+114 lines):
* validate_nlist: validate exactly n elements in a loop. Simple
while loop counting down from n, calling the inner validator each
iteration. This is the general-purpose version (contrast with
validate_tot_nlist_recursive in LowParse.Pulse.Recursive which
handles recursive parsers with serialize_recursive_param).
* validate_vclist: validate a variable-count list (length prefix +
nlist). Reads the count via leaf_reader, bounds-checks it, then
delegates to validate_nlist. Requires fits_u64 for U32-to-SZ
conversion.
Validators NOT ported (with reasons):
- validate_deplen: parse_deplen requires a serializer in its type
signature (parse_deplen_data_t is parameterized by serializer)
- Sum/DSum validators (validate_sum, validate_dsum, ~20 helpers):
require complex dispatch infrastructure (enum tables, sum case
matching) not available in Pulse; the spec types themselves are
serializer-heavy
- Enum validators (validate_enum_key, validate_maybe_enum_key):
dependent on enum/sum infrastructure
- validate_ifthenelse: requires Low*-specific test_ifthenelse_tag
type; would need new Pulse-specific test infrastructure
- Error code variants (validate_with_error_code, etc.): Pulse
validators return bool, not error codes
- Low*-specific wrappers (validate_no_read, validate_with_comment):
no Pulse equivalent needed
- LowParse.Low.Int validators: omitted per user request; these are
validate_total_constant_size wrappers
- LowParse.Pulse.Recursive validators: already exist in Pulse and
require serialize_recursive_param (cannot remove serializer dep)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adapt LowParse.Pulse.Base.peek_trade_gen to PulseParse, replacing pts_to_serialized with pts_to_parsed. Requires ParserStrong. Given a successful validator result (offset, off), splits the input at offset and at offset+consumed to isolate the parsed sub-slice, uses parse_strong_prefix to establish the parse on the sub-slice, then pts_to_parsed_intro to produce a pts_to_parsed resource. Returns pts_to_parsed p input' #(pm /. 2.0R) v' with a trade back to pts_to input #pm v. Permission halving (pm /. 2.0R) is inherent to pts_to_parsed_intro for non-injective parsers. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the admit() in validate_sum_aux with a verified implementation following the Low.Sum pattern: - Call parse_sum_eq'' to decompose parse_sum into tag + payload parsing - Validate the tag with the tag validator - Read the tag value using read_parsed_from_validator_success (requires ParserStrong on the tag parser kind, added as squash parameter) - Connect sub-slice equivalence with Seq.lemma_eq_elim - Delegate to v_payload callback for payload validation/dispatch Also fix validate_sum_aux_payload_postcond for the Unknown case to include SZ.v off <= Seq.length v, which is required by validator_postcond even on failure. No admit() or assume left. Verified with --z3rlimit 64. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Port validate_sum_aux_payload', validate_sum_aux_payload, and validate_sum from LowParse.Low.Sum to Pulse: - validate_sum_aux_payload': Pulse fn with match on maybe_enum_key — for Known k, delegates to pc32 k; for Unknown, returns false - validate_sum_aux_payload: uses dep_maybe_enum_destr_t to dispatch the payload validation per tag repr value - validate_sum: top-level combinator wiring everything together Also fix validate_sum_aux to restore poffset on payload failure, since validate_sum_aux_payload_postcond for Unknown doesn't constrain the offset (needed by validator_postcond which requires SZ.v off <= len even on failure). Revert the postcondition strengthening that caused Pulse type-checking issues with Unknown instantiation. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Port all 12 BitSum validator combinators from LowParse.Low.BitSum to LowParse.PulseParse.BitSum, using Pulse's validator type (LPS.validator): Pure F* combinators (kept as Tot let definitions): - validate_bitsum': composes validate_filter + validate_synth - validate_bitsum_cases_t: type definition for case dispatch - validate_bitsum_cases_bitstop: leaf base case - validate_bitsum_cases_bitfield: intermediate bitfield node - validate_bitsum_cases_bitsum_gen: enum-based dispatch - validate_bitsum_cases_bitsum'_t: list iterator type - validate_bitsum_cases_bitsum'_intro: initialize list iteration - validate_bitsum_cases_bitsum'_nil: unreachable case (false_elim) - validate_bitsum_cases_bitsum'_cons: conditional case matching - mk_validate_bitsum_cases_bitsum'_t': recursive list traversal - mk_validate_bitsum_cases_t': recursive structure traversal Pulse fn (ported from Low* Stack effect): - validate_bitsum: main entry point — validates tag with validate_bitsum', reads tag via read_parsed_from_validator_success, dispatches to case validator via vs Key adaptations: - Dropped #rrel #rel sl pos validator args, return B.validator directly - Fixed universe: Type0 instead of Type u#r (Pulse validator requires Type0) - Added ParserStrong squash for leaf_reader-based tag reading - Reorder lemma calls (parse_synth_eq, parse_filter_eq) before read_parsed_from_validator_success to establish validator_success p - Restore poffset on failure for validator_postcond off bound No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add DSum validator combinators ported from LowParse.Low.Sum to Pulse: - validate_dsum_cases_t: type alias for DSum case validators - validate_dsum_cases_if'/validate_dsum_cases_if: if-combinator for dep_maybe_enum_destr_t dispatch (Pulse fn wrapping cond branch) - validate_dsum_cases': case validator using validate_synth for Known/Unknown - validate_dsum_cases_dispatch: pure Tot wrapper for destr call (needed because dep_maybe_enum_destr_t refinement checking fails inside Pulse fn bodies; mirrors validate_sum_aux_payload pattern) - validate_dsum: top-level Pulse validator for parse_dsum, validates tag, reads repr via read_parsed_from_validator_success, dispatches to case validator via destr, restores offset on failure Key technical insight: dep_maybe_enum_destr_t calls must happen in pure Tot context (not inside Pulse fn), because Pulse's type checker cannot prove the trivial refinement (eq_trivial) on the return type. Solution: extract the destr call into validate_dsum_cases_dispatch (pure Tot let), then call the resulting validator from the Pulse fn body. All verification conditions discharged, no admit() or assume used. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create LowParse.PulseParse.IfThenElse.fst with validate_ifthenelse ported from LowParse.Low.IfThenElse. Instead of the Low* test_ifthenelse_tag callback (which reads the tag from the buffer via Stack effect), uses a leaf_reader to read the tag via read_parsed_from_validator_success, then applies parse_ifthenelse_tag_cond to get the branch condition. Requires ParserStrong on the tag parser kind (squash parameter). No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create LowParse.PulseParse.ListUpTo.fst with validate_list_up_to ported from LowParse.Low.ListUpTo to Pulse. Uses a while loop that iterates: validate one element, read it via read_parsed_from_validator_success, check the termination condition. If cond is true, stop with success. If cond is false, advance and continue. If element validation fails, stop with failure. Loop invariant tracks consumed bytes: relates parse result at the initial offset to parse result at the current offset, ensuring the total consumed bytes are consistent across iterations. Requires ParserStrong on the element parser (for leaf_reader). No admit() or assume. Verified with --z3rlimit 32. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add serialized_of_leaf_reader: converts a PulseParse leaf_reader (works on pts_to_parsed p) to a Pulse leaf_reader (works on pts_to_serialized s), given a serializer. This is the reverse of the existing leaf_reader_of_serialized. The conversion uses pts_to_serialized_parsed to go from pts_to_serialized to pts_to_parsed, calls the PulseParse reader, then uses pts_to_parsed_serialized to convert back, chaining the trades. Together with the existing leaf_reader_of_serialized, this provides bidirectional conversion between the two leaf_reader types. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create LowParse.PulseParse.BCVLI.fst with both BCVLI validators ported from LowParse.Low.BCVLI: - validate_bcvli: validates variable-length integer (1/3/5 bytes). Validates 1-byte header with validate_total_constant_size, reads it via read_parsed_from_validator_success, then branches: - <253: value is header byte, done - 253: validate+read 2-byte LE payload, check non-malleability (>=253) - 254: validate+read 4-byte LE payload, check non-malleability (>=65536) - 255: error - validate_bounded_bcvli: same structure plus bounds checking (min/max). Early-rejects impossible branches based on bounds. Both take leaf_readers for parse_bounded_integer_le 1/2/4 as parameters, allowing callers to provide the appropriate readers. Restores poffset on failure for validator_postcond. No admit() or assume. Verified with --z3rlimit 32. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create LowParse.PulseParse.BoundedInt.fst with the constant-size bounded integer validators: - validate_bounded_integer (i): BE, sz=1/2/3/4 — validate_total_constant_size - validate_bounded_integer' (i): runtime-sized variant (needs fits_u64) - validate_bounded_integer_le (i): LE variant - validate_u16_le, validate_u32_le: LE integer validators The bounded int32 composite validators (validate_bounded_int32', validate_bounded_int32_le', validate_bounded_int32_le_fixed_size and their size-specialized variants) are NOT included because they require equational lemmas relating parse_bounded_int32 to parse_bounded_integer + filter, but the Spec.BoundedInt module does not expose these equations and its definitions are opaque due to caching (--already_cached). Adding parse_bounded_int32_eq to LowParse.Spec.BoundedInt.fsti would enable these validators. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add equational lemmas to LowParse.Spec.BoundedInt.fsti exposing the
compositional structure of parse_bounded_int32, parse_bounded_int32_le,
and parse_bounded_int32_le_fixed_size. These are needed because the
Pulse build caches Spec modules (--already_cached), making their .fst
definitions opaque. The Low* validators don't need these lemmas because
they use 'friend' with the uncached Spec module.
New equational lemmas in Spec.BoundedInt.fsti:
- parse_bounded_int32_eq: decomposes into parse_bounded_integer + filter
- parse_bounded_int32_le_eq: same for LE
- parse_bounded_int32_le_fixed_size_eq: decomposes into parse_u32_le + filter
New validators in PulseParse.BoundedInt (all 20 from Low.BoundedInt):
Constant-size (5):
- validate_bounded_integer, validate_bounded_integer' (BE)
- validate_bounded_integer_le (LE)
- validate_u16_le, validate_u32_le
Bounded int32 BE (4): validate_bounded_int32_{1,2,3,4}
Bounded int32 LE (4): validate_bounded_int32_le_{1,2,3,4}
Fixed-size LE (1): validate_bounded_int32_le_fixed_size
Each composite validator: validates constant-size bytes, reads value via
read_parsed_from_validator_success, checks bounds, restores poffset on
failure. Uses the new equational lemmas to connect the parse result.
No admit() or assume (except fits_u64 in validate_bounded_integer').
Verified with make lowparse.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add the remaining BoundedInt validators to PulseParse: - validate_bounded_int32': generic BE, takes sz + sub-validator + reader - validate_bounded_int32_le': generic LE variant - validate_bounded_int32: runtime dispatcher, branches on max32 to call _1/_2/_3/_4 - validate_bounded_int32_le: LE runtime dispatcher The generic versions take sz as integer_size with refinement sz == log256' max, plus the base validator and leaf_reader for parse_bounded_integer sz. The caller provides the concrete sz. The dispatchers take all 4 leaf_readers and branch at runtime. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add three FLData validators: - validate_fldata_gen: alias for validate_fldata (already handles non-ConsumesAll parsers via consumed == sz check) - validate_fldata_consumes_all: alias for validate_fldata with ParserConsumesAll squash (existing impl handles both cases) - validate_fldata_strong: validates parse_fldata_strong s sz, which refines parse_fldata with a serializer length predicate. F* sees through coerce_parser/parse_strengthen/bare_parse_strengthen to connect the postcondition directly to validate_fldata. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add three VLData validators: - validate_vldata_payload: wraps validate_fldata with validate_weaken for the vldata_payload parser kind - validate_bounded_vldata_strong': validates parse_bounded_vldata_strong' by delegating to validate_bounded_vldata' (F* sees through coerce_parser/parse_strengthen) - validate_bounded_vldata_strong: default log256' version No admit() or assume (except fits_u64). Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create three new PulseParse modules: LowParse.PulseParse.VLGen.fst (3 validators): - validate_bounded_vlgen: Pulse fn — validates length prefix, reads it via read_parsed_from_validator_success, delegates to validate_fldata_strong - validate_vlgen: validate_synth wrapper over validate_bounded_vlgen with synth_vlgen coercion - validate_vlgen_weak: Pulse fn — like validate_bounded_vlgen but uses validate_fldata (no serializer constraint on payload) LowParse.PulseParse.Bytes.fst (5 validators): - validate_flbytes: validate_total_constant_size wrapper - validate_all_bytes: Pulse fn — accepts all remaining bytes - validate_bounded_vlbytes': validate_synth over validate_bounded_vldata_strong' with synth_bounded_vlbytes - validate_bounded_vlbytes: default log256' wrapper - validate_bounded_vlgenbytes: validate_synth over validate_bounded_vlgen with serialize_all_bytes LowParse.PulseParse.Array.fst (3 validators): - validate_array': validate_synth over validate_fldata_strong + validate_list with fldata_to_array - validate_array: total constant-size when metadata is Total, otherwise delegates to validate_array' - validate_vlarray: validate_synth over validate_bounded_vldata_strong + validate_list with vldata_to_vlarray No admit() or assume (except fits_u64). Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create LowParse.Pulse.DepLen.fst with validate_deplen ported from LowParse.Low.DepLen. This goes in LowParse.Pulse (not PulseParse) because parse_deplen requires a serializer in its type definition. The validator: 1. Validates header with hv, reads it via read_from_validator_success 2. Computes payload length with dlf(header_value) 3. Checks remaining bytes >= payload_len 4. Splits input at off1 + payload_len, validates payload in sub-slice 5. Checks consumed == payload_len 6. Uses serializer_correct_implies_complete to establish the Seq.length(serialize ps t) == consumed condition needed by parse_deplen_unfold2 Requires ParserStrong on header parser (for reading) and fits_u64. No admit() or assume (except fits_u64). Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create two new modules: LowParse.PulseParse.Int.fst (3 validators): - validate_u64_le: validate_total_constant_size (8 bytes LE) - validate_int32le: validate_total_constant_size (4 bytes LE) - validate_constint32le: validates parse_int32le then reads and compares value against expected constant. Takes leaf_reader for parse_int32le. LowParse.Pulse.DER.fst (2 validators, serializer-based): - validate_der_length_payload32: multi-branch DER length payload validator. Branches on tag byte: <128 (zero payload), 129 (1-byte u8 payload), 130-132 (2/3/4-byte bounded_integer payload). Checks non-malleability (value >= pow2(8*(len-1))). - validate_bounded_der_length32: validates u8 tag, checks tag range against min/max bounds, then inlines the DER payload validation + bounds checking in one pass. Both DER validators take leaf_reader serialize_u8 and a function providing leaf_reader (serialize_bounded_integer i) for each size. No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add jumper implementations across 13 files, porting from LowParse.Low.*
to LowParse.Pulse.* and LowParse.PulseParse.* modules.
Tier 1 - Constant-size jumpers:
- BoundedInt: jump_bounded_integer, jump_bounded_integer_le,
jump_u16_le, jump_u32_le, jump_bounded_int32_{1,2,3,4},
jump_bounded_int32_le_{1,2,3,4}, jump_bounded_int32_le_fixed_size
- Int: jump_u64_le, jump_int32le, jump_constint32le
- Bytes: jump_flbytes, jump_all_bytes
- FLData: jump_fldata_strong
Tier 2 - Simple wrappers:
- VLData: jump_vldata_gen, jump_bounded_vldata', jump_bounded_vldata,
jump_bounded_vldata_strong', jump_bounded_vldata_strong
- VLGen: jump_bounded_vlgen, jump_vlgen
- Bytes: jump_bounded_vlbytes', jump_bounded_vlbytes,
jump_bounded_vlgenbytes
- Enum: jump_enum_key, jump_maybe_enum_key
- IfThenElse: jump_ifthenelse
Tier 3 - Complex jumpers:
- BCVLI: jump_bcvli, jump_bounded_bcvli
- DER: jump_der_length_payload32, jump_bounded_der_length32
- Sum: jump_sum_cases_aux, jump_sum_cases, jump_sum_aux, jump_sum,
jump_dsum_cases', jump_dsum_cases_dispatch, jump_dsum
- VCList: jump_vclist
- Array: jump_array, jump_vlarray
All 29 Pulse module files verified successfully with no admits.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create share/everparse/tests/lowparse/ with: - Makefile: build system for Pulse LowParse tests, includes lowparse/pulse in the path - LowParseTestLib.Pulse.fst: test library with test_validator_accept and test_validator_reject functions (stubs with admit for now, implementations will be in C at extraction time) - LowParseTestLib_Pulse_c.c: C implementations of print_string, exit_failure, and load_file utility This provides the foundation for porting Low* LowParse tests from tests/lowparse/ to Pulse. Test functions take a validator, a test name, and a byte slice, then check whether the validator accepts/rejects as expected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add zero_copy_parse type and combinators using pts_to_parsed (parser-only) instead of pts_to_serialized (serializer-based). LowParse.PulseParse.Base.fst (8 definitions): - pts_to_parsed_with_perm: analog of pts_to_serialized_with_perm - zero_copy_parse: type taking parser p instead of serializer s, producing vmatch res v with trade back to pts_to_parsed p input - zero_copy_parse_id: returns input with pts_to_parsed_with_perm - zero_copy_parse_lens: transforms vmatch via lens - zero_copy_parse_read: uses PulseParse leaf_reader p - zero_copy_parse_ignore: ignores parsed value - zero_copy_parse_ext: parser extensionality - zero_copy_parse_ifthenelse: conditional dispatch LowParse.PulseParse.Combinators.fst (5 definitions): - zero_copy_parse_synth: for parse_synth - zero_copy_parse_filter: for parse_filter - zero_copy_parse_nondep_then: pairs two parsers, uses jumper for p1 to compute split point (replaces serializer-based split) - zero_copy_parse_dtuple2: dependent pair, uses jumper - read_and_zero_copy_parse_dtuple2: reads first, zero-copy second Key differences from serializer-based versions: - Permission halving: pts_to_parsed_intro gives pm /. 2.0R - Jumpers replace serializer-computed split points - No serializer dependency in types No admit() or assume. Verified with make lowparse. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add zero_copy_parse combinators that port Low* accessor patterns (accessor_fst, accessor_snd, etc.) to PulseParse using zero_copy_parse from LowParse.PulseParse.Base. Combinators (LowParse.PulseParse.Combinators.fst): - zero_copy_parse_fst: extract first field of nondep_then - zero_copy_parse_snd: extract second field of nondep_then - zero_copy_parse_dtuple2_fst: extract first field of dtuple2 FLData (LowParse.PulseParse.FLData.fst): - pts_to_parsed_fldata_payload_trade: ghost conversion between parse_fldata and underlying parser predicates - zero_copy_parse_fldata: lift zero_copy_parse through parse_fldata VLData (LowParse.PulseParse.VLData.fst): - zero_copy_parse_bounded_vldata_payload': access payload of bounded vldata by reading length prefix, splitting slice, and delegating to the underlying zero_copy_parse - zero_copy_parse_bounded_vldata_payload: convenience wrapper with default log Sum (LowParse.PulseParse.Sum.fst): - read_sum_tag: read the tag from a parsed sum value - vmatch_sum_payload: vmatch type for sum payload access - zero_copy_parse_sum_payload: access payload of a sum for a known tag by jumping past the tag and zero-copy parsing the case payload Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Create share/everparse/tests/lowparse/LowParseExample3.Pulse.fst —
Pulse port of tests/lowparse/LowParseExample3, demonstrating:
- Spec-level type definition: t = { a: U16.t; b: U32.t; c: U16.t }
- Parser: parse_synth (nondep_then (nondep_then parse_u16 parse_u32) parse_u16) synth_t
- PulseParse leaf_readers via leaf_reader_of_serialized
- PulseParse validator via validate_synth + validate_nondep_then
- Test function 'dummy': validates input, then reads individual
fields (a/b/c) by re-validating sub-parsers at known offsets
and using read_parsed_from_validator_success
Also fix Makefile to include both lowparse spec and pulse paths.
No admit() or assume. Verified with make.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Rewrite LowParseExample3.Pulse to use composed zero_copy_parse accessors instead of re-validating sub-parsers at known offsets: - access_a: zero_copy_parse_synth + zero_copy_parse_fst (outer) + zero_copy_parse_fst (inner) + zero_copy_parse_read - access_b: zero_copy_parse_synth + zero_copy_parse_fst (outer) + zero_copy_parse_snd (inner) + zero_copy_parse_read - access_c: zero_copy_parse_synth + zero_copy_parse_snd + zero_copy_parse_read The dummy test function: 1. Validates with validate_t 2. Uses peek_trade_gen to get pts_to_parsed sub-slice 3. Calls the appropriate accessor (access_a/b/c) 4. Eliminates the trade chain (accessor trade -> peek trade) Uses simple vmatch_a/b/c aliases (pure (x == v.field)) for clean unfold at the call site. No admit() or assume. Verified. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace R.alloc/R.free with let mut for the validator offset reference. Cleaner and avoids deprecation warnings. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add extractable test and main functions: - test(): creates an 8-byte array using let mut + array initializer syntax ([| 0uy ; 8sz |]), converts to slice with from_array, writes test bytes through slice indexing, calls dummy to validate and read fields, then converts back with to_array. - main(): calls test(), returns EXIT_SUCCESS. These are designed to be extracted to C and run as an executable test. No admit() or assume. Verified. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Rename LowParseExample3.Pulse.fst to LowParseExample3.fst (matching the Low* naming convention, dropping the .Pulse suffix). Update Makefile with extraction rules: - verify target: F* verification via common.Makefile - extract-all: extracts to C via KaRaMeL, compiles, and runs - Uses -bundle and -no-prefix for clean C output - FSTAR_DEP_OPTIONS with Pulse extraction settings The test successfully extracts to C, compiles, and runs: make Example3 → Example3/a.out runs and exits 0 Add .gitignore for build artifacts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- QD: Use validate_dsum_cases_fn/jump_dsum_cases_fn with dep_maybe_enum_destr_t_tac (handles both Known and Unknown branches via tactic) instead of validate_dsum_cases/jump_dsum_cases with dep_enum_destr_tac (Known only, Unknown handled by manual match that caused PCMReference.read leak during extraction) - QD: Add inline_for_extraction to parse_cases definitions - QD: Make synth_cases/synth_cases_recip/synth_known_cases noextract when -pulse is active (no SLow code generated) - QD: Make -pulse automatically disable SLow (emit_high := false) - QD: Suppress KaRaMeL warning 26 in extracted.Makefile - PulseParse.Sum: Make f (parse_cases) argument Ghost.erased in validate_dsum_cases_t, validate_dsum_cases_if, validate_dsum_cases', validate_dsum_cases_dispatch, validate_dsum_cases'_destr, validate_dsum_cases, validate_dsum_cases_fn, and all jump_dsum_* counterparts - PulseParse.Sum: Convert validate_dsum_cases' to Pulse fn with direct g' call in Unknown branch (no B.validate_synth wrapper) - PulseParse.Combinators: Eta-expand validate_compose_context and jump_compose_context (matching Low* pattern) - PulseParse.Combinators: Add inline_for_extraction to jump_compose_context - Pulse.Base: Eta-expand validate_ext Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- QD: Generate Pulse leaf_reader for enum types using PPE.mk_read_enum_key / PPE.mk_read_maybe_enum_key + read_synth' - QD: Generate Pulse leaf_reader for struct types using PPC.leaf_read_nondep_then composition + read_synth' - QD: Move Pulse reader generation after validator generation to satisfy F* definition ordering requirements - QD: Make synth_cases/synth_cases_recip/synth_known_cases noextract when -pulse (no SLow), add inline_for_extraction to parse_cases - QD: Make -pulse disable SLow (emit_high := false) - QD: Suppress KaRaMeL warning 26 in extracted.Makefile Note: sum/dsum leaf_readers (read_sum, read_dsum) not yet implemented in PulseParse - T38/T39/T40/T41/T15_body readers still Low*-only. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add leaf_reader dispatch infrastructure for sum types: - read_sum_cases_t: type alias for per-key leaf_reader - read_sum_cases_t_if': Pulse fn for if-combinator dispatch - read_sum_cases_t_if: if_combinator wrapper - read_sum_cases': per-key reader using read_synth' + synth_sum_case - read_sum_cases: dep_enum_destr-based dispatch The full read_sum combinator (read tag + jump + dispatch) is not yet implemented due to ghost ownership management complexity with pts_to_parsed narrowing from parse_sum to parse_sum_cases'. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Read a sum type value by: 1. Reading the tag with read_sum_tag 2. Getting the payload sub-slice with accessor_clens_sum_payload 3. Reading the raw case value with pc32 k 4. Trading back to restore original ownership 5. Applying synth_sum_case to produce the sum value Also includes read_sum_cases infrastructure (read_sum_cases_t, read_sum_cases_t_if, read_sum_cases', read_sum_cases) for dep_enum_destr-based dispatch, though read_sum itself uses the simpler accessor-based approach. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ssors - Add read_dsum leaf_reader: uses accessor_dsum_tag to read tag, accessor_clens_dsum_payload to get payload sub-slice, then reads Known/Unknown case directly with f32/g32 and applies synth_dsum_case - Make f parameter Ghost.erased in all dsum accessor combinators: accessor_dsum_tag, accessor_clens_dsum_payload, accessor_clens_dsum_payload', accessor_clens_dsum_unknown_payload, accessor_clens_dsum_unknown_payload', accessor_clens_dsum_cases_known_payload, accessor_clens_dsum_cases_unknown_payload Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- PulseParse.Combinators: add read_false() leaf_reader for parse_false - QD: Generate Pulse read_cases for sum/dsum types - QD: Generate Pulse read_sum/read_dsum calls for sum/dsum readers - QD: Fix pulse_leaf_reader_name for Empty (PPC.leaf_read_empty) and Fail (PPC.read_false ()) All types verify and extract to .krml. C compilation has a KaRaMeL issue with sum reader return type initialization in T39.c. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Generate PulseParse accessor tree using PPC.accessor_then_fst, PPC.accessor_then_snd, PPC.accessor_id, PPC.accessor_compose, PPC.accessor_ext, PPC.accessor_synth_inv - Generate clens definitions using LowParse.CLens - No gaccessor needed (PulseParse doesn't have it) All 44 types verify, extract to C, compile, link, and test passes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Generate Pulse accessor for vlgen payload types using PPVG.accessor_vlgen_payload with jumper and leaf_reader for the length header. All 44 types verify, extract, compile, link, and test passes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- PulseParse.Combinators: add clens_synth_fwd and accessor_synth_fwd for forward synth direction (p → parse_synth p f) - QD: Generate Pulse tag accessors using PPS.accessor_sum_tag/dsum_tag composed with accessor_synth_fwd for the user-defined tag type - QD: Generate Pulse payload accessors using PPS.accessor_clens_sum_payload/dsum_payload with accessor_ext - QD: Generate Pulse Unknown payload accessors using PPS.accessor_clens_dsum_unknown_payload with accessor_ext - QD: Generate clens definitions using LowParse.CLens for Pulse All 44 types verify, extract, compile, link, and test passes. Low* quackyducky tests also pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Write a non-dependent pair by writing the first component then the second. Proves the Seq.slice composition postcondition using slice_slice, lemma_split, and lemma_eq_intro. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- LowParse.Pulse.Base: extract l2r_leaf_writer postcondition into l2r_leaf_writer_postcond prop; add l2r_leaf_writer_ext_squash variant taking parser equivalence as separate squash argument - LowParse.Pulse.Combinators: add l2r_leaf_write_enum_key, l2r_leaf_write_maybe_enum_key (enum writers using destructor); l2r_leaf_write_sum_cases_t/_aux/_cases (sum case dispatcher); l2r_leaf_write_false (unreachable type writer) - LowParse.Pulse.Sum (new): l2r_leaf_write_sum and l2r_leaf_write_dsum Pulse fn writers that sequentially write tag then payload, with squash lemmas for precondition/postcondition bridging; l2r_leaf_write_dsum_type_of_tag/_cases_aux/_cases (dsum helpers) - QD codegen (rfc_fstar_compiler.ml): generate Pulse writers wherever Low* generates lserializers - enum writers (l2r_leaf_write_enum_key + l2r_leaf_write_synth), struct writers (l2r_leaf_write_nondep_then + l2r_leaf_write_synth), sum writers (l2r_leaf_write_sum with dep_enum_destr_tac), dsum writers (l2r_leaf_write_dsum with dep_enum_destr_tac), type alias writers; add pulse_leaf_writer_name mapping, write_cases table generation, LPPS module alias Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Mark implicit parser_kind arguments as Ghost.erased in PulseParse.Bytes, PulseParse.Combinators, PulseParse.VCList, and PulseParse.VLGen to avoid top-level ghost effects (Warning 272) that prevent F* extraction to .krml. Add --warn_error '+272' to extracted.Makefile to catch top-level effect issues early. bitcoin.rfc types now fully verify, extract, compile, link, and run. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
force-pushed
the
_taramana_pulse_parse
branch
from
5e89c6b to
6de4df8
Compare
Member
Author
|
Some accessors are missing: array_nth and the like |
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.
In light of the upcoming deprecation of Low*, this PR is porting LowParse combinators to Pulse.
This PR is also porting some LowParse.Pulse combinators from ACM CCS 2025 to a new separation logic predicate,
pts_to_parsed, which relies on the parser specification rather than the serializer specification, so that (most of) those combinators can be used with non-injective parsers.Coarse-grained roadmap:
Left unported: offset reasoning and finalizers for serialization. These should be replaced with wholesale serializers, from our ACM CCS 2025 paper