GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 22:17:18 +03:00
Code Issues Projects Releases Wiki Activity

Fix reference semantics of the signed bitvector primitives

Browse Source
This commit is contained in:
Rob Dockins 2020-05-27 15:34:58 -07:00
parent 0bc02bcae0
commit 897f631910
2 changed files with 7 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
docs/Semantics.pdf
View File

Binary file not shown.

17
src/Cryptol/Eval/Reference.lhs
View File

@ -632,11 +632,11 @@ by corresponding typeclasses
> , ("/$" , vFinPoly $ \n ->
> VFun $ \l ->
> VFun $ \r ->
> vWord n $ appOp2 divWrap (fromVWord l) (fromVWord r))
> vWord n $ appOp2 divWrap (fromSignedVWord l) (fromSignedVWord r))
> , ("%$" , vFinPoly $ \n ->
> VFun $ \l ->
> VFun $ \r ->
> vWord n $ appOp2 modWrap (fromVWord l) (fromVWord r))
> vWord n $ appOp2 modWrap (fromSignedVWord l) (fromSignedVWord r))
> , (">>$" , signedShiftRV)
> , ("lg2" , vFinPoly $ \n ->
> VFun $ \v ->
@ -1299,20 +1299,17 @@ amount, but as lazy as possible in the list values.
>
> signedShiftRV :: Value
> signedShiftRV =
> VNumPoly $ \n ->
> VNumPoly $ \(Nat n) ->
> VPoly $ \ix ->
> VFun $ \v ->
> VFun $ \x ->
> copyByTValue (tvSeq n TVBit) $
> copyByTValue (tvSeq (Nat n) TVBit) $
> case cryToInteger ix x of
> Left e -> cryError e (tvSeq n TVBit)
> Right i -> VList n $
> Left e -> cryError e (tvSeq (Nat n) TVBit)
> Right i -> VList (Nat n) $
> let vs = fromVList v
> z = head vs in
> case n of
> Nat m -> genericReplicate (min m i) z ++ genericTake (m - min m i) vs
> Inf -> genericReplicate i z ++ vs
> genericReplicate (min n i) z ++ genericTake (n - min n i) vs
Indexing
--------