Place ONE bit, given the bit's TARGET position and the bit itself.
This used to take the field's value and a bit index and recover the bit with
`value / 2^bitIndex mod 2`. That `2^bitIndex` is the reason the encoder could
not be run: naturals are unary here, so `naturalPowerOfTwo 31` -- what a
field at bit 31 needs -- materialises a successor chain of 2,147,483,648
elements, and the divide beside it is repeated subtraction over that numeral.
Measured, 2^22 alone took 921 ms; one instruction is 128 such placements.
The caller now threads the value, halving it per bit, so the only power left
here is `2^(targetBit mod 8)` -- at most 128, because a bit's home inside a
byte is what it is regardless of how wide the field is.
255def sm86PlaceBitAt =
256 (lambda unrestricted targetBit : Nat .
257 (lambda unrestricted sourceBit : Nat .
258 (lambda unrestricted encoded : Bytes .
259 (app
260 (lambda unrestricted targetByteIndex : Nat .
261 (app
262 (lambda unrestricted targetBitIndex : Nat .
263 (app
264 (lambda unrestricted targetPower : Nat .
265 (app
266 (lambda unrestricted priorByte : Nat .
267 (app
268 (lambda unrestricted priorBit : Nat .
269 (sm86ReplaceByteAt
270 targetByteIndex
271 (nat-to-byte
272 (naturalAdd
273 (naturalSaturatingSubtract
274 priorByte
275 (naturalMultiply priorBit targetPower))
276 (naturalMultiply sourceBit targetPower)))
277 encoded))
278 (naturalModuloUnchecked
279 (naturalDivideUnchecked priorByte targetPower)
280 sm86EncodingNaturalTwo)))
281 (byte-to-nat (sm86ByteAt targetByteIndex encoded))))
282 (naturalPowerOfTwo targetBitIndex)))
283 (naturalModuloUnchecked targetBit sm86EncodingNaturalEight)))
284 (naturalDivideUnchecked targetBit sm86EncodingNaturalEight)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.