Reflection #
We have a decision procedure which operates on BitStream operations, but we'd like
Preliminaries #
Append a single bit to the least significant end of a bitvector. That is, the new bit is the least significant bit.
Equations
- BitStream.concat b x 0 = b
- BitStream.concat b x i.succ = x i
Instances For
map f maps a (unary) function over a bitstreams
Equations
- BitStream.map f x i = f (x i)
Instances For
mapAccum₂ ("binary map accumulate") maps a binary function f over two streams,
while accumulating some state
Equations
- One or more equations did not get rendered due to their size.
Instances For
The field projection .1 distributes over function composition, so we can compute
the first field of the result of the composition by repeatedly composing the first projection.
Coinduction principle for corec.
To show that corec f a = corec g b,
we must show that:
- The relation
R a bis inhabited ["base case"] - Given that
R a bholds, thenR (f a) (g b)holds [coinductive case]
OfNat #
Zero-extend a natural number to an infinite bitstream
Equations
- BitStream.ofNat x = x.testBit
Instances For
Equations
- BitStream.instOfNat = { ofNat := BitStream.ofNat n }
Sign-extend a finite bitvector x to the infinite stream (x.msb)^ω ⋅ x
Equations
- BitStream.ofBitVec x i = if i < w then x.getLsbD i else x.msb
Instances For
x.toBitVec w returns the first w bits of bitstream x
Equations
- BitStream.toBitVec 0 x = 0#0
- BitStream.toBitVec i.succ x = BitVec.cons (x i) (BitStream.toBitVec i x)
Instances For
EqualUpTo w x y holds iff x and y are equal in the first w bits
Equations
- BitStream.EqualUpTo w x y = ∀ i < w, x i = y i
Instances For
Bitwise Operations #
Equations
- BitStream.instComplement = { complement := BitStream.map not }
Equations
- BitStream.instAndOp = { and := BitStream.map₂ and }
Equations
- BitStream.instOrOp = { or := BitStream.map₂ or }
Equations
- BitStream.instXor = { xor := BitStream.map₂ xor }
Addition, Subtraction, Negation #
Equations
- x.addAux y 0 = (BitVec.adcb (x 0) (y 0) false).swap
- x.addAux y i_1.succ = (BitVec.adcb (x i_1.succ) (y i_1.succ) (x.addAux y i_1).2).swap
Instances For
Equations
- BitStream.instAdd = { add := BitStream.add }
Equations
- BitStream.instNeg = { neg := BitStream.neg }
Equations
- BitStream.instSub = { sub := BitStream.sub }
repeatBit xs will repeat the first bit of xs which is true.
That is, it will be all-zeros iff xs is all-zeroes,
otherwise, there's some number k so that after dropping the k least
significant bits, repeatBit xs is all-ones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
TODO: We should define addition and carry in terms of mapAccum.
For example:
def add := mapAccum₂ BitVec.adcb false
and
def carry : BitStream → BitStream → BitStream :=
mapAccum₂ (fun c x₀ y₀ =>
let c' := Bool.atLeastTwo c x₀ y₀
(c', c')
) false
Following the same pattern as for ofBitVec_and, _or, etc., we would expect an equality like:
ofBitVec (x + y) = (ofBitVec x) + (ofBitVec y)
However, this is not actually true, since the left hand side does addition on the bitvector level,
thus forgets the extra carry bit, while rhe rhs does addition on streams,
thus could have a bit set in the w+1th position.
Crucially, our decision procedure works by considering which equalities hold for all widths,
Will subAux overflow/carry when computing a - b?
Equations
Instances For
Equations
- BitStream.congr_trans = { trans := ⋯ }
OfInt #
Using OfInt we can convert an Int into the infinite bitstream that represents that
particular constant
Sign-extend an integer to its representation as a 2-adic number (morally, an infinite width 2s complement representation)
Equations
- BitStream.ofInt (Int.ofNat n) = BitStream.ofNat n
- BitStream.ofInt (Int.negSucc n) = -BitStream.ofNat (n + 1)