defs.bend
1import Base
2
3# lawful-words definitions. The laws are in LAWS.bend.
4
5# 2^32, for prose and tests. The laws write Nat.pow(2n, 32n) inline instead:
6# the checker evaluates a named constant when comparing terms, and 2^32 in
7# unary is too deep to evaluate. (A Nat literal of 2^32 or more is not allowed.)
8def two32() -> Nat:
9 Nat.pow(2n, 32n)
10
11# n modulo 2^32: the number U32.from_nat(n) stands for (the laws write
12# Nat.mod(n, Nat.pow(2n, 32n)) inline, for the same reason).
13def wrap(n: Nat) -> Nat:
14 Nat.mod(n, two32())
15
16# Bit k of a word (bit 0 is the lowest; every bit from 32 up is 0).
17def bit(a: U32, k: Nat) -> Bool:
18 Nat.is_eq(Nat.mod(Nat.div(U32.to_nat(a), Nat.pow(2n, k)), 2n), 1n)
19
20# Byte j of a word (byte 0 is the lowest): (w >> 8j) & 255.
21def byte(w: U32, j: Nat) -> U32:
22 U32.and(U32.shrn(w, Nat.mul(8n, j)), 255)
23
24# w with byte j replaced by b: (w & ~(255 << 8j)) | (b << 8j). Meant for
25# b < 256 and j < 4: a larger b spills into the next byte, and from j = 4 up
26# the word is unchanged.
27def put_byte(w: U32, +j: Nat, b: U32) -> U32:
28 U32.or(U32.and(w, U32.not(U32.shln(255, Nat.mul(8n, j)))), U32.shln(b, Nat.mul(8n, j)))
29
30# The word whose bytes 0 to 3 are b0 to b3: b0 | b1 << 8 | b2 << 16 | b3 << 24.
31# Meant for bytes below 256: larger values spill into the next byte.
32def pack4(b0: U32, b1: U32, b2: U32, b3: U32) -> U32:
33 U32.or(b0, U32.or(U32.shln(b1, 8n), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n))))
34
35# The j-th of four values (j = 0 to 3; b3 from 3 up).
36def nth4(j: Nat, b0: U32, b1: U32, b2: U32, b3: U32) -> U32:
37 match j:
38 case 0n:
39 b0
40 case 1n+p:
41 match p:
42 case 0n:
43 b1
44 case 1n+q:
45 match q:
46 case 0n:
47 b2
48 case 1n+t:
49 b3
50
51# The word that starts r bytes into the pair (lo, hi), r from 0 to 4:
52# (lo >> 8r) | (hi << 8(4 - r)). Copying at any alignment reads such words.
53def merge(lo: U32, hi: U32, +r: Nat) -> U32:
54 U32.or(U32.shrn(lo, Nat.mul(8n, r)), U32.shln(hi, Nat.mul(8n, Nat.sub(4n, r))))
55
56# The zero-byte flags: (v - 0x01010101) & ~v & 0x80808080. It is zero exactly
57# when no byte of v is zero (law zb_zero); individual flags are not exact.
58def zb(+v: U32) -> U32:
59 U32.and(U32.and(U32.sub(v, 16843009), U32.not(v)), 2155905152)
60
61# A byte repeated in all four bytes: searching for b is searching xor(w, bcast(b))
62# for a zero byte.
63def bcast(+b: U32) -> U32:
64 pack4(b, b, b, b)