Bas Spitters
Bas Spitters
@bshvass What is the status of this?
@bshvass we should probably try with hacl-rs (including hmac and bignum), as it would compile to wasm.
Yes, we would like to do that, but currently lack the resources at AU. You are pointing to the hacspec specification, but as you can see here: https://github.com/AU-COBRA/AUCurves/blob/main/src/Hacspec/Curve/BlsProof.v The pairing...
LGTM. Do we need MachineIntegers.v? The readme says to install it via opam.
> From what I can see `MachineIntergers.v` file is not directly part of CompCert library, so we do need it here. Interesting. So, where does it come from then? If...
Yes, that seems like a likely source. It's possible that we are just using an old version. For the last yard, we've switched to the math-comp integers. It would be...
Why are you going back to the compcert integers? The jasmin/math-comp ones are needed for the jasmin connection. Getting this merged would help us make a choice. Moreover, that library...
Ok. Yes, that's a good idea. Didn't we use the MC/jasmin integers for the SSProve backend? On Mon, Mar 25, 2024 at 3:08 PM Lasse Letager Hansen < ***@***.***> wrote:...
1. is nice, but indeed seems very tedious. 2. Pure may become quite small and also an artificial way of placing files. Will we have Pure/categories/... ? 3. I am...
I think that might work. It is sufficiently uninvasive to be workable. On Wed, Oct 29, 2014 at 9:13 AM, Mike Shulman [email protected] wrote: > What about a version of...