1	import Base
2	import ../../../spec/crypto/curve25519/field.bend as FS
3	import ../../../spec/crypto/ed25519.bend as SE
4	import ../../../spec/crypto/sha512.bend as SHA
5	import ../../../src/crypto/hash.bend as H
6	import ../../../src/crypto/sha512/types.bend as T512
7	import ../../../src/crypto/sha512/core.bend as C512
8	import ../../../src/crypto/curve25519/field.bend as F
9	import ../../../src/crypto/curve25519/x25519.bend as X
10	import ../../../src/crypto/ed25519/ed25519.bend as E
11	import ../../lib/logic.bend as L
12	import ../../math/hash/hash.bend as HH
13	import ../sha512/conformance.bend as S512
14	import ../curve25519/limbs.bend as LM
15	
16	# Byte-string facts for Ed25519: the implementation's take / drop / cat are
17	# the spec's first / rest / cat; a SHA-512 digest is 64 bytes, each below
18	# 256, and equals FIPS 180-4's (proofs/crypto/sha512/conformance.bend).
19	
20	def v(+x: U32) -> Nat:
21	  U32.to_nat(x)
22	
23	# ---- take, drop, cat ----
24	
25	def take_eq(+n: Nat, +xs: List<&2, U32>) -> {F.take(n, xs) == SE.first(n, xs) : List<&2, U32>}:
26	  match n:
27	    case 0n:
28	      {==}
29	    case 1n+ +m:
30	      match xs:
31	        case Nil{}:
32	          {==}
33	        case Con{+x, +xt}:
34	          Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, F.take(m, xt), SE.first(m, xt), take_eq(m, xt))
35	
36	def drop_eq(+n: Nat, +xs: List<&2, U32>) -> {F.drop(n, xs) == SE.rest(n, xs) : List<&2, U32>}:
37	  match n:
38	    case 0n:
39	      {==}
40	    case 1n+ +m:
41	      match xs:
42	        case Nil{}:
43	          {==}
44	        case Con{+x, +xt}:
45	          drop_eq(m, xt)
46	
47	def cat_eq(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {E.cat(xs, ys) == SE.cat(xs, ys) : List<&2, U32>}:
48	  match xs:
49	    case Nil{}:
50	      {==}
51	    case Con{+x, +xt}:
52	      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{x, z}, E.cat(xt, ys), SE.cat(xt, ys), cat_eq(xt, ys))
53	
54	# n + m, by recursion on n
55	def pl(n: Nat, +m: Nat) -> Nat:
56	  match n:
57	    case 0n:
58	      m
59	    case 1n+k:
60	      1n+pl(k, m)
61	
62	def take_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(n, F.take(n, xs), b) == True{} : Bool}:
63	  match n:
64	    case 0n:
65	      {==}
66	    case 1n+ +k:
67	      match xs:
68	        case Nil{}:
69	          e
70	        case Con{+x, +xt}:
71	          L.and_intro(Nat.is_le(v(x), b), LM.okb(k, F.take(k, xt), b), L.and_left(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e), take_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e)))
72	
73	def drop_okb(+n: Nat, +m: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(pl(n, m), xs, b) == True{} : Bool}) -> {LM.okb(m, F.drop(n, xs), b) == True{} : Bool}:
74	  match n:
75	    case 0n:
76	      e
77	    case 1n+ +k:
78	      match xs:
79	        case Nil{}:
80	          Empty.absurd({LM.okb(m, Nil{}, b) == True{} : Bool}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
81	        case Con{+x, +xt}:
82	          drop_okb(k, m, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(pl(k, m), xt, b), e))
83	
84	# 8 n
85	def e8(n: Nat) -> Nat:
86	  match n:
87	    case 0n:
88	      0n
89	    case 1n+k:
90	      Nat.add(8n, e8(k))
91	
92	def bitlen_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {LM.okb(n, xs, b) == True{} : Bool}) -> {X.bitlen(xs) == e8(n) : Nat}:
93	  match n xs:
94	    case 0n Nil{}:
95	      {==}
96	    case 0n Con{x, xt}:
97	      Empty.absurd({X.bitlen(Con{x, xt}) == 0n : Nat}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
98	    case 1n+k Nil{}:
99	      Empty.absurd({0n == e8(1n+k) : Nat}, L.true_false(Equal.sym(Bool, False{}, True{}, e)))
100	    case 1n+ +k Con{+x, +xt}:
101	      Equal.cong(Nat, Nat, z => Nat.add(8n, z), X.bitlen(xt), e8(k), bitlen_okb(k, xt, b, L.and_right(Nat.is_le(v(x), b), LM.okb(k, xt, b), e)))
102	
103	def bitlen_256(+xs: List<&2, U32>, +e: {LM.okb(32n, xs, 255n) == True{} : Bool}) -> {X.bitlen(xs) == 256n : Nat}:
104	  bitlen_okb(32n, xs, 255n, e)
105	
106	# ---- SHA-512 ----
107	
108	def sha_eq(+bytes: List<&2, U32>) -> {H.sha512(bytes) == SHA.sha512_bytes(bytes) : List<&2, U32>}:
109	  S512.sha512_correct(bytes)
110	
111	def byte_and(+x: U32) -> {Nat.is_le(v(U32.and(x, 255)), 255n) == True{} : Bool}:
112	  HH.and_le32(x, 255)
113	
114	def okb_con(+n: Nat, +x: U32, +t: List<&2, U32>, +hx: {Nat.is_le(v(x), 255n) == True{} : Bool}, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(1n+n, Con{x, t}, 255n) == True{} : Bool}:
115	  L.and_intro(Nat.is_le(v(x), 255n), LM.okb(n, t, 255n), hx, ht)
116	
117	def octets_okb(+n: Nat, +x: U32, +t: List<&2, U32>, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(4n+n, C512.octets(x, t), 255n) == True{} : Bool}:
118	  +b0 = U32.and(x, 255)
119	  +b1 = U32.and(U32.shrn(x, 8n), 255)
120	  +b2 = U32.and(U32.shrn(x, 16n), 255)
121	  +b3 = U32.and(U32.shrn(x, 24n), 255)
122	  +l0 = okb_con(n, b0, t, byte_and(x), ht)
123	  +l1 = okb_con(1n+n, b1, Con{b0, t}, byte_and(U32.shrn(x, 8n)), l0)
124	  +l2 = okb_con(2n+n, b2, Con{b1, Con{b0, t}}, byte_and(U32.shrn(x, 16n)), l1)
125	  okb_con(3n+n, b3, Con{b2, Con{b1, Con{b0, t}}}, byte_and(U32.shrn(x, 24n)), l2)
126	
127	def lane_okb(+n: Nat, +l: T512.Lane, +t: List<&2, U32>, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(8n+n, C512.lane_octets(l, t), 255n) == True{} : Bool}:
128	  match l:
129	    case T512.W{+hi, +lo}:
130	      octets_okb(4n+n, hi, C512.octets(lo, t), octets_okb(n, lo, t, ht))
131	
132	def digest_okb(+s: T512.State) -> {LM.okb(64n, C512.digest_bytes(s), 255n) == True{} : Bool}:
133	  match s:
134	    case T512.H{+a, +b, +c, +d, +e, +f, +g, +h}:
135	      +th = C512.lane_octets(h, Nil{})
136	      +tg = C512.lane_octets(g, th)
137	      +tf = C512.lane_octets(f, tg)
138	      +te = C512.lane_octets(e, tf)
139	      +td = C512.lane_octets(d, te)
140	      +tc = C512.lane_octets(c, td)
141	      +tb = C512.lane_octets(b, tc)
142	      lane_okb(56n, a, tb, lane_okb(48n, b, tc, lane_okb(40n, c, td, lane_okb(32n, d, te, lane_okb(24n, e, tf, lane_okb(16n, f, tg, lane_okb(8n, g, th, lane_okb(0n, h, Nil{}, {==}))))))))
143	
144	# a digest: 64 bytes, each below 256
145	def sha_okb(+bytes: List<&2, U32>) -> {LM.okb(64n, H.sha512(bytes), 255n) == True{} : Bool}:
146	  digest_okb(C512.blocks(C512.lanes(List.append(&2, U32, bytes, C512.suffix(List.length(&2, U32, bytes)))), 64n, C512.round_constants(), C512.initial()))
147	
148	def sha_lea(+bytes: List<&2, U32>) -> {LM.lea(H.sha512(bytes), 255n) == True{} : Bool}:
149	  LM.okb_lea(64n, H.sha512(bytes), 255n, sha_okb(bytes))