1	import 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.)
8	def 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).
13	def 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).
17	def 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.
21	def 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.
27	def 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.
32	def 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).
36	def 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.
53	def 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.
58	def 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.
63	def bcast(+b: U32) -> U32:
64	  pack4(b, b, b, b)