1	import Base
2	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
4	import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
5	import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
6	import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as CoreP
7	import ./camellia.bend as C
8	import ./LAWS.bend as Laws
9	
10	def block_xx(s: M.CmBlock, k: M.CmBlock) -> {s == M.CmBlock.xor(M.CmBlock.xor(s, k), k) : M.CmBlock}:
11	  match s k:
12	    case M.CmBlock{+a0, +a1, +a2, +a3} M.CmBlock{+b0, +b1, +b2, +b3}:
13	      %CoreL.u32_xor_cancel(a0, b0) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{_, U32.xor(U32.xor(a1, b1), b1), U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
14	      %CoreL.u32_xor_cancel(a1, b1) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, _, U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
15	      %CoreL.u32_xor_cancel(a2, b2) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, _, U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
16	      %CoreL.u32_xor_cancel(a3, b3) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, a2, _} : M.CmBlock}
17	      {==}
18	
19	# Camellia: each step of the cipher is undone (FL by FL^-1 and back, the
20	# rounds and whitening by XOR, whatever F is), so the list of steps is
21	
22	def cam_fl_inv(x: L.LcBlock64, k: L.LcBlock64) -> {x == C.cam.flinv(C.cam.fl(x, k), k) : L.LcBlock64}:
23	  match x k:
24	    case L.LcBlock64{+x1, +x2} L.LcBlock64{+k1, +k2}:
25	      %CoreL.u32_xor_cancel(x1, U32.or(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), k2)) : {L.LcBlock64{x1, x2} == L.LcBlock64{_, U32.xor(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), L.lc.rotl(U32.and(_, k1), 1n))} : L.LcBlock64}
26	      %CoreL.u32_xor_cancel(x2, L.lc.rotl(U32.and(x1, k1), 1n)) : {L.LcBlock64{x1, x2} == L.LcBlock64{x1, _} : L.LcBlock64}
27	      {==}
28	
29	def cam_flinv_inv(y: L.LcBlock64, k: L.LcBlock64) -> {y == C.cam.fl(C.cam.flinv(y, k), k) : L.LcBlock64}:
30	  match y k:
31	    case L.LcBlock64{+y1, +y2} L.LcBlock64{+k1, +k2}:
32	      %CoreL.u32_xor_cancel(y2, L.lc.rotl(U32.and(U32.xor(y1, U32.or(y2, k2)), k1), 1n)) : {L.LcBlock64{y1, y2} == L.LcBlock64{U32.xor(U32.xor(y1, U32.or(y2, k2)), U32.or(_, k2)), _} : L.LcBlock64}
33	      %CoreL.u32_xor_cancel(y1, U32.or(y2, k2)) : {L.LcBlock64{y1, y2} == L.LcBlock64{_, y2} : L.LcBlock64}
34	      {==}
35	
36	def cam_white(a: L.LcBlock64, b: L.LcBlock64, +s: M.CmBlock) -> {s == C.cam.white(a, b, C.cam.white(a, b, s)) : M.CmBlock}:
37	  match a b:
38	    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}:
39	      block_xx(s, M.CmBlock{a0, a1, b0, b1})
40	
41	def cam_f1(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF1{t, k}, C.cam.op(C.LcCamF1{t, k}, s)) : M.CmBlock}:
42	  match s:
43	    case M.CmBlock{+s0, +s1, +s2, +s3}:
44	      %CoreL.u32_xor_cancel(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock}
45	      %CoreL.u32_xor_cancel(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock}
46	      {==}
47	
48	def cam_f1d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF1{t, k}, C.cam.unop(C.LcCamF1{t, k}, s)) : M.CmBlock}:
49	  match s:
50	    case M.CmBlock{+s0, +s1, +s2, +s3}:
51	      %CoreL.u32_xor_cancel(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock}
52	      %CoreL.u32_xor_cancel(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock}
53	      {==}
54	
55	def cam_f2(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF2{t, k}, C.cam.op(C.LcCamF2{t, k}, s)) : M.CmBlock}:
56	  match s:
57	    case M.CmBlock{+s0, +s1, +s2, +s3}:
58	      %CoreL.u32_xor_cancel(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock}
59	      %CoreL.u32_xor_cancel(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock}
60	      {==}
61	
62	def cam_f2d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF2{t, k}, C.cam.unop(C.LcCamF2{t, k}, s)) : M.CmBlock}:
63	  match s:
64	    case M.CmBlock{+s0, +s1, +s2, +s3}:
65	      %CoreL.u32_xor_cancel(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock}
66	      %CoreL.u32_xor_cancel(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock}
67	      {==}
68	
69	def cam_fl_step(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamFl{a, b}, C.cam.op(C.LcCamFl{a, b}, s)) : M.CmBlock}:
70	  match a b s:
71	    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}:
72	      %cam_fl_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock}
73	      %cam_flinv_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock}
74	      {==}
75	
76	def cam_fl_step_dual(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamFl{a, b}, C.cam.unop(C.LcCamFl{a, b}, s)) : M.CmBlock}:
77	  match a b s:
78	    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}:
79	      %cam_flinv_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock}
80	      %cam_fl_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock}
81	      {==}
82	
83	def cam_unop_op(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.unop(o, C.cam.op(o, s)) : M.CmBlock}:
84	  match o:
85	    case C.LcCamWhite{a, b}:
86	      cam_white(a, b, s)
87	    case C.LcCamF1{t, k}:
88	      cam_f1(t, k, s)
89	    case C.LcCamF2{t, k}:
90	      cam_f2(t, k, s)
91	    case C.LcCamFl{a, b}:
92	      cam_fl_step(a, b, s)
93	    case C.LcCamSwap{}:
94	      match s:
95	        case M.CmBlock{s0, s1, s2, s3}:
96	          {==}
97	
98	def cam_op_unop(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.op(o, C.cam.unop(o, s)) : M.CmBlock}:
99	  match o:
100	    case C.LcCamWhite{a, b}:
101	      cam_white(a, b, s)
102	    case C.LcCamF1{t, k}:
103	      cam_f1d(t, k, s)
104	    case C.LcCamF2{t, k}:
105	      cam_f2d(t, k, s)
106	    case C.LcCamFl{a, b}:
107	      cam_fl_step_dual(a, b, s)
108	    case C.LcCamSwap{}:
109	      match s:
110	        case M.CmBlock{s0, s1, s2, s3}:
111	          {==}
112	
113	def cam_unrun_run(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.unrun(os, C.cam.run(os, s)) : M.CmBlock}:
114	  match os:
115	    case Nil{}:
116	      {==}
117	    case Con{+o, +t}:
118	      %cam_unrun_run(t, C.cam.op(o, s)) : {s == C.cam.unop(o, _) : M.CmBlock}
119	      cam_unop_op(o, s)
120	
121	def cam_run_unrun(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.run(os, C.cam.unrun(os, s)) : M.CmBlock}:
122	  match os:
123	    case Nil{}:
124	      {==}
125	    case Con{+o, +t}:
126	      %cam_op_unop(o, C.cam.unrun(t, s)) : {s == C.cam.run(t, _) : M.CmBlock}
127	      cam_run_unrun(t, s)
128	
129	def Laws.camellia_round_trip(k, b):
130	  match k:
131	    case C.LcCamelliaKey{ops}:
132	      Equal.sym(M.CmBlock, b, C.cam.unrun(ops, C.cam.run(ops, b)), cam_unrun_run(ops, b))
133	
134	def Laws.camellia_round_trip_dual(k, b):
135	  match k:
136	    case C.LcCamelliaKey{ops}:
137	      Equal.sym(M.CmBlock, b, C.cam.run(ops, C.cam.unrun(ops, b)), cam_run_unrun(ops, b))
138	
139	# BEGIN GENERATED by gen/vectors.py: vectors
140	
141	def Laws.camellia_rfc3713():
142	  {==}
143	
144	def Laws.camellia_bad_key_length():
145	  {==}
146	# END GENERATED: vectors