search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
395 stars 59 forks source link

(RFC) Add a test for mul_underspec #446

Closed mtzguido closed 3 months ago

mtzguido commented 3 months ago

Hi Jonathan, this PR adds a test for mul_underspec to test the patch in https://github.com/FStarLang/FStar/pull/3349.

I had to use this irreducible four definition to prevent the normalizer from simpliyfing the operation, so we actually try to extract it. Not sure if you have a better way?

I don't know if this is of much value as-is, maybe we can beef it up with other operations/widths too. For that I think main would look like

if not (test1 ()) then 1l else
if not (test2 ()) then 1l else
if not (test3 ()) then 1l else
...

or something similar.

msprotz commented 3 months ago

I usually use an effectful function that returns a constant to prevent optimizations. But this is fine too! Thanks, this looks good to me, you can go ahead and merge. Thanks so much.

mtzguido commented 3 months ago

Thanks! Sorry, I should have removed the (RFC) before merging...