CI: add EverParse CBOR, COSE regression tests

[tahina-pro]

Trying to answer Jonathan's question from #679 (comment) :

Would you like to add some additional regressions in the karamel CI? If so, I'm open to it

This PR augments Karamel's CI with an extraction test for EverCBOR and EverCOSE, the verified CBOR and COSE implementations from EverParse.

To this end, this PR adds a GitHub Actions job, test-everparse, into the existing CI workflow, to extract EverCBOR and EverCOSE. This job clearly isolates the calls to Karamel away from unrelated logs (e.g. F* verification and extraction to .krml)

test-everparse needs to build EverCBOR and EverCOSE, which by default takes ~ 18 minutes (see https://github.com/tahina-pro/karamel/actions/runs/22079451423/job/63801660122), but this PR introduces enough cache to reduce this task to a few seconds only (see https://github.com/tahina-pro/karamel/actions/runs/22083264582/job/63812690728)

Since test-everparse uses the same dependencies as build-and-test-krml, this PR also refactors the dependency build by adding a new prior job, build-deps, leveraging cache to be shared across the two jobs.

The 2 logs linked above succeed on EverParse because this PR has been initially built on top of the Karamel version used by EverParse as of 2/16/2026, fb36fec. They fail with Karamel master: in fact, this PR can be merged only after #679 is fixed and #681 is merged.

[tahina-pro]

The --branch line (along with the comment above) to be removed once project-everest/everparse#244 is merged

[protz]

From a quick review:

• as long as you can help maintain this, I'm fine with adding it to the CI
• why bother testing two Z3 versions? if krml is mostly about extraction, then I think the everparse CI should admit the everparse SMT queries, no?

[tahina-pro]

Thanks Jonathan! As of today I can see that there is further fallout on EverParse after merging #679 , so I will open issues with minimal test cases from such fallout. (These may be related to unknown issues other than #676.)

Alternatively, I could try to open a pull request with all necessary fixes to Karamel that make EverParse work, adding unit test cases to Karamel for each issue I encounter in this process. What do you think about that?

• as long as you can help maintain this, I'm fine with adding it to the CI

Yes, it is easy for me to maintain it.

• why bother testing two Z3 versions? if krml is mostly about extraction, then I think the everparse CI should admit the everparse SMT queries, no?

You are right, I don't need any Z3 for test-everparse. I just removed that task.

[protz]

Alternatively, I could try to open a pull request with all necessary fixes to Karamel that make EverParse work, adding unit test cases to Karamel for each issue I encounter in this process. What do you think about that?

If you know the fixes you need, then I'd be happy to take the PR!

Sorry about the fallout -- I did not realize this was so impactful (I tried it on my own regressions, which obviously aren't covering enough).

Yes, it is easy for me to maintain it.

Great thank you. Can you run with OCAMLRUNPARAM=b? I'd love to see backtraces, right now I'm quite curious where the error comes from.

[tahina-pro]

If you know the fixes you need, then I'd be happy to take the PR!

I just opened #681 . Thanks in advance!

Sorry about the fallout -- I did not realize this was so impactful (I tried it on my own regressions, which obviously aren't covering enough).

No worries! Conversely, it would be very helpful if a subset of regression test suites from Eurydice were added to Karamel's CI, so that the fixes needed for EverParse wouldn't inadvertently break Eurydice. It's up to you!