[SHA3 / ML-KEM/ ML-DSA] C extraction #117
Conversation
|
At this point the extraction and build succeed, but the test fails. |
|
The failing test was due to an apparently incorrect translation of a |
jschneider-bensch
changed the title
keks
left a comment
keks
left a comment
There was a problem hiding this comment.
The changes to the Rust code look good to me. There is a bunch of commented old code in the shell script, let's remove that. I like the new logic for handling dependencies, it's a lot cleaner. I expect it works just as well for distinguishing kebab-case and snake-case?
Otherwise I was not able to extract the ML-DSA code, but it looks like it worked for you. Maybe let's talk to see what I am doing wrong.
keks
left a comment
keks
left a comment
There was a problem hiding this comment.
I think this mostly looks pretty good! I just had the pleasure of doing a proper deep update of the glue in another project, so I had that on my mind when I reviewed this, and it looks like this is pretty out of date.
Here is the glue for our Eurydice version, but maybe it has too much stuff in it: https://github.com/AeneasVerif/eurydice/blob/cdf02f/include/eurydice_glue.h
I mostly commented on the one that was added to ML-DSA, but I suppose we might also have in ML-KEM and SHA3.
Otherwise I think this looks good!
| typedef struct Eurydice_dst_ref_87_s { | ||
| uint8_t *ptr; | ||
| size_t meta; | ||
| } Eurydice_dst_ref_87; | ||
|
|
||
| typedef struct Eurydice_dst_ref_9a_s { | ||
| int16_t *ptr; | ||
| size_t meta; | ||
| } Eurydice_dst_ref_9a; | ||
|
|
|
|
||
| // This macro is a pain because in case the dereferenced element type is an | ||
| // array, you cannot simply write `t x` as it would yield `int[4] x` instead, | ||
| // which is NOT correct C syntax, so we add a dedicated phase in Eurydice that | ||
| // adds an extra argument to this macro at the last minute so that we have the | ||
| // correct type of *pointers* to elements. | ||
| #define Eurydice_slice_index(s, i, t, t_ptr_t) (((t_ptr_t)s.ptr)[i]) | ||
| #define Eurydice_slice_index(s, i, t) ((s).ptr[i]) | ||
|
|
There was a problem hiding this comment.
This was dropped in the glue:
| // We represent a slice as a pair of an (untyped) pointer, along with the length | ||
| // of the slice, i.e. the number of elements in the slice (this is NOT the | ||
| // number of bytes). This design choice has two important consequences. | ||
| // - if you need to use `ptr`, you MUST cast it to a proper type *before* | ||
| // performing pointer arithmetic on it (remember that C desugars pointer | ||
| // arithmetic based on the type of the address) | ||
| // - if you need to use `len` for a C style function (e.g. memcpy, memcmp), you | ||
| // need to multiply it by sizeof t, where t is the type of the elements. | ||
| // | ||
| // Empty slices have `len == 0` and `ptr` always needs to be a valid pointer | ||
| // that is not NULL (otherwise the construction in EURYDICE_SLICE computes `NULL | ||
| // + start`). | ||
| typedef struct { | ||
| void *ptr; | ||
| size_t len; | ||
| } Eurydice_slice; | ||
|
|
||
| typedef struct Eurydice_dst_ref_87_s { | ||
| uint8_t *ptr; | ||
| size_t meta; | ||
| } Eurydice_dst_ref_87; | ||
|
|
||
| typedef struct Eurydice_dst_ref_9a_s { | ||
| int16_t *ptr; | ||
| size_t meta; | ||
| } Eurydice_dst_ref_9a; |
| // Helper macro to create a slice out of a pointer x, a start index in x | ||
| // (included), and an end index in x (excluded). The argument x must be suitably | ||
| // cast to something that can decay (see remark above about how pointer | ||
| // arithmetic works in C), meaning either pointer or array type. | ||
| #define EURYDICE_SLICE(x, start, end) \ | ||
| (KRML_CLITERAL(Eurydice_slice){(void *)(x + start), end - start}) |
| #define Eurydice_slice_eq_shared(s1, s2, t, _) \ | ||
| ((s1)->meta == (s2)->meta && \ | ||
| memcmp((s1)->ptr, (s2)->ptr, (s1)->meta * sizeof(t)) == 0) |
| ((X)->tag == 1) | ||
| // STRINGS | ||
|
|
||
| typedef const char *Prims_string; |
There was a problem hiding this comment.
This looks different upstream
| // MISC (UNTESTED) | ||
|
|
||
| typedef void *core_fmt_Formatter; | ||
| typedef void *core_fmt_Arguments; | ||
| typedef void *core_fmt_rt_Argument; | ||
| #define core_fmt_rt__core__fmt__rt__Argument__a__1__new_display(x1, x2, x3, \ | ||
| x4) \ | ||
| NULL |
| // Crimes. | ||
| static inline char *malloc_and_init(size_t sz, char *init) { | ||
| char *ptr = (char *)malloc(sz); | ||
| memcpy(ptr, init, sz); | ||
| return ptr; | ||
| } |
There was a problem hiding this comment.
Upsteam it doesn't say "Crimes" and also checks whether the pointer returned by malloc is NULL 😅
| // VECTORS (ANCIENT, POSSIBLY UNTESTED) | ||
|
|
||
| /* For now these are passed by value -- three words. We could conceivably change | ||
| * the representation to heap-allocate this struct and only pass around the | ||
| * pointer (one word). */ | ||
| typedef struct { | ||
| void *ptr; | ||
| size_t len; /* the number of elements */ | ||
| size_t alloc_size; /* the size of the allocation, in number of BYTES */ | ||
| } Eurydice_vec_s, *Eurydice_vec; | ||
|
|
||
| /* Here, we set everything to zero rather than use a non-standard GCC | ||
| * statement-expression -- this suitably initializes ptr to NULL and len and | ||
| * size to 0. */ | ||
| #define EURYDICE_VEC_NEW(_) calloc(1, sizeof(Eurydice_vec_s)) | ||
| #define EURYDICE_VEC_PUSH(v, x, t) \ | ||
| do { \ | ||
| /* Grow the vector if capacity has been reached. */ \ | ||
| if (v->len == v->alloc_size / sizeof(t)) { \ | ||
| /* Assuming that this does not exceed SIZE_MAX, because code proven \ | ||
| * correct by Aeneas. Would this even happen in practice? */ \ | ||
| size_t new_size; \ | ||
| if (v->alloc_size == 0) \ | ||
| new_size = 8 * sizeof(t); \ | ||
| else if (v->alloc_size <= SIZE_MAX / 2) \ | ||
| /* TODO: discuss growth policy */ \ | ||
| new_size = 2 * v->alloc_size; \ | ||
| else \ | ||
| new_size = (SIZE_MAX / sizeof(t)) * sizeof(t); \ | ||
| v->ptr = realloc(v->ptr, new_size); \ | ||
| v->alloc_size = new_size; \ | ||
| } \ | ||
| ((t *)v->ptr)[v->len] = x; \ | ||
| v->len++; \ | ||
| } while (0) | ||
|
|
||
| #define EURYDICE_VEC_DROP(v, t) \ | ||
| do { \ | ||
| free(v->ptr); \ | ||
| free(v); \ | ||
| } while (0) | ||
|
|
||
| #define EURYDICE_VEC_INDEX(v, i, t) &((t *)v->ptr)[i] | ||
| #define EURYDICE_VEC_LEN(v, t) (v)->len |
There was a problem hiding this comment.
The upstream glue has new array stuff -- are we even using arrays? Maybe this can just be removed.
| /* TODO: remove GCC-isms */ | ||
|
|
||
| #define EURYDICE_REPLACE(ptr, new_v, t) \ | ||
| ({ \ | ||
| t old_v = *ptr; \ | ||
| *ptr = new_v; \ | ||
| old_v; \ | ||
| }) |
2 participants
This PR provides a C extraction for ML-DSA and updates the C extractions for SHA3 and ML-KEM to work with Eurydice revision
cdf02f9d8ed0d73f88c0a495c5b79359a51398fc.CI will fail at the moment, because the latest publishedlibcrux-cdocker image runs an older version of Eurydice. Should work once cryspen/libcrux#1237 is merged.