1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ./AES_ZipLengthProof.bend as ZipLengthProof
4	
5	def bool_and_true_right(+a: Bool, +b: Bool,
6	    both: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
7	    match a b:
8	        case False{} False{}:
9	            Empty.absurd({False{} == True{} : Bool},
10	                ZipLengthProof.false_true(both))
11	        case False{} True{}: {==}
12	        case True{} False{}:
13	            Empty.absurd({False{} == True{} : Bool},
14	                ZipLengthProof.false_true(both))
15	        case True{} True{}: {==}
16	
17	def predecessor(n: Nat) -> Nat:
18	    match n:
19	        case 0n: 0n
20	        case 1n+p: p
21	
22	def length_limit_go_same(+a: List<&2, U32>, +b: List<&2, U32>,
23	    +low: U32, +high: U32, +max_low: U32, +max_high: U32,
24	    +within: Bool,
25	    same_length: {List.length(&2, U32, a) ==
26	        List.length(&2, U32, b) : Nat}) ->
27	    {AES.bytes_length_limit.go(List.length(&2, U32, a), a,
28	        low, high, max_low, max_high, within) ==
29	     AES.bytes_length_limit.go(List.length(&2, U32, b), b,
30	        low, high, max_low, max_high, within) : Bool}:
31	    match a b within:
32	        case Nil{} Nil{} _: {==}
33	        case Nil{} y <> ys _:
34	            mismatch = Equal.cong(Nat, Bool,
35	                n => Nat.is_eq(0n, n),
36	                List.length(&2, U32, Nil{}),
37	                List.length(&2, U32, y <> ys), same_length)
38	            Empty.absurd(
39	                {AES.bytes_length_limit.go(0n, Nil{}, low, high,
40	                    max_low, max_high, within) ==
41	                 AES.bytes_length_limit.go(
42	                    List.length(&2, U32, y <> ys), y <> ys,
43	                    low, high, max_low, max_high, within) : Bool},
44	                ZipLengthProof.false_true(Equal.sym(Bool,
45	                    True{}, False{}, mismatch)))
46	        case x <> xs Nil{} _:
47	            mismatch = Equal.cong(Nat, Bool,
48	                n => Nat.is_eq(n, 0n),
49	                List.length(&2, U32, x <> xs),
50	                List.length(&2, U32, Nil{}), same_length)
51	            Empty.absurd(
52	                {AES.bytes_length_limit.go(
53	                    List.length(&2, U32, x <> xs), x <> xs,
54	                    low, high, max_low, max_high, within) ==
55	                 AES.bytes_length_limit.go(0n, Nil{}, low, high,
56	                    max_low, max_high, within) : Bool},
57	                ZipLengthProof.false_true(mismatch))
58	        case x <> xs y <> ys False{}: {==}
59	        case x <> xs y <> ys True{}:
60	            tail_length = Equal.cong(Nat, Nat, predecessor,
61	                List.length(&2, U32, x <> xs),
62	                List.length(&2, U32, y <> ys), same_length)
63	            +next_low = U32.add(low, 1)
64	            +next_high = Bool.pick(U32, U32.is_eq(next_low, 0),
65	                U32.add(high, 1), high)
66	            next_within = AES.length_pair_within(next_low, next_high,
67	                max_low, max_high)
68	            length_limit_go_same(xs, ys, next_low, next_high,
69	                max_low, max_high, next_within, tail_length)
70	
71	def bytes_length_limit_same(+a: List<&2, U32>, +b: List<&2, U32>,
72	    +max_low: U32, +max_high: U32,
73	    same_length: {List.length(&2, U32, a) ==
74	        List.length(&2, U32, b) : Nat}) ->
75	    {AES.bytes_length_limit(a, max_low, max_high) ==
76	     AES.bytes_length_limit(b, max_low, max_high) : Bool}:
77	    length_limit_go_same(a, b, 0, 0, max_low, max_high, True{},
78	        same_length)
79	
80	def plaintext_valid_same_length(+ciphertext: List<&2, U32>,
81	    +plaintext: List<&2, U32>,
82	    ciphertext_bytes_valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
83	    plaintext_is_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
84	    same_length: {List.length(&2, U32, ciphertext) ==
85	        List.length(&2, U32, plaintext) : Nat}) ->
86	    {AES.plaintext_valid(ciphertext) == True{} : Bool}:
87	    length_limit_eq = bytes_length_limit_same(ciphertext, plaintext,
88	        4294967264, 15, same_length)
89	    plaintext_limit = bool_and_true_right(AES.bytes_valid(plaintext),
90	        AES.bytes_length_limit(plaintext, 4294967264, 15),
91	        plaintext_is_valid)
92	    ciphertext_limit = Equal.trans(Bool,
93	        AES.bytes_length_limit(ciphertext, 4294967264, 15),
94	        AES.bytes_length_limit(plaintext, 4294967264, 15), True{},
95	        length_limit_eq, plaintext_limit)
96	    Equal.trans(Bool, AES.plaintext_valid(ciphertext),
97	        Bool.and(True{}, True{}), True{},
98	        Equal.trans(Bool,
99	            Bool.and(AES.bytes_valid(ciphertext),
100	                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
101	            Bool.and(True{},
102	                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
103	            Bool.and(True{}, True{}),
104	            Equal.cong(Bool, Bool, valid => Bool.and(valid,
105	                AES.bytes_length_limit(ciphertext, 4294967264, 15)),
106	                AES.bytes_valid(ciphertext), True{}, ciphertext_bytes_valid),
107	            Equal.cong(Bool, Bool, within => Bool.and(True{}, within),
108	                AES.bytes_length_limit(ciphertext, 4294967264, 15), True{},
109	                ciphertext_limit)),
110	        {==})