1	import Base
2	import ../types/model.bend as T
3	import ../../../../spec/lib/numeric.bend as W
4	
5	# The word model lives in spec/lib/numeric.bend; its names are kept here as
6	# one-line aliases for the proofs that use them, next to the cache model's
7	# Int64 interpretation (expiry, deadlines).
8	
9	def bit_value(b: Bool) -> Nat:
10	  W.bit_value(b)
11	
12	def unsigned(n: Nat, w: Word(n)) -> Nat:
13	  W.unsigned(n, w)
14	
15	def sign_threshold(n: Nat) -> Word(1n+n):
16	  W.sign_threshold(n)
17	
18	def negative(+w: Word(64n)) -> Bool:
19	  W.negative(w)
20	
21	def zero(w: Word(64n)) -> Bool:
22	  W.zero(w)
23	
24	def order(a: Word(64n), b: Word(64n), sign_a: Bool, sign_b: Bool) -> Bool:
25	  W.order(a, b, sign_a, sign_b)
26	
27	def expired(deadline: T.Int64, now: T.Int64) -> Bool:
28	  match deadline now:
29	    case T.I64{+a} T.I64{+b}:
30	      Bool.not(zero(a)) && order(a, b, negative(a), negative(b))
31	
32	def from_nat(n: Nat, +value: Nat) -> Word(n):
33	  W.from_nat(n, value)
34	
35	def modulus() -> Nat:
36	  W.modulus()
37	
38	def unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
39	  W.unsigned_quotient(n, word, d)
40	
41	def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
42	  W.negative_quotient(n, word, d)
43	
44	def quotient_signed(bits: Word(64n), negative: Bool) -> Word(64n):
45	  W.quotient_signed(bits, negative)
46	
47	def milliseconds(duration: T.Int64) -> T.Int64:
48	  T.I64{+bits} = duration
49	  T.I64{quotient_signed(bits, negative(bits))}
50	
51	def add(a: T.Int64, b: T.Int64) -> T.Int64:
52	  match a b:
53	    case T.I64{x} T.I64{y}:
54	      T.I64{from_nat(64n, Nat.add(unsigned(64n, x), unsigned(64n, y)))}
55	
56	def expiry_choose(now: T.Int64, duration: T.Int64, forever: Bool) -> T.Int64:
57	  match forever:
58	    case True{}:
59	      T.I64{Word.zero(64n)}
60	    case False{}:
61	      add(now, milliseconds(duration))
62	
63	def deadline(now: T.Int64, duration: T.Int64) -> T.Int64:
64	  T.I64{+bits} = duration
65	  expiry_choose(now, T.I64{bits}, zero(bits))
66	
67	def scale_binary(places: Nat, value: Nat) -> Nat:
68	  W.scale_binary(places, value)