ROMemories
ROMemories
Is proof generation a deterministic/reproducible process? If so, maybe it would make sense to only store cryptographic hashes of the resulting proofs?
> A locked version of Rust, its dependencies and of hax should always produce the same extraction, that's (or should be!) a deterministic process. > I think we converge to...
This is still a blocker for us.
I simplified the reproducer a lot; the error message seems to be different now (this seems to be a change in hax, not caused by the simplification), and *F\* extraction*...
I think the multiple-quantification trick does the job, thanks!
This issue is still relevant.
Pondering on this some more, it seems to be me that the platform being multicore or not is actually irrelevant, it just has to support multi-threading for this to be...
> But then you'll most likely also not have threads. These MCUs—the RP2040 and the ESP32-C3 (RISC-V without the (A) extension) for instance—*do* support threading however, and we do support...
> (it's something to docs already call out: https://docs.rs/log/latest/log/fn.set_logger_racy.html#safety) The docs mention that: > It is safe to use other logging functions while this function runs (including all logging macros)....
Workaround A should work now that cryspen/hax#1016 is fixed. However I think the original limitation is still there so I'm not sure whether this issue can be closed. We're currently...