Import NI modules of GHASH from pnmadelaine_aes branch and adds specific proofs
#942
Conversation
|
[CI] Important!
|
|
Can you say more about why you want to clone from Vale? If the specs are there and are ok, can we make sure there's no copy-paste? |
|
I had concerns that we need to remove the dependencies to Vale modules but it turned out it's ok so there's no need to do any abstraction. |
|
@msprotz Missing equivalent lemmas are added in |
|
@msprotz What's the state of this one? |
There was a problem hiding this comment.
This is a great step in the right direction. For now, we need to improve the API, understand what needs to be public and/or private, and write proper documentation about how to use this module.
Seeing how to improve the proofs would also be a plus, as this is going to add quite a bit to the maintenance effort going forward.
|
|
||
| #include "libintvector.h" | ||
|
|
||
| void Hacl_Gf128_NI_gcm_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key); |
There was a problem hiding this comment.
@pnmadelaine can you please suggest names for all of these functions?
|
|
||
| #include "libintvector.h" | ||
|
|
||
| void Hacl_Gf128_NI_gcm_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key); |
There was a problem hiding this comment.
@mamonet we need a comment here that answers the following questions:
- how does one obtain a ctx? which function should one use to allocate it?
- is the key expanded? or not? what is the length of the key? (this also applies to your other PR -- you should specify the length of the pointers your receive -- again, please look at the bignum modules for how to write good effective documentation)
There was a problem hiding this comment.
I added a layout for GHASH context, I hope it makes it clear to understand the procedure underneath.
| uint8_t *text | ||
| ); | ||
|
|
||
| extern void |
There was a problem hiding this comment.
why is this a function pointer?
| void Hacl_Gf128_NI_gcm_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key); | ||
|
|
||
| void | ||
| Hacl_Gf128_NI_gcm_update_blocks( |
There was a problem hiding this comment.
what is the expected usage of this API? the documentation should tell me which functions to call, in which order, and how to obtain the final result
There was a problem hiding this comment.
You are right, not point of having a duplicate function in API. Input message is supposed to be padded anyways.
| uint8_t *x2 | ||
| ); | ||
|
|
||
| void Hacl_Gf128_NI_gcm_emit(uint8_t *tag, Lib_IntVector_Intrinsics_vec128 *ctx); |
There was a problem hiding this comment.
again I think @pnmadelaine called it digest or something -- it should have the same name as poly1305
There was a problem hiding this comment.
This function just copies hash state to output buffer, it doesn't involve any computations. is digest more convenient in this case?
| let load_elem (b:lbytes 16) : elem = load_felem_be #gf128 b | ||
| let store_elem (e:elem) : lbytes 16 = store_felem_be #gf128 e | ||
|
|
||
| let irred_le = mk_int #U128 #SEC 0x87 |
There was a problem hiding this comment.
what does lemean? lesser or equal? comments please
There was a problem hiding this comment.
le here stands for little-endian mode. I will adds a comment that clears things up.
| let gmul (text:bytes) (h:lbytes size_block) : Tot tag = | ||
| let acc, r = gf128_init h in | ||
| let acc = gf128_update text acc r in | ||
| decode acc |
There was a problem hiding this comment.
is this shown anywhere to be equivalent to the vale version?
|
|
||
|
|
||
| let gf128_update_multi_mul_add_lemma_load_acc_aux a0 b0 b1 b2 b3 r = | ||
| admit(); |
There was a problem hiding this comment.
please give us an update on how many admit()s are left and to what extent they are fixable
There was a problem hiding this comment.
This and others (if any) got to be uploaded without being seen. I will address this one and lookup for other potential admits
|
|
||
| #push-options "--z3rlimit 20 --max_fuel 0" | ||
| let logxor_disjoint #n a b m = | ||
| assert (forall (i:nat{n - m <= i /\ i < n}).{:pattern (index #bool #n (to_vec a) i)} |
There was a problem hiding this comment.
are you familiar with calc statements? they might make this sort of proof a lot more readable
There was a problem hiding this comment.
This function is ported from logor_disjoint in FStar.UInt.fst https://github.com/FStarLang/FStar/blob/master/ulib/FStar.UInt.fst#L302
The body of the function was hand-copied from there, I still can improve the syntax for better readability.
| (shift a1 64) +. a0 +. (shift b1 64 +. b0); | ||
| == {lemma_add_associate ((shift a1 64) +. a0) (shift b1 64) b0} | ||
| ((shift a1 64) +. a0 +. shift b1 64) +. b0; | ||
| == {lemma_add_commute (shift a1 64) a0} |
There was a problem hiding this comment.
can't a lot of these be done with the semiring tactic? that sounds very labor intensive doing all of these steps by hand
There was a problem hiding this comment.
How can I learn about semiring tactic? or where can I look for example?
|
@msprotz Thanks for reviewing the code, I agree that documentation for AES-GCM API should be in-depth and more helpful for the user. I will see how I can put such doc up tomorrow. |
This PR imports NI modules of GHASH from
pnmadelaine_aesbranch and adds specific proofs. However, the proofs use properties and definitions from Vale modules so there's still some work left before this PR can be merged.