Bas Spitters

@samuelgruetter I see there's a bit of progress on spilling in bedrock2. Is there a convenient way to use it from fiat-crypto so that we can use it to time...

Thanks @samuelgruetter . Coming back to the original question, with your work, would it now be feasible to write a jasmin backend for bedrock2?

@samuelgruetter I was wondering about the status of this issue. It seems you now have spilling https://github.com/mit-plv/bedrock2/commit/19fe67d23eafc5c7f7a676284c13694402803bf0 and are even working on new spilling https://github.com/mit-plv/bedrock2/commit/170a56324c52bd9d1be623dd51b8fa4fb6215e01 Does that make any progress...

Thanks for the link to the nice paper! Our application is not set in stone, and to some extend it is a conceptual question: How can we bridge the gap...

I guess C would be the easiest to start with. Bedrock comes with a set of other dependencies.

Zulip seems to work well, both for hacspec, and sometimes in the rust formal verification stream.

Zulip was also used quite effectively for the rust verification workshop. It the common platform for most people in verification. I currently have 8 of them open. It would be...

@tarcieri What's the reason for having a separate zulip for rustcrypto. I find it easier to follow streams in the general rust zulip. It would also increase the visibility of...

Somehow the link does not work for me. On Mon, May 31, 2021 at 11:07 PM Tony Arcieri ***@***.***> wrote: > Okay, it seems there are enough people in favor...

@tarcieri since you mentioned RISC-V. There's some discussion on adding constant time to the Spec. https://github.com/riscv/riscv-v-spec/issues/417