From 344e403ab577c60603e537cab836ef056bba157d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 11 Oct 2019 16:42:05 -0400 Subject: [PATCH] Better conversion to 32-bit for bedrock2 c.f. https://github.com/mit-plv/fiat-crypto/issues/524#issuecomment-540059615 --- src/Rewriter/Rules.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v index 1a7830680d..2f8a5f09d8 100644 --- a/src/Rewriter/Rules.v +++ b/src/Rewriter/Rules.v @@ -851,14 +851,16 @@ Section with_bitwidth. ; (forall xl xh offset, 0 < offset < bitwidth -> doublewidth (cstZsingle_to_double xl xh >> singlewidth ('offset)) - = cstZsingle_to_double - (Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset))) - (singlewidth - (Z.truncating_shiftl - (singlewidth ('bitwidth)) - (singlewidth xh) - (singlewidth ('(bitwidth - offset)))))) - (singlewidth xh >> singlewidth ('offset))) + = (dlet l := singlewidth + (Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset))) + (singlewidth + (Z.truncating_shiftl + (singlewidth ('bitwidth)) + (singlewidth xh) + (singlewidth ('(bitwidth - offset)))))) in + dlet h := singlewidth + (singlewidth xh >> singlewidth ('offset)) in + cstZsingle_to_double l h)) ] ]. End with_bitwidth.