search

jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography
MIT License
271 stars 55 forks source link

reference tests for easycrypt extraction #863

Closed cassiersg closed 2 months ago

cassiersg commented 4 months ago

Tests that the easycrypt extraction matches vested "golden" files, up to insignificant whitespace changes.

cassiersg commented 4 months ago

@vbgl Do you know why the CI fails?

I see that https://gitlab.com/jasmin-lang/jasmin/-/jobs/7317501176 fails because of No such file or directory: './scripts/extract-and-check'.

Running nix-shell --run 'make -C compiler CHECKCATS="x86-64-extraction arm-m4-extraction" check' locally works.

vbgl commented 4 months ago

Is it really needed to store so many expected test results? Shouldn’t a checksum be enough to detect regressions?

cassiersg commented 4 months ago

That could be done indeed, but w'd loose:

  1. the current fine-grained approach where we can ignore non-significant white-space changes
  2. ease of reviewing what changes: currently, if the test fails, it displays a diff expected vs new. (Both when promoting the new reference files as a reviewer, and when reviewing the changes as a PR reviewer.)

It is debatable whether 1. is a good idea to have. For 2., I think that it's a significant annoyance.

The long-term plan of @eponier is to move this to dune "cramtest" (and extend it to also check assembly output).

We could also try to reduce the number of files by putting all the test results in a single file (tar-like, but in a human-readable format). Would that help to adress your concerns ? Is the issue more w.r.t. to the number of files, or with the amount of data in the repository ?

vbgl commented 4 months ago

I’m mostly concerned by the amount of data that is added there.

cassiersg commented 4 months ago

(To quantify: it's about 6.8 MB of data.)

I have no strong opinion (and I am not a maintainer), so I'm totally open to moving to hashes. We can always change the approach later if point 2. above ends up being too annoying. Should I move forward with a solution with hashes?