1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/subtle/word.bend as SW
4	import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/logic.bend as Logic
5	
6	def diff_same(+a: List<&2, U32>, +acc: U32,
7	    acc_zero: {U32.is_eq(acc, 0) == True{} : Bool}) ->
8	    {U32.is_eq(AES.bytes_difference.go(a, a, acc), 0) == True{} : Bool}:
9	    match a:
10	        case Nil{}: acc_zero
11	        case x <> xs:
12	            xor_zero = Equal.trans(Bool,
13	                U32.is_eq(U32.xor(x, x), 0), U32.is_eq(x, x), True{},
14	                SW.u32_xor_zero(x, x), SW.u32_refl(x))
15	            both = Logic.and_intro(U32.is_eq(acc, 0),
16	                U32.is_eq(U32.xor(x, x), 0), acc_zero, xor_zero)
17	            next_zero = Equal.trans(Bool,
18	                U32.is_eq(U32.or(acc, U32.xor(x, x)), 0),
19	                Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0)),
20	                True{}, SW.u32_or_zero(acc, U32.xor(x, x)), both)
21	            diff_same(xs, U32.or(acc, U32.xor(x, x)), next_zero)
22	
23	def equal_same(+a: List<&2, U32>) ->
24	    {AES.bytes_equal_full_scan(a, a) == True{} : Bool}:
25	    diff_same(a, 0, {==})
26	
27	def equal_of_equal(+a: List<&2, U32>, +b: List<&2, U32>,
28	    same: {a == b : List<&2, U32>}) ->
29	    {AES.bytes_equal_full_scan(a, b) == True{} : Bool}:
30	    Equal.trans(Bool, AES.bytes_equal_full_scan(a, b),
31	        AES.bytes_equal_full_scan(b, b), True{},
32	        Equal.cong(List<&2, U32>, Bool,
33	            left => AES.bytes_equal_full_scan(left, b), a, b, same),
34	        equal_same(b))
35	
36	def diff_acc_zero(+a: List<&2, U32>, +b: List<&2, U32>, +acc: U32,
37	    zero: {U32.is_eq(AES.bytes_difference.go(a, b, acc), 0) == True{} : Bool}) ->
38	    {U32.is_eq(acc, 0) == True{} : Bool}:
39	    match a b:
40	        case Nil{} Nil{}: zero
41	        case Nil{} y <> ys:
42	            Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
43	                Logic.false_true(zero))
44	        case x <> xs Nil{}:
45	            Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
46	                Logic.false_true(zero))
47	        case x <> xs y <> ys:
48	            acc2 = U32.or(acc, U32.xor(x, y))
49	            step_zero = diff_acc_zero(xs, ys, acc2, zero)
50	            both = Equal.trans(Bool,
51	                Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)),
52	                U32.is_eq(acc2, 0), True{},
53	                Equal.sym(Bool, U32.is_eq(acc2, 0),
54	                    Bool.and(U32.is_eq(acc, 0),
55	                        U32.is_eq(U32.xor(x, y), 0)),
56	                    SW.u32_or_zero(acc, U32.xor(x, y))),
57	                step_zero)
58	            Logic.and_left(U32.is_eq(acc, 0),
59	                U32.is_eq(U32.xor(x, y), 0), both)
60	
61	def diff_list_sound(+a: List<&2, U32>, +b: List<&2, U32>, +acc: U32,
62	    +zero: {U32.is_eq(AES.bytes_difference.go(a, b, acc), 0) == True{} : Bool}) ->
63	    {a == b : List<&2, U32>}:
64	    match a b:
65	        case Nil{} Nil{}: {==}
66	        case Nil{} y <> ys:
67	            Empty.absurd({Nil{} == y <> ys : List<&2, U32>},
68	                Logic.false_true(zero))
69	        case x <> xs Nil{}:
70	            Empty.absurd({x <> xs == Nil{} : List<&2, U32>},
71	                Logic.false_true(zero))
72	        case x <> xs y <> ys:
73	            +acc2 = U32.or(acc, U32.xor(x, y))
74	            acc2_zero = diff_acc_zero(xs, ys, acc2, zero)
75	            both = Equal.trans(Bool,
76	                Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)),
77	                U32.is_eq(acc2, 0), True{},
78	                Equal.sym(Bool, U32.is_eq(acc2, 0),
79	                    Bool.and(U32.is_eq(acc, 0),
80	                        U32.is_eq(U32.xor(x, y), 0)),
81	                    SW.u32_or_zero(acc, U32.xor(x, y))),
82	                acc2_zero)
83	            xor_zero = Logic.and_right(U32.is_eq(acc, 0),
84	                U32.is_eq(U32.xor(x, y), 0), both)
85	            byte_equal = SW.u32_sound(x, y,
86	                Equal.trans(Bool, U32.is_eq(x, y),
87	                    U32.is_eq(U32.xor(x, y), 0), True{},
88	                    Equal.sym(Bool, U32.is_eq(U32.xor(x, y), 0),
89	                        U32.is_eq(x, y), SW.u32_xor_zero(x, y)),
90	                    xor_zero))
91	            tail_equal = diff_list_sound(xs, ys, acc2, zero)
92	            Equal.trans(List<&2, U32>, x <> xs, y <> xs, y <> ys,
93	                Equal.cong(U32, List<&2, U32>, h => h <> xs,
94	                    x, y, byte_equal),
95	                Equal.cong(List<&2, U32>, List<&2, U32>,
96	                    t => y <> t, xs, ys, tail_equal))
97	
98	def equal_sound(+a: List<&2, U32>, +b: List<&2, U32>,
99	    accepted: {AES.bytes_equal_full_scan(a, b) == True{} : Bool}) ->
100	    {a == b : List<&2, U32>}:
101	    diff_list_sound(a, b, 0, accepted)
102	
103	def unequal_from_bool(+a: List<&2, U32>, +b: List<&2, U32>,
104	    compared: Bool,
105	    link: {compared == AES.bytes_equal_full_scan(a, b) : Bool},
106	    unequal: {a != b : List<&2, U32>}) ->
107	    {AES.bytes_equal_full_scan(a, b) == False{} : Bool}:
108	    match compared:
109	        case False{}:
110	            Equal.sym(Bool, False{}, AES.bytes_equal_full_scan(a, b), link)
111	        case True{}:
112	            accepted = Equal.sym(Bool, True{},
113	                AES.bytes_equal_full_scan(a, b), link)
114	            Empty.absurd(
115	                {AES.bytes_equal_full_scan(a, b) == False{} : Bool},
116	                unequal(equal_sound(a, b, accepted)))
117	
118	def unequal_is_false(+a: List<&2, U32>, +b: List<&2, U32>,
119	    unequal: {a != b : List<&2, U32>}) ->
120	    {AES.bytes_equal_full_scan(a, b) == False{} : Bool}:
121	    unequal_from_bool(a, b, AES.bytes_equal_full_scan(a, b), {==}, unequal)