@@ -298,12 +298,16 @@ instance Ord (Bits n) where
298298 then EQ
299299 else GT
300300
301−complement' : machineTy n -> machineTy n
302−complement' {n=n} x with n
303− | O = prim__complB8 x
304− | S O = prim__complB16 x
305− | S (S O) = prim__complB32 x
306− | S (S (S _)) = prim__complB64 x
301+complement' : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
302+complement' {n=n} x with (log2Bytes n)
303+ | O = let pad = prim__intToB8 (8 - cast n) in
304+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
305+ | S O = let pad = prim__intToB16 (16 - cast n) in
306+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
307+ | S (S O) = let pad = prim__intToB32 (32 - cast n) in
308+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
309+ | S (S (S _)) = let pad = prim__intToB64 (64 - cast n) in
310+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
307311
308312public
309313complement : Bits n -> Bits n
@@ -328,39 +332,47 @@ public partial
328332zeroExtend : Bits n -> Bits (n+m)
329333zeroExtend (MkBits x) = MkBits (zext' x)
330334
335+-- Fill in the high bits of a sign-extended bitstring
336+fixupSE : (m : Nat) -> machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes (n+m))
337+fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))
338+
331339-- TODO: Prove
332340%assert_total
333341sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
334342sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
335− | (O, O) = believe_me x
336− | (O, S O) = believe_me (prim__sextB8_16 (believe_me x))
337− | (O, S (S O)) = believe_me (prim__sextB8_32 (believe_me x))
338− | (O, S (S (S _))) = believe_me (prim__sextB8_64 (believe_me x))
339− | (S O, S O) = believe_me x
340− | (S O, S (S O)) = believe_me (prim__sextB16_32 (believe_me x))
341− | (S O, S (S (S _))) = believe_me (prim__sextB16_64 (believe_me x))
342− | (S (S O), S (S O)) = believe_me x
343− | (S (S O), S (S (S _))) = believe_me (prim__sextB32_64 (believe_me x))
344− | (S (S (S _)), S (S (S _))) = believe_me x
343+ | (O, O) = fixupSE m (believe_me x)
344+ | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))
345+ | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))
346+ | (O, S (S (S _))) = fixupSE m (believe_me (prim__sextB8_64 (believe_me x)))
347+ | (S O, S O) = fixupSE m (believe_me x)
348+ | (S O, S (S O)) = fixupSE m (believe_me (prim__sextB16_32 (believe_me x)))
349+ | (S O, S (S (S _))) = fixupSE m (believe_me (prim__sextB16_64 (believe_me x)))
350+ | (S (S O), S (S O)) = fixupSE m (believe_me x)
351+ | (S (S O), S (S (S _))) = fixupSE m (believe_me (prim__sextB32_64 (believe_me x)))
352+ | (S (S (S _)), S (S (S _))) = fixupSE m (believe_me x)
345353
346354public partial
347355signExtend : Bits n -> Bits (n+m)
348356signExtend (MkBits x) = MkBits (sext' x)
349357
358+-- Zero out the high bits of a truncated bitstring
359+fixupTR : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
360+fixupTR x = x `and'` complement' (intToBits' 0)
361+
350362-- TODO: Prove
351363%assert_total
352364trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
353365trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
354− | (O, O) = believe_me x
366+ | (O, O) = fixupTR (believe_me x)
355367 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
356368 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
357369 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
358− | (S O, S O) = believe_me x
370+ | (S O, S O) = fixupTR (believe_me x)
359371 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
360372 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
361− | (S (S O), S (S O)) = believe_me x
373+ | (S (S O), S (S O)) = fixupTR (believe_me x)
362374 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
363− | (S (S (S _)), S (S (S _))) = believe_me x
375+ | (S (S (S _)), S (S (S _))) = fixupTR (believe_me x)
364376
365377public partial
366378truncate : Bits (n+m) -> Bits n