Bas Spitters
Bas Spitters
adding Halo2 ### Description ### Checklist - [ ] The description above is sufficient to understand the PR - [ ] The code compiles correctly - [ ] The code...
@raoxiaojia and others, with @jeanpichon we are discussing how to host the work on certicoq-wasm with @womeier for posterity. We're considering Coq community as, personally, I have very good experiences...
There are various initiatives to understand subsets of safe rust more formally. For example, [hacspec](https://github.com/hacspec/hacspec/blob/master/formalization/formalization.pdf) or [oxide](https://github.com/aatxe/oxide). What would it take for such initiatives to be considered "correct". Is there...
A gitter discussion suggested making stdlib2 compatible with [stdpp](https://gitlab.mpi-sws.org/iris/stdpp). Is that a realistic goal? @robbertkrebbers @RalfJung
Coqide comes up and then dies ... It does raise an error message, but it disappears to fast to read it. If you give me a clue about where the...
I understand rupicola uses bedrock2, which can produce RISC-V. Is there a way to output C or rust from Rupicola/bedrock2?
There may be a possibility to avoid duplication... https://github.com/coq/coq/pull/17043
This looks like a bug: https://coq.zulipchat.com/#narrow/channel/237659-Equations-devs-.26-users/topic/Equations.20vs.20Function/near/486295559
The definition of fvec_to_vec below, is non-idiomatic, but I believe should give better error messages. Coq complains: > Functional induction principle could not be proved automatically, it is left as...
@cmester0 suggested to have (nominal) names for "wires" e.g. names of functions. This would be helpful in Bert13 TLS where wires can be indexed by e.g. the round. @MarkusKL responded:...