1	import Base
2	import ../../../src/crypto/chacha/chacha20.bend as I
3	import ../../../spec/crypto/chacha.bend as R
4	import ./laws.bend as Laws
5	import ./stream.bend as T
6	import ./xchacha.bend as X
7	import ./involution.bend as V
8	
9	# Entry point: `bend proofs/crypto/chacha/proof.bend` checks every clause of
10	# laws.bend (the core refinement is proofs/crypto/chacha/core.bend, the
11	# byte-level stream stream.bend, HChaCha20/XChaCha20 xchacha.bend, the
12	# involution involution.bend).
13	
14	def Laws.block_rounds(r, key, counter, nonce):
15	  T.block_rounds_correct(r, key, counter, nonce)
16	
17	def Laws.encrypt_rounds(r, key, counter, nonce, plaintext):
18	  T.encrypt_correct(r, key, counter, nonce, plaintext)
19	
20	def Laws.hchacha_rounds(r, key, nonce):
21	  X.hchacha_rounds_correct(r, key, nonce)
22	
23	def Laws.hchacha20(key, nonce):
24	  X.hchacha20_correct(key, nonce)
25	
26	def Laws.xencrypt(key, counter, nonce, plaintext):
27	  X.xencrypt_correct(key, counter, nonce, plaintext)
28	
29	# ---- checked API
30	
31	law when_true:
32	  for +ok: Bool
33	  for +x: List<&2, U32>
34	  for +h: {ok == True{} : Bool}
35	  {I.when(ok, x) == Some{x} : Maybe<&2, List<&2, U32>>}
36	
37	def when_true(ok, x, h):
38	  %Equal.sym(Bool, ok, True{}, h) : {I.when(_, x) == Some{x} : Maybe<&2, List<&2, U32>>}
39	  {==}
40	
41	law when_false:
42	  for +ok: Bool
43	  for +x: List<&2, U32>
44	  for +h: {ok == False{} : Bool}
45	  {I.when(ok, x) == None{} : Maybe<&2, List<&2, U32>>}
46	
47	def when_false(ok, x, h):
48	  %Equal.sym(Bool, ok, False{}, h) : {I.when(_, x) == None{} : Maybe<&2, List<&2, U32>>}
49	  {==}
50	
51	law valid_true:
52	  for +key: List<&2, U32>
53	  for +nonce: List<&2, U32>
54	  for +n: Nat
55	  for +hk: {List.length(&2, U32, key) == 32n : Nat}
56	  for +hn: {List.length(&2, U32, nonce) == n : Nat}
57	  {I.valid(key, nonce, n) == True{} : Bool}
58	
59	def is_eq_self(+n: Nat) -> {Nat.is_eq(n, n) == True{} : Bool}:
60	  match n:
61	    case 0n: {==}
62	    case 1n+p: is_eq_self(p)
63	
64	def valid_true(key, nonce, n, hk, hn):
65	  %Equal.sym(Nat, List.length(&2, U32, key), 32n, hk) :
66	    {Bool.and(Nat.is_eq(_, 32n), Nat.is_eq(List.length(&2, U32, nonce), n)) == True{} : Bool}
67	  %Equal.sym(Nat, List.length(&2, U32, nonce), n, hn) :
68	    {Bool.and(Nat.is_eq(32n, 32n), Nat.is_eq(_, n)) == True{} : Bool}
69	  is_eq_self(n)
70	
71	def Laws.chacha20_block.valid(key, counter, nonce, hk, hn):
72	  Equal.trans(Maybe<&2, List<&2, U32>>, I.chacha20_block(key, counter, nonce), Some{I.block_rounds(10n, key, counter, nonce)}, Some{R.block(key, counter, nonce)},
73	    when_true(I.valid(key, nonce, 12n), I.block_rounds(10n, key, counter, nonce), valid_true(key, nonce, 12n, hk, hn)),
74	    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.block_rounds(10n, key, counter, nonce), R.block(key, counter, nonce), T.block_rounds_correct(10n, key, counter, nonce)))
75	
76	def Laws.chacha20_block.invalid(key, counter, nonce, h):
77	  when_false(I.valid(key, nonce, 12n), I.block_rounds(10n, key, counter, nonce), h)
78	
79	def Laws.chacha20.valid(key, counter, nonce, plaintext, hk, hn):
80	  Equal.trans(Maybe<&2, List<&2, U32>>, I.chacha20(key, counter, nonce, plaintext), Some{I.encrypt_rounds(10n, key, counter, nonce, plaintext)}, Some{R.encrypt(key, counter, nonce, plaintext)},
81	    when_true(I.valid(key, nonce, 12n), I.encrypt_rounds(10n, key, counter, nonce, plaintext), valid_true(key, nonce, 12n, hk, hn)),
82	    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.encrypt_rounds(10n, key, counter, nonce, plaintext), R.encrypt(key, counter, nonce, plaintext), T.encrypt_correct(10n, key, counter, nonce, plaintext)))
83	
84	def Laws.chacha20.invalid(key, counter, nonce, plaintext, h):
85	  when_false(I.valid(key, nonce, 12n), I.encrypt_rounds(10n, key, counter, nonce, plaintext), h)
86	
87	def Laws.hchacha20.valid(key, nonce, hk, hn):
88	  Equal.trans(Maybe<&2, List<&2, U32>>, I.hchacha20(key, nonce), Some{I.hchacha20_unchecked(key, nonce)}, Some{R.hchacha20(key, nonce)},
89	    when_true(I.valid(key, nonce, 16n), I.hchacha20_unchecked(key, nonce), valid_true(key, nonce, 16n, hk, hn)),
90	    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.hchacha20_unchecked(key, nonce), R.hchacha20(key, nonce), X.hchacha20_correct(key, nonce)))
91	
92	def Laws.hchacha20.invalid(key, nonce, h):
93	  when_false(I.valid(key, nonce, 16n), I.hchacha20_unchecked(key, nonce), h)
94	
95	def Laws.xchacha20.valid(key, counter, nonce, plaintext, hk, hn):
96	  Equal.trans(Maybe<&2, List<&2, U32>>, I.xchacha20(key, counter, nonce, plaintext), Some{I.xencrypt_unchecked(key, counter, nonce, plaintext)}, Some{R.xencrypt(key, counter, nonce, plaintext)},
97	    when_true(I.valid(key, nonce, 24n), I.xencrypt_unchecked(key, counter, nonce, plaintext), valid_true(key, nonce, 24n, hk, hn)),
98	    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.xencrypt_unchecked(key, counter, nonce, plaintext), R.xencrypt(key, counter, nonce, plaintext), X.xencrypt_correct(key, counter, nonce, plaintext)))
99	
100	def Laws.xchacha20.invalid(key, counter, nonce, plaintext, h):
101	  when_false(I.valid(key, nonce, 24n), I.xencrypt_unchecked(key, counter, nonce, plaintext), h)
102	
103	# ---- properties
104	
105	def Laws.involution(r, key, counter, nonce, plaintext):
106	  +ct = I.encrypt_rounds(r, key, counter, nonce, plaintext)
107	  +sct = R.encrypt_rounds(r, key, counter, nonce, plaintext)
108	  Equal.trans(List<&2, U32>, I.encrypt_rounds(r, key, counter, nonce, ct), R.encrypt_rounds(r, key, counter, nonce, ct), plaintext,
109	    T.encrypt_correct(r, key, counter, nonce, ct),
110	    Equal.trans(List<&2, U32>, R.encrypt_rounds(r, key, counter, nonce, ct), R.encrypt_rounds(r, key, counter, nonce, sct), plaintext,
111	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.encrypt_rounds(r, key, counter, nonce, l), ct, sct, T.encrypt_correct(r, key, counter, nonce, plaintext)),
112	      V.involution(r, key, counter, nonce, plaintext)))
113	
114	def Laws.xinvolution(key, counter, nonce, plaintext):
115	  +ct = I.xencrypt_unchecked(key, counter, nonce, plaintext)
116	  +sct = R.xencrypt(key, counter, nonce, plaintext)
117	  Equal.trans(List<&2, U32>, I.xencrypt_unchecked(key, counter, nonce, ct), R.xencrypt(key, counter, nonce, ct), plaintext,
118	    X.xencrypt_correct(key, counter, nonce, ct),
119	    Equal.trans(List<&2, U32>, R.xencrypt(key, counter, nonce, ct), R.xencrypt(key, counter, nonce, sct), plaintext,
120	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.xencrypt(key, counter, nonce, l), ct, sct, X.xencrypt_correct(key, counter, nonce, plaintext)),
121	      V.involution(10n, R.xsubkey(key, nonce), counter, R.xnonce(nonce), plaintext)))
122	
123	def Laws.encrypt_length(r, key, counter, nonce, plaintext):
124	  %Equal.sym(List<&2, U32>, I.encrypt_rounds(r, key, counter, nonce, plaintext), R.encrypt_rounds(r, key, counter, nonce, plaintext), T.encrypt_correct(r, key, counter, nonce, plaintext)) :
125	    {List.length(&2, U32, _) == List.length(&2, U32, plaintext) : Nat}
126	  V.encrypt_length(r, key, counter, nonce, plaintext)
127	
128	def Laws.block_length(r, key, counter, nonce):
129	  T.block_length(r, key, counter, nonce)
130	
131	def Laws.hchacha_length(r, key, nonce):
132	  match key:
133	    case Nil{}: {==}
134	    case b <> rest: {==}