Fix issue 676

[protz]

I recommend viewing the diff with whitespace off: link

the changes are relatively minimal and consist in skipping a recursive traversal if we have no good reason to do it

this also allowed me to remove a call to self#visit_node that I always thought was un-necessary but for some reason remained... good riddance

@tahina-pro are there any additional regressions you would like to run for this?

on my end, this breaks eurydice: AeneasVerif/eurydice#378 so I need to investigate what's going on there

[protz]

Things look good on the Eurydice end -- @tahina-pro please confirm this works for you in case you have other regression suites you'd like to run. Thank you!

[tahina-pro]

Thanks a lot Jonathan!

While this PR solves the C extraction and compilation issue, it now seems to introduce a Karamel-to-Rust extraction issue where Karamel does not properly remove a record field of Ghost.erased type and complains with "some fields are superfluous (expr)". I mention it here if it is any similar to the regression you found in Eurydice, but in any case, I will try to minimize it and push a unit test here. Stay tuned!

Details

Meanwhile, for completeness: on https://github.com/tahina-pro/quackyducky/commits/_taramana_krml_679/ , the following command:

make clean && ADMIT=1 make -j$(nproc) cbor-extract-pre && ADMIT=1 ./shell.sh -c 'make -j$(nproc) -C src/cbor/pulse/krml det-rust'

to rebuild Karamel and extract Rust parsers and serializers for Deterministically Encoded CBOR, works on tahina-pro/quackyducky@c586551, which pulls the latest Karamel master as of now, but fails with tahina-pro/quackyducky@ba646ec, which pulls this Karamel PR as of now, with the following error message:

Cannot re-check CBOR.Pulse.Raw.Match.cbor_string_reset_perm as valid Low* and will not extract it.  If CBOR.Pulse.Raw.Match.cbor_string_reset_perm is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in top-level declaration CBOR.Pulse.Raw.Match.cbor_string_reset_perm, in file CBORDetVerAux: Malformed input:
some fields are superfluous (expr) in { cbor_string_type = match @0 with | λ cbor_string_type(Mark.Present,1, ): uint8_t, cbor_string_size(Mark.MaybeAbsent,0, ): uint8_t, cbor_string_ptr(Mark.MaybeAbsent,0, ): Pulse_Lib_Slice_slice uint8_t, cbor_string_perm(Mark.MaybeAbsent,0, ): ().  { cbor_string_type = @3; cbor_string_size = @2; cbor_string_ptr = @1; cbor_string_perm = @0; } ->  cbor_string_type@3; cbor_string_size = match @0 with | λ cbor_string_type(Mark.MaybeAbsent,0, ): uint8_t, cbor_string_size(Mark.Present,1, ): uint8_t, cbor_string_ptr(Mark.MaybeAbsent,0, ): Pulse_Lib_Slice_slice uint8_t, cbor_string_perm(Mark.MaybeAbsent,0, ): ().  { cbor_string_type = @3; cbor_string_size = @2; cbor_string_ptr = @1; cbor_string_perm = @0; } ->  cbor_string_size@2; cbor_string_ptr = match @0 with | λ cbor_string_type(Mark.MaybeAbsent,0, ): uint8_t, cbor_string_size(Mark.MaybeAbsent,0, ): uint8_t, cbor_string_ptr(Mark.Present,1, ): Pulse_Lib_Slice_slice uint8_t, cbor_string_perm(Mark.MaybeAbsent,0, ): ().  { cbor_string_type = @3; cbor_string_size = @2; cbor_string_ptr = @1; cbor_string_perm = @0; } ->  cbor_string_ptr@1; cbor_string_perm = (); }: ()
Warning 4 is fatal, exiting.
make: *** [Makefile:34: /home/tahina/everparse/src/cbor/pulse/det/rust-extracted/cbordetver.rs] Error 255

[protz]

Ok interesting. I'll hold off on merging this until you can provide me with a repro, and then I'll make sure this PR contains both the new testcase and a fix for it.

Is there some CI place I should be looking at to avoid these unpleasant regressions? Would you like to add some additional regressions in the karamel CI? If so, I'm open to it

[tahina-pro]

I'll hold off on merging this until you can provide me with a repro

I just pushed it here as promised. I instructed GitHub Copilot CLI 0.410.0 with Claude Opus 4.6 to minimize the CBOR Rust extraction failure that I mentioned in the details above, and it produced 4a20397, with an example, test/rust-propererasure-bundle, with a record type with an erased field, and a private function using that record, and a public function calling that private function. That example worked on top of master without this PR: https://github.com/FStarLang/karamel/actions/runs/22011396114 . It fails with this PR.

In doing so, the LLM claims the following as the root cause:

remove_unit_fields assumes DType declarations come before their uses in the declaration list, but bundling + monomorphization can violate this assumption.

[tahina-pro]

Is there some CI place I should be looking at to avoid these unpleasant regressions? Would you like to add some additional regressions in the karamel CI? If so, I'm open to it

Thanks a lot Jonathan for suggesting!

In fact, EverParse has a nightly CI workflow where it tries to upgrade F* and Pulse (and Karamel, once this PR is merged) : https://github.com/project-everest/everparse/actions/workflows/nightly.yml . There, Karamel-specific output can be seen in Actions > Upgrade hashes, 3d doc, CBOR, COSE (nightly.yml) > Advance hashes > Generate CBOR snapshot with Karamel, and Actions > ... > Generate COSE snapshot with Karamel. However, since this nightly workflow rebuilds and re-tests all of EverParse, it is very slow. Thus, it only runs twice a week, on Sundays and Wednesdays at 2pm Seattle time.

Alternatively, if you want to test rebuilding of CBOR and COSE at each Karamel PR, I just opened #680 to add such rebuilds to the Karamel CI, with what I believe is enough leverage of GitHub Actions' caching mechanism to reduce the rebuilds of F* and EverParse unrelated to Karamel to a few seconds instead of a few dozen minutes.

[protz]

I think your comment is correct and the assumption that the definition comes before the use was never true.

EverParse has a nightly CI workflow where it tries to upgrade F* and Pulse

How can I get emails for such build breakages?

if you want to test rebuilding of CBOR and COSE at each Karamel PR

This sounds even better. I'll take a look at that second PR once we get a green on this one. Thanks so much!