Port 3D from Low\* to Pulse (--pulse) - #318
Open
tahina-pro wants to merge 104 commits into
Open
Conversation
…reuse Ports funptr, ifdefs, iter, tcpip, goto_return and the four specialize tests to --pulse. All fifteen ported subdirectories now build, link and run as part of the pulse suite. The specialize tests exposed a real bug. Low* probe_then_validate calls the validator for the probed type at position 0uL, because there the position is an argument rather than part of the buffer. The Pulse port passed the copy buffer position ref instead, so a copy buffer reused at a second probe site was validated from wherever the first probe left it, and the second validation reported not enough data. The copy_buffer class gains a reset method, and probe_then_validate rewinds before validating. The other adaptations follow from ABI changes already made: - A copy buffer is now the buffer backend input buffer passed by value, so clients read cb_base and cb_len instead of casting to a descriptor of their own, and supply a position cell. - The extern and static primitives no longer take the application context, so funptr moves its vtable into the stream object. The test is unchanged in substance: no stream operation is resolved at link time. - The goto_return snapshot is regenerated for the three input buffer arguments and the uint8_t status code. Two subdirectories stay out. probe and probe_error_handler_macro build the z3 test-case generator, which still uses the Low* interpreter, and their ProbeInPlace callback repoints the copy buffer at the source instead of copying into it, which a by-value copy buffer cannot express. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This definition failed to verify at the rlimit of 16 granted by the enclosing push-options block, which broke the Low* 3d prelude and hence the whole Low* test suite. It verifies deterministically at 128. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Two optimizations present in the Low* prelude had no Pulse counterpart.
validate_nlist_total_constant_size{,_mod_ok,_mod_ko}: when the payload has
total constant size, the whole list does too, so validating it is a single
bounds check rather than an element loop. validate_nlist_constant_size_
without_actions accepted payload_is_constant_size but ignored it.
validate_dep_pair_with_refinement{,_and_action}_total_zero_parser: when the
tag parser is total and consumes no input it can neither fail nor consume, so
the tag validator is skipped and the leaf reader runs directly. Here too the
p1_is_constant_size_without_actions argument was accepted and ignored.
The Pulse interpreter now passes not ha1 for that flag, where ha1 is the
has_action index of the tag dtyp: that is exactly the without-actions
criterion, and it is known at specialization time. The Low* interpreter
hard-codes false there, so the optimization was unreachable on its
interpreted path.
UINT8 f1[10] in TestFieldPtr.3d now generates a single bounds check with no
loop. The full share/everparse/tests/3d suite still passes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
package.sh now copies everything 3d.exe --pulse looks up relative to EVERPARSE_HOME: lib/everparse/3d (sources and .checked), its extracted .krml files, the Pulse stdlib, and the EverParsePulse headers. The Pulse stdlib copy moves out of the EVERPARSE_ONLY_3D block so that the 3d-only release package supports --pulse too. The root Makefile adds 3d-pulse-krml to the packaged subset, guarded by NO_PULSE. Validated against a simulated package tree with PULSE_HOME, KRML_EXE, FSTAR_EXE and EVERPARSE_HOME unset: all paths resolve inside the package and the generated C compiles. Adds a Test EverParse (--pulse) step to all six binary-package test jobs. Inputs come from share/everparse/tests/3d so that --check_hashes inplace does not clobber the hashes the Low* step just wrote. The --z3_test steps get no --pulse counterpart, since Z3TestGen still uses the Low* interpreter. FieldDependence0.3d is deliberately omitted from the --pulse steps: it verifies fine but fstar --codegen krml on the generated module runs away past 32GB. It is excluded from positive_tests in both suites, so this is a pre-existing gap rather than a regression. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The previous commit covered package-{linux,macos,windows}.yml and the
three release.yml test jobs, but missed nightly.yml, which has the same
three binary-package test jobs, and the cross-platform hash interop
jobs in both nightly.yml and release.yml.
Each test job now also uploads everparse-test-pulse-<os>, holding the
--pulse Comments*, and each interop job downloads it into <os>-pulse/
and re-runs --pulse --check_hashes inplace there. A separate artifact
is needed because both files are called Comments.3d: putting them in
one artifact would move the archive root and break the existing Low*
interop steps.
nightly-fstar2.yml, ci.yml, ci-macos.yml and cbor.yml need no change:
they run the in-tree make test, which already reaches 3d-pulse-test.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
FieldDependence0.3d generated and verified fine under --pulse, but "fstar.exe --codegen krml" on the generated module never finished: it reached 166 GB RSS after 50 minutes, and died with "allocation failure during minor GC" under a 32 GB cap. Root cause: the generated "kind_X" definitions are left as an unreduced nest of "and_then_kind" / "glb" applications. Those two functions build a parser_kind record whose four fields each mention their arguments, so "and_then_kind k1 k2" mentions k2 six times and k1 four times. They are "inline_for_extraction", so F* extraction unfolds the whole nest, and the term grows exponentially with its depth. That is why the blowup needed both a casetype mixing strong-prefix and weak cases (deep "glb" nest) and preceding struct fields (deep "and_then_kind" nest): a bisection over (number of cases) x (number of preceding fields) shows the cost is multiplicative in the two, while all-strong-kind casetypes and plain field chains of any depth stay flat. Fix: wrap the kind expression in a "norm" that reduces the nest to a literal record. Extraction of FieldDependence0.validate__s2 goes from 129 s (then OOM) to 57 ms, and the whole file now builds in 20 s / 1.2 GB. The normalization is restricted to the EverParse3d and LowParse namespaces. A plain "delta" also works for FieldDependence0 but changes which branch of validate_nlist_constant_size_without_actions is selected for ELF.3d, leaving a reference to Pulse.Lib.Array.Core.mk_carrier that KaRaMeL cannot compile. Only the --pulse output changes; the Low* generated F* is byte-identical. FieldDependence0.3d is therefore re-enabled in the --pulse steps of the binary-package tests in all five workflows. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The Pulse test suite excluded only FineGrainedProbe, Specialize2, Specialize3 and Specialize5 on Windows, but src/3d/tests also excludes FineGrainedProbeSpecialize and Specialize6 for the same reason (UlongToPtr is defined in Windows DLLs and conflicts with those examples). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Ports the remaining src/3d/tests scenarios that had no --pulse counterpart: - elf-test: build and link the C++ TestELF.cpp driver against the --pulse-generated ELF parser (not run, as in src/3d/tests: it needs an ELF file to read). - pulse-cc now goes through the Makefile.basic that KaRaMeL emits, so the generated C is held to the same -Wall -Wextra -Werror standard as the Low* suite, and links and *runs* test.cpp. This is the first time a --pulse-generated validator is executed by the test suite. - pulse-cleanup-test: --cleanup --skip_c_makefiles must leave behind exactly the C artifacts. Compared to Low*, the expected set also has EverParse.c, EverParse.h and internal/, because the Pulse backend extracts EverParseErrorReasonOfResult as a real function rather than a static inline in the hand-written prelude header. - pulse-inplace-hash-test: --check_hashes inplace and --check_inplace_hash on Comments.3d. - pulse-batch now saves strong hashes and re-checks them, as batch-test does for the Low* backend. Also factors the Windows exclusions into an exclude_modules list, so that the cleanup expected-file list drops the same modules. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Main.fst passed (print_c_initializers, use_ptr) to Z3TestGen.do_test and do_diff_test, but both callees declare their parameters in the order (use_ptr, print_c_initializer). Z3TestGen.do_diff_test contained a second, compensating swap when forwarding to do_diff_test_for. Net effect: do_test was wholly wrong, while do_diff_test was correct except for the cout_test_probe_functions call, which received the wrong flag. Both parameters are bool, so the mistake typechecked silently. The bug was masked because every existing test sets both flags to the same value: src/3d/tests/probe/src passes --z3_use_ptr without --z3_skip_c_initializers (both true), and the ELF z3-testgen test passes neither (both false). Any single-flag or mixed-flag invocation misbehaved: --z3_use_ptr --z3_skip_c_initializers silently fell back to array-index probe mode and also ignored --z3_skip_c_initializers. Verified: --z3_use_ptr --z3_skip_c_initializers on Probe.3d now emits the pointer-mode copy_buffer_t typedef together with the pointer-patching statements and no designated initializers in the echoed witness. The existing probe and z3-testgen tests are unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
--z3_test, --z3_diff_test and --test_checker now work under --pulse.
The SMT half needed no change: Z3TestGen.produce_decls consumes the
InterpreterTarget AST, which is backend-independent. Only the emitted C
harness was Low*-specific. Bridge the ABI differences:
- Pulse validators return a uint8_t status (0 on success) and report the
consumed length through a size_t* position, rather than returning the
consumed length or an error code.
- Their error handler takes the input as a (base, len, pos) triple instead
of an EVERPARSE_INPUT_BUFFER, and error codes are uint8_t.
- EverParseIsError and EVERPARSE_INPUT_BUFFER do not exist under --pulse.
- KaRaMeL only declares EVERPARSE_COPY_BUFFER_T when the module actually
uses it, so cout_test_probe_functions must emit nothing under --pulse.
This is what made probe-free modules fail to compile.
Reject two combinations rather than emitting C that does not compile:
--z3_use_ptr with --pulse (rejected in Main.go before any file is written),
and parsers taking a copy buffer. Both have the same root cause: the Pulse
EVERPARSE_COPY_BUFFER_T is passed by value, so a probe callback cannot
repoint it, which is exactly what pointer mode relies on.
To make the second rejection abort cleanly, produce_z3_and_test_gen gained a
pre_check parameter, run on the main thread before with_z3_thread_or spawns
the Z3 worker. A failure raised from that worker printed its message but let
the rest of the batch keep running, so the build failed later at link time
with an unrelated error.
Verified on ELFTestGen._ELFTestGen with --z3_witnesses 10 --z3_branch_depth 5:
both backends produce byte-identical witnesses and an identical sequence of
170 ACCEPTED/REJECTED verdicts. The harness compiles under -Wall -Wextra
-Werror -std=c11 and runs. --test_checker likewise agrees on verdict and exit
code across backends.
Reported positions do differ: Low* passes each field's start position to the
error handler, whereas Pulse has no such parameter and reports the current
position. The harness matches what the generated *Wrapper.c error handler
already does.
Add pulse-z3-testgen-test to share/everparse/tests/3d, mirroring the Low*
z3-testgen-test. There is no counterpart to z3-testgen-probe-test.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
A Pulse copy buffer was the buffer backend's input buffer itself, a by-value (base, len, pos) triple whose components were pure projections of an immutable handle. Neither the C ABI nor the spec could then express a probe callback repointing the buffer at the probed bytes, which is what in-place probing does in Low*, where copy_buffer_t is an abstract type behind a void* and stream_of is a spec-only projection. Put one reference between the handle and the triple, above the input stream class so that probe_then_validate still runs the same validator, with the same input_stream_inst, on the copy buffer. The input stream specs and instances are untouched. EverParse3d.CopyBuffer: the class now carries a descriptor type and its three projections, plus a descr handle -> ref descr_t. pts_to quantifies the descriptor existentially, so a probe function's postcondition admits a new one without its signature changing, and the caller never learns which region the buffer points at. The descriptor type is a class field rather than a record here so that each backend picks a monomorphic one: a polymorphic record is monomorphized by KaRaMeL under a mangled name, emitted into whichever generated module uses it first. EverParse3d.InputStream.Buffer: copy_buffer_descr is that record, and copy_buffer_t a ref to it. KaRaMeL emits EVERPARSE_COPY_BUFFER_DESCR into EverParse.h and inlines the abbreviation, so EverParsePulseEndianness.h defines EVERPARSE_COPY_BUFFER_T as a pointer to it. Test clients that used to build a copy buffer by value now allocate a descriptor and pass its address; the ones that include EverParseEndianness.h directly now go through EverParsePulseEndianness.h, so the legacy void* typedef stays suppressed whatever the include order. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Now that EVERPARSE_COPY_BUFFER_T is an indirection, a probe callback can repoint it, so --pulse no longer has to reject probes in z3-testgen. Z3TestGen: add --pulse variants of the probe harness. The harness copy_buffer_t embeds an EVERPARSE_COPY_BUFFER_DESCR as its first member so that callbacks can cast the copy buffer back to it; EverParseStreamOf and EverParseStreamLen are no longer emitted, since the validator reads cb_base/cb_len/cb_pos directly. The definitions are only emitted for modules that actually have probes, because KaRaMeL only puts the descriptor type in EverParse.h for those. Drop check_pulse_supported, the pre_check parameter of produce_z3_and_test_gen, and the --z3_use_ptr rejection in Main. Target: the probe wrapper reads probeDest->cb_base under --pulse instead of calling EverParseStreamOf. tests: port share/everparse/tests/3d/probe and probe_error_handler_macro to --pulse, and add a pulse-z3-testgen-probe-test target covering both the default and the --z3_use_ptr harness modes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replaces the reference-to-descriptor indirection with the Low* shape: an abstract copy_buffer_t plus assumed projections that the client implements in C. The earlier objection to this -- that pure projections cannot express a repointing probe -- was wrong: the pre and post of a probe differ in the stream contents, so a probe does change the slprop. What had actually broken was purely a C-level problem, namely that EVERPARSE_COPY_BUFFER_T was a by-value struct that a callee could not repoint. An opaque void* handle can be repointed, and EverParseStreamOf then returns the new pointer, which is exactly how the Low* backend behaves. The copy_buffer class loses descr_t, descr and the existential in pts_to, keeping only base_of/len_of/pos_of and reset. The buffer backend assumes the type and the three projections, named so that the EverParse bundle renames them to EverParseStreamOf, EverParseStreamLen and EverParseStreamPos. The first two are the Low* hooks verbatim, modulo EverParseStreamLen returning size_t since Pulse stream lengths are SZ.t; the third has no Low* counterpart and returns the position cell, which Low* validators instead take as an argument. Consequently EVERPARSE_COPY_BUFFER_T is void* again, straight from EverParseEndianness.h, so EverParsePulseEndianness.h no longer redefines it -- which removes the include-order conflict that had forced six hand-written test stream headers to change includes. It does republish the three prototypes, because KaRaMeL emits them into internal/EverParse.h rather than the public header, and without them a client's definitions would not be signature-checked. Target and Z3TestGen drop their --pulse special cases for probes, and probe_then_validate and the ProbeActions error handler lose their reference bookkeeping. Client C code is now source-compatible with Low* apart from adding EverParseStreamPos and widening EverParseStreamLen to size_t; the probe and specialize test clients are updated accordingly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The subdirectory Makefiles were copied from src/3d/tests, where a rule that compiles a hand-written .c file lists the generated wrapper header it includes, but not EverParse.h. Under the Low* backend that is harmless: EverParse.h is copied from the prelude by the same copy_everparse_h step that produces EverParseEndianness.h, at the very start of the pipeline, so by the time any wrapper header exists it is already there. Under --pulse it is not copied at all. KaRaMeL emits it, carrying the bundled runtime, at the same time as the generated .c files -- that is, at the very end. The prerequisite list is then genuinely wrong, and a parallel build compiles main.c as soon as the wrapper header appears, failing with "EverParse.h: No such file or directory". A serial build only masked this by accident of ordering. The generated EverParse.Makefile already models this correctly; only the hand-written rules were missing it. With them fixed, the whole suite passes from clean under -j16, in about a third of the serial time. Also drops a comment that still described copy buffers as an indirection. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The Pulse suite copied src/3d/tests' exclusion of FieldDependence0.3d and ActAndCheck.3d from positive_tests, but not the second batch target that covers them, so ActAndCheck.3d was exercised nowhere. That split is historical. 3D used to have two translation backends, Translate.fst (specialized) and TranslateForInterpreter.fst, and :act/:check were only ever supported by the latter, so ActAndCheck.3d was excluded from positive_tests by the very commit that added it (7b2764b). Translate.fst is long gone -- Main.fst only calls TranslateForInterpreter.translate_decls -- so batch-test and batch-interpret-test now drive the same pipeline and differ only in which files they feed it. Mirror it anyway, so this Makefile stays diffable against src/3d/tests and so that pulse-cleanup-test keeps asserting an exact output file list over the narrower set. The new target needs its own output directory, because EverParse.h is generated per batch and carries that batch's external typedefs. Unlike the Low* version it needs neither --no_copy_everparse_h nor a copy of the auxiliary headers: -I $(CURDIR) already finds them. interpretable_tests also drops exclude_modules, which INTERPRETABLE_FILES fails to do; those modules do not build on Windows for a reason unrelated to which files a target selects. Both extra modules generate, verify, extract, compile and link under --pulse with no change to the prelude or the frontend. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When the --pulse package tests were added, the --z3_test steps were deliberately left without a counterpart, because Z3TestGen only emitted a Low* harness. That stopped being true once it learned to emit a Pulse one and then to handle probes, but the workflows were never revisited, so nine ELFTestGen steps and three probe steps stayed Low*-only across all five workflows. This is worth covering rather than assuming it follows from the in-tree suite: the emitted harness is where the two backends diverge most. Pulse validators return a uint8_t status and report the consumed length through a size_t* position, and the probe harness additionally defines the copy-buffer hooks, including EverParseStreamPos, which has no Low* counterpart. None of that C is compiled by any other packaged test. Each new step mirrors its Low* neighbour exactly, taking its input from share/everparse/tests/3d rather than src/3d/tests, as the other --pulse steps already do, and writing to its own --odir so the two runs cannot collide. All nine affected jobs already sparse-checkout the Pulse corpus. Both commands were run locally against the source tree first. The probe steps remain Windows-only, as they have been since they were introduced; this change does not widen their platform coverage. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The C generated by `3d --pulse` is self-contained: the Pulse runtime is bundled into EverParse.c/EverParse.h, and nothing refers to krmllib. But KaRaMeL's misc/Makefile.basic unconditionally puts krmllib's headers on the include path and links every executable against libkrmllib.a, which a KaRaMeL built with LOWSTAR=false does not even produce -- so linking the z3 test-case generation harness failed. Rather than patch KaRaMeL, ship our own: - share/everparse/3d/Makefile.basic, a standalone variant with no krmllib dependency. Since it is used without a Makefile.include, it discovers the generated C files with a wildcard over the output directory. - Under --pulse, invoke KaRaMeL with -skip-makefiles unconditionally, so neither Makefile.basic nor Makefile.include is emitted (making --skip_c_makefiles a no-op as far as KaRaMeL is concerned), and drive the C build through EverParse's copy instead, both from 3d.exe itself (build_test_exe) and from the --pulse test Makefiles. - Install it in the binary package alongside the rest of the Pulse runtime. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…lean Neither tree was reachable from the top-level clean. clean-3d cleans the Low* prelude under src/3d/prelude, and clean-3d-tests the Low* corpus under src/3d/tests, so the Pulse prelude's .checked and .krml files and the whole Pulse test corpus survived a full clean. Three latent bugs surfaced while wiring this up. krml/extract.Makefile added clean-extracted to clean_rules but never defined it, so `make -f extract.Makefile clean` died with "No rule to make target clean-extracted". It had presumably never been run; krml/Makefile carried its own `rm -rf extracted` instead, which is why nobody noticed. Define the rule and have krml/Makefile delegate rather than duplicate it. It has to remove the directory, not just its .krml files as common.Makefile's clean-krml does, because the F* dep file lives inside it. share/everparse/tests/3d/iter/Makefile had no clean at all -- it only recurses into coarse/ and fine/ for the default target -- so both obj/ directories survived. Its Low* original has the same gap. And the loop that cleans the subdirectories ran without set -e, so that failure was swallowed and the loop carried on. Add the guard, so the next missing clean is loud rather than silent. Verified by cleaning both trees to a state where git status --ignored is empty, checking the targets are idempotent, and rebuilding the prelude from scratch afterwards: 20 .checked and 148 .krml, as before. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
commented
Aug 28, 2026
Under --pulse, KaRaMeL was emitting an EverParse.c holding the handful of runtime helpers that survive specialization, which the generated Makefile then had to compile and link. The Low* backend has no such file: it ships a self-contained EverParse.h whose helpers are all static inline. Extend -static-header to cover the two runtime modules that actually contribute those bodies, mirroring the Low* list minus EverParse3d.CopyBuffer and EverParse3d.InputStream.*. Those two hold the assume vals the client implements in C; Low* can list them because it also passes -library, which drops their declarations outright, whereas here KaRaMeL would emit them as static prototypes that never get a definition and clash with the client's non-static one. That alone left one resident behind. EverParse3d.Actions.Base re-exports is_range_okay as a bare alias so the frontend can emit the unqualified name; F* extracts an alias as a global holding a function reference, and KaRaMeL emits it as a function pointer variable. So every is_range_okay call in generated code was an indirect call through a global, where Low* has a direct call to a static inline. Marking the alias inline_for_extraction removes the global and the indirection. With no EverParse.c left, drop the rules that produced and compiled it and the link lines that referenced it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
Under --pulse the KaRaMeL bundle listed a single API module, EverParse3d.Actions.Common. Everything else in the bundle was therefore private, and any of it that survived as a cross-translation-unit symbol was raised to internal/EverParse.h -- a header client code is not meant to include. That covered the ErrorCode helpers, the StaticHeader bitfield accessors, the copy-buffer projections and, in extern/static mode, the input-stream hooks, all of which the Low* prelude declares in EverParse.h. It also left EverParseErrorReasonOfResult non-public, unlike in Low*. Widen the API list so those modules are public. Two constraints shape it: - Bundle APIs are per-module, so a module can only be listed if all of its extracted declarations belong in the public ABI. EverParse3d.InputStream. Buffer does not qualify: its stream helpers are inline_for_extraction but not noextract, and going public forces KaRaMeL to materialise each of them as a real function, resurrecting EverParse.c. Move the four assumed copy-buffer declarations to a new leaf module, EverParse3d.CopyBuffer. Buffer, which the API list can name on its own; InputStream.Buffer re-exports them so existing uses are unchanged. For the same reason, mark field_ptr_after_with_setter_impl noextract in InputStream.Extern. - Each of the Buffer, Extern and Static backends owns a [@@cmacro] error_handler_macro, and they only coexist because the unselected ones are private. Making two public at once collides on EVERPARSE_ERROR_HANDLER_MACRO (KaRaMeL warning 23), so only the selected backend is listed. call_krml now takes the input stream binding to decide. Static has no extracted declarations of its own and needs nothing public. EverParsePulseEndianness.h re-declared the three copy-buffer projections as a workaround for their living in internal/. That workaround is now not just redundant but wrong: the duplicate sits outside the extern "C" guard, so C++ clients see conflicting linkage against the generated EverParse.h. Drop it. internal/ still holds one header, for the monomorphized (base, len, pos) triple that stream_truncate returns; KaRaMeL places monomorphized instances in the generated module that uses them first, which no bundle can reach. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
…lued input_stream_inst.truncate returned a (base_t & len_t & pos_t) triple. That extracts to a C struct, and KaRaMeL assigns a monomorphized instance to whichever *generated* module uses it first -- a client module no bundle can reach -- so once a second generated module used it too it had to be shared through internal/. That was the one remaining difference between the file set --pulse emits and the Low* one. Neither backend actually needs all three components: truncating a byte array leaves the base pointer and the position cell alone and only shortens the length, while an extern stream keeps its length and position on the far side of the C boundary and returns a fresh base handle. So give the class an associated type trunc_t naming the single component the backend modifies, plus trunc_base/trunc_len/trunc_pos to recover the other two from the original stream. Buffer sets trunc_t = len_t, extern sets trunc_t = base_t. Both backends now extract to a scalar-returning function, no struct is ever built, and internal/ disappears. The extern ABI is unchanged -- EverParseStreamTruncate still returns EVERPARSE_INPUT_STREAM_BASE -- and the buffer call sites get strictly simpler C: three plain locals in place of a struct literal that was immediately projected three ways. The projections are ordinary Tot functions, so the three callers in Actions.Base keep passing a single value around and no proof structure changes; they just bind tb/tl/tp and rewrite. The rewrites have to name the record projector (inst.trunc_base) rather than the typeclass method, since Pulse frame inference matches syntactically and does not delta-reduce. An alternative was to pass three ref out-parameters. That works too -- krml erases ref unit arguments and collapses the let-mut locals when the writer is inlined. It was rejected for the extern backend: there the writer is an assumed val and is not inlined, so the refs become real stack slots whose addresses are passed, turning a scalar return into an out-parameter and breaking the C ABI. It also adds boilerplate at each of the three call sites (three refs, three reads, three more existentials to open) rather than removing any. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
The stream_trunc_base/len/pos projections are inline_for_extraction noextract lets, so they are delta-reducible; when type-checking an instance's stream_truncate against the class field type, F* substitutes the earlier fields of the same record literal. That makes the directly- stated spec convertible with the projection-stated one. So each backend can now say what it actually means: buffer: stream_pts_to b res pos ... (only the length shortens) extern: stream_pts_to res () () ... (only the base changes) instead of routing every component through stream_trunc_*. No change to the generated C: extraction, the absence of internal/ and EverParse.c, and the full share/everparse/tests/3d suite are all unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
`3d.exe --pulse` rebuilt the whole Pulse runtime header on every invocation,
bundling it into the client's output directory with -static-header. That is
wasteful: the result does not depend on the .3d input at all. Verified by
generating it for five very different inputs (TestAllBytes, Pair, ELF,
Arithmetic, FineGrainedProbe) -- byte-identical every time, 159 lines. It
depends only on the input stream backend, and extern and static agree.
So do what the Low* backend does. lib/everparse/3d/krml/header.Makefile now
generates one EverParse.h per backend at build time, from the prelude .krml
files alone, into lib/everparse/3d/krml/<backend>/ -- the exact analogue of
src/3d/prelude/<backend>/EverParse.h. Batch.ml passes KaRaMeL -library
instead of -static-header, which turns the runtime into plain `extern`
declarations resolved by that header, and copies the shipped header into the
output directory.
This works because everything the runtime contributes to the generated
validators is inline_for_extraction and has already been inlined by F*
itself; -library only has to cover the residue, which is what the shipped
header defines. Confirmed: the generated .c/.h are byte-identical either
way for all five inputs above.
Two visible consequences, both convergences with Low*:
- EverParse.h no longer #includes itself (an artifact of the global
-add-include '"EverParse.h"', harmless but silly).
- --no_copy_everparse_h now leaves no EverParse.h behind, so the
pulse-cleanup-test expectation is now literally the Low* one.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
The new lib/everparse/3d/krml/header.Makefile derived DDD_HOME from
$(realpath ../../../../src), which under Cygwin make yields a
/cygdrive/d/... path. KRML_EXE on Windows is a native krml.exe, which
cannot open such a path, so all three backend header rules died with
Fatal error: exception Sys_error("/cygdrive/d/a/everparse/everparse/src/3d/noheader.txt: No such file or directory")
failing 3d-pulse-krml and hence the whole nuget-noversion package build.
Include src/windows.Makefile, which rewrites EVERPARSE_SRC_PATH with
cygpath -m on Windows, and derive DDD_HOME after it. This is exactly what
the sibling extract.Makefile already does. No-op on Linux: the three
generated headers are byte-identical.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 9280194c-7c30-4916-8e1c-9b786e884b25
This reverts commit 5828117.
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.
This branch adds a second, complete code-generation backend to 3D, built on
Pulse instead of Low*, selected by a new
--pulseflag. The Low* backend isuntouched and remains the default: every change is either additive or guarded
by
Options.get_pulse ().The port is functionally complete. The new runtime has no admits, the
generated C compiles under
-Wall -Wextra -Werror, and a full parallel copy ofthe 3D test corpus builds, links and runs against it.
What is here
1.
lib/everparse/3d— the Pulse combinator libraryA Pulse counterpart to
src/3d/prelude:Prelude,Kinds,ErrorCode,InputStream.{Base,Buffer,Extern,Static},CopyBuffer,AppCtxt,Actions.{Base,Common},ProbeActions,State, andInterpreter.Three structural departures from Low*:
Memory locations and invariants become
extra_state. Low* threadsloc/inv/livenessthrough every validator and action. Pulse replaces allof it with a state dictionary (
EverParse3d.State): a keyed product ofresources, where disjointness is a syntactic property of distinct string keys
rather than an SMT obligation.
Pulse.Lib.ForEverycarries the pointwiseownership, and the
callcombinators rename keys at call boundaries. Almostall of the reasoning discharges by normalization instead of Z3.
One input buffer becomes three arguments.
input_stream_inst base_t len_t pos_t, withpts_to : base_t -> len_t -> pos_t -> Seq.seq U8.t -> Seq.seq U8.t -> slprop. Thebufferinstance usesPulse.Lib.ArrayPtr.ptr U8.t,SZ.tandref SZ.t;externandstaticinstantiate the unused ones tounit, and KaRaMeL erases those arguments.Backend-conditional actions without a backend flag. Rather than a flag,
the interpreter takes
option field_ptr_t,option field_ptr_after_tetc.,and
Action_field_ptrcarries asquash (Some? ...). The frontend suppliesthe instance, so
field_ptrstays buffer-only andfield_ptr_afterextern/static-only, exactly as in Low*, with no linking or
--includetricks.The library is extracted to
.krml(lib/everparse/3d/krml) and bundled intothe generated C, rather than shipped as a separate C library the way the Low*
prelude is.
2.
src/3d— the frontend--pulseswitches F* emission, the--includepath, the KaRaMeL invocationand the C wrapper. Notable points:
_Static_asserts thatsize_tis at least as wide asuint32_tanduint64_t.buffer,externandstaticeach own a[@@CMacro] assume val error_handler_macro, and the frontend instantiatesvalidate_with_error_handleraccordingly.extern/static, and reject nestedprobes that would reuse one copy buffer.
--pulse, in both harness modes,including probes. The SMT half is backend-independent — it runs on the
InterpreterTargetAST — and produces byte-identical witnesses and verdictson both backends; only the emitted C harness differs.
--pulse(
norm [delta_namespace ["EverParse3d"; "LowParse"]; ...]). Without this,and_then_kind/glbnests unfold exponentially during extraction:FieldDependence0.3dwent from OOM at 166 GB to 57 ms.3.
share/everparse/tests/3d— the test corpusA full copy of
src/3d/testsadapted to--pulse;src/3d/testsisunchanged. 37 top-level
.3dfiles (10 negative) plus 18 subdirectories, allof which generate, verify, extract, compile and run.
4. Packaging and CI
package.shshipslib/everparse/3d(sources,.checkedand pre-extracted.krml) pluslib/pulse. Every binary-package test job inpackage-{linux,macos,windows}.yml,nightly.ymlandrelease.ymlgained a--pulsestep, as did the cross-platform hash-interop jobs and the Z3test-generation steps.
Notable fixes along the way
Several of these are pre-existing bugs the port exposed rather than caused:
Z3TestGenargument swap —Main.fstpassed(print_c_initializers, use_ptr)todo_test/do_diff_test, which declare(use_ptr, print_c_initializer);do_diff_testhad a second, compensatingswap. Both are
bool, so it typechecked silently, and every existing testset the two flags to the same value.
a1b6f3df6.from wherever the first probe left it. Fixed with a
resetmethod on thecopy_bufferclass. No test outsidespecialize_*would have caught it.make cleangaps —krml/extract.Makefilelistedclean-extractedinclean_ruleswithout defining it;tests/3d/iter/Makefilehad nocleanatall (its Low* original has the same gap); and the subdirectory clean loop ran
without
set -e, swallowing both.68909c201..orules listed the generatedwrapper header but not
EverParse.h. Harmless under Low*, where it iscopied at the start of the pipeline, but under
--pulseKaRaMeL emits it atthe end, so parallel builds raced.
4f409e1cc.Remaining work to reach near-parity with Low*
Nothing below blocks the branch; none of it is a correctness regression
against the Low* backend.
Correctness coverage
validate_t_exacton a non-buffer stream is untested. Underextern,stream_truncatereturns(base_t & unit & unit), and how KaRaMeL rendersthat struct is unverified — no subdirectory exercises it. This is the only
genuine unknown left, as opposed to polish.
--pulseoutput.Low*'s three
hashchk-*targets have no Pulse counterpart.Feature gaps
act_with_commentcarries aTODO at three sites in
Actions.Base.fst;T_with_commentand thevalidate_filterstrings are dropped, so--pulseC is cosmetically poorerthan Low*'s. Needs Pulse-side support.
3d-doc-testhas no--pulsesnapshot.doc/3d-snapshot/isregenerated and diffed for Low* only. Best done after (3), to avoid
re-baselining.
--pulseclient ABI is undocumented.doc/3d-lang.rstgives onlythe Low* copy-buffer hooks; under
--pulsea client must also defineEverParseStreamPos(returningsize_t *), andEverParseStreamLenreturns
size_t. The flag itself and the(base, len, pos)validator/error-handler ABI are undocumented.
Verification debt
Tot→GTotTODOs on the erased bijection argument(
State.fst:785,Actions.Base.fst:{741,1285},.fsti:{343,485}).Erasure hygiene only; needs ghost bijections to exist first.
Actions.Base.fst:284— anif/elsethat would read better as anon-terminal early exit with an
ensures.Accepted differences (by design, not oversight)
staticandexternare byte-identical at the C level. KaRaMeL emitsplain
externfor every assumed val, so Low*'sstatic inlineprelude trickis unreproducible. They remain separate F* modules only because each owns its
error_handler_macro. Consequentlyfield_ptr_afteris allowed for both,where Low* restricts it to
extern.--input_stream extern|static, as agreed.reports each field's start position. Verdicts and witnesses agree; only the
position column in the trace comments differs.
the validator as an argument; in Pulse it lives in the stream, hence the extra
EverParseStreamPoshook and theresetmethod.Trust footprint
lib/everparse/3dhas no admits. The deliberateassume vals mirrorLow*'s one-for-one: the input-stream primitives per backend, the probe
functions, the
[@@CMacro] error_handler_macros, and the copy-buffer handlewith its three projections. That last one is exactly Low*'s bargain —
stream_ofis assumed and is not really a function of its argument; Low* paysfor it in liveness, Pulse in ownership, and in both the fresh region is
admitted by fiat inside the already-assumed probe functions.
Testing
make 3d-pulse-prelude— verifies the library (20 modules).make 3d-pulse-krml— extracts it (148.krml).make 3d-pulse-test— the full corpus: generation, F* verification, KaRaMeLextraction, C compilation under
-Wall -Wextra -Werror, and execution.Wired into
make test, and parallel-safe (-j16, ~11 min from clean).src/3d/tests, includingz3-testgen-probe-test) werere-run and are unaffected.