Bas Spitters
Bas Spitters
@beurdouche Thanks. As you know the library well. How much of the issues above are already provided by F*.
Fiat cryptography produces straight line code. Would that be constant time in wasm?
Just curious, AWS has their (formally verified) s2n bignum assembly library. https://github.com/awslabs/s2n-bignum It looks like there may be rust bindings for it. Would that solve any of these issues?
From @protz: HACL* extracted as pure safe Rust (dubbed "HACL-rs") lives here: https://github.com/hacl-star/hacl-star/tree/afromher_rs/dist/rs In there, you'll find bignums in src/hacl: - bignum.rs, bignum64.rs: variable-length, 32 and 64-bit versions (scattered across...
I wonder how it compares to Jasmin's https://github.com/haslab/libjbn
So far, stdlib2 seems to be mostly following the math-comp style. stdpp uses a different style (type classes, for example). E.g. how do we expect the finmap library to look?
More experiments here: https://github.com/coq/stdlib2/wiki/EqClass
Perhaps the real question here is what should be the intended semantics of stdlib2? Should it be vanille type theory, HoTT, or perhaps HoTT with classical axioms. @SkySkimmer is working...
If one is serious about this semantics one should use setoids throughout, at least for structures with possibly non-decidable equality. When the equality can be assumed to be decidable the...
I think as long as there is a unified view of what the intended semantics is, that could be a reasonable choice. It would be interesting to see what can...