Aymeric Fromherz
Aymeric Fromherz
I'd go for simply `bst`
I'd be curious about the second part, it seems like it could also optimize heavily some of the current VCs. Regarding your first suggestion, do you mean to expose this...
Sure, I can give it a shot. Regarding 1, I'm wondering if there are usecases where we would *not* want to have canonicalization, especially if the SMT encoding is not...
We discussed this during today's F* developers meeting. The conclusion was that the way forward might be to revive a variant of #2305, but applied during reflection (inside pack) instead...
Below is a small example (courtesy of @TWal) of how the behavior presented in this issue can cause issues with reflection. With the current behavior, the SMTPat is not triggered,...
The error seems to come from Charon not recognizing internal operations in the `vec!` macro, leading to the following unsafe cast in LLBC (on an equivalent example with a bool...
For soft constraints, I'd personally be in favor of an external config file, I'm worried that these soft constraints would quickly pollute Catala code. But we should experiment first with...
I tend to agree, I'm not sure how much the additional indirection brings, apart from shortening the commands
CI failures were due to the transition between CI machines. dist refresh should occur with the latest HACL* in two days. Closing in the meantime