proofs/crypto/blake/blake3/lists.bend

bend-collections-laws-crypto@1.0.0.0 · 104 lines · 17 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
5
6# List and arithmetic facts used by the tree proof (generic over the element
7# type, on the spec/common list functions).
8
9def cons_cong(-A: Data, +h: A, +xs: List<&2,A>, +ys: List<&2,A>, e: {xs == ys : List<&2,A>}) -> {Con{h,xs} == Con{h,ys} : List<&2,A>}:
10  Equal.cong(List<&2,A>,List<&2,A>,zs => Con{h,zs},xs,ys,e)
11
12def take_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {SC.append(A,SC.take(A,xs,k),SC.drop(A,xs,k)) == xs : List<&2,A>}:
13  match xs k:
14    case Nil{} _: {==}
15    case Con{+h,+t} 0n: {==}
16    case Con{+h,+t} 1n+j: cons_cong(A,h,SC.append(A,SC.take(A,t,j),SC.drop(A,t,j)),t,take_drop(A,t,j))
17
18def length_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {SC.length(A,SC.drop(A,xs,k)) == Nat.sub(SC.length(A,xs),k) : Nat}:
19  match xs k:
20    case Nil{} 0n: {==}
21    case Nil{} 1n+j: {==}
22    case Con{+h,+t} 0n: {==}
23    case Con{+h,+t} 1n+j: length_drop(A,t,j)
24
25def take_all(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(SC.length(A,xs),k) == True{} : Bool}) -> {SC.take(A,xs,k) == xs : List<&2,A>}:
26  match xs k:
27    case Nil{} _: {==}
28    case Con{+a,+t} 0n: Empty.absurd({SC.take(A,Con{a,t},0n) == Con{a,t} : List<&2,A>},L.false_true(h))
29    case Con{+a,+t} 1n+j: cons_cong(A,a,SC.take(A,t,j),t,take_all(A,t,j,h))
30
31def drop_all(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(SC.length(A,xs),k) == True{} : Bool}) -> {SC.drop(A,xs,k) == Nil{} : List<&2,A>}:
32  match xs k:
33    case Nil{} _: {==}
34    case Con{+a,+t} 0n: Empty.absurd({SC.drop(A,Con{a,t},0n) == Nil{} : List<&2,A>},L.false_true(h))
35    case Con{+a,+t} 1n+j: drop_all(A,t,j,h)
36
37def drop_zero(-A: Data, +ys: List<&2,A>) -> {SC.drop(A,ys,0n) == ys : List<&2,A>}:
38  match ys:
39    case Nil{}: {==}
40    case Con{+b,+u}: {==}
41
42def take_zero(-A: Data, +ys: List<&2,A>) -> {SC.take(A,ys,0n) == Nil{} : List<&2,A>}:
43  match ys:
44    case Nil{}: {==}
45    case Con{+b,+u}: {==}
46
47def drop_append_left(-A: Data, +xs: List<&2,A>, +ys: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.drop(A,SC.append(A,xs,ys),k) == SC.append(A,SC.drop(A,xs,k),ys) : List<&2,A>}:
48  match xs k:
49    case Nil{} 0n: drop_zero(A,ys)
50    case Nil{} 1n+j: Empty.absurd({SC.drop(A,ys,1n+j) == ys : List<&2,A>},L.false_true(h))
51    case Con{+a,+t} 0n: {==}
52    case Con{+a,+t} 1n+j: drop_append_left(A,t,ys,j,h)
53
54def take_append_left(-A: Data, +xs: List<&2,A>, +ys: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.take(A,SC.append(A,xs,ys),k) == SC.take(A,xs,k) : List<&2,A>}:
55  match xs k:
56    case Nil{} 0n: take_zero(A,ys)
57    case Nil{} 1n+j: Empty.absurd({SC.take(A,ys,1n+j) == Nil{} : List<&2,A>},L.false_true(h))
58    case Con{+a,+t} 0n: {==}
59    case Con{+a,+t} 1n+j: cons_cong(A,a,SC.take(A,SC.append(A,t,ys),j),SC.take(A,t,j),take_append_left(A,t,ys,j,h))
60
61def length_take(-A: Data, +xs: List<&2,A>, +k: Nat, +h: {Nat.is_le(k,SC.length(A,xs)) == True{} : Bool}) -> {SC.length(A,SC.take(A,xs,k)) == k : Nat}:
62  match xs k:
63    case Nil{} 0n: {==}
64    case Nil{} 1n+j: Empty.absurd({SC.length(A,SC.take(A,Nil{},1n+j)) == 1n+j : Nat},L.false_true(h))
65    case Con{+a,+t} 0n: {==}
66    case Con{+a,+t} 1n+j: N.succ_cong(SC.length(A,SC.take(A,t,j)),j,length_take(A,t,j,h))
67
68def length_snoc(-A: Data, +xs: List<&2,A>, +x: A) -> {SC.length(A,SC.append(A,xs,Con{x,Nil{}})) == 1n+SC.length(A,xs) : Nat}:
69  match xs:
70    case Nil{}: {==}
71    case Con{+a,+t}: N.succ_cong(SC.length(A,SC.append(A,t,Con{x,Nil{}})),1n+SC.length(A,t),length_snoc(A,t,x))
72
73def is_empty(-A: Data, xs: List<&2,A>) -> Bool:
74  match xs:
75    case Nil{}: True{}
76    case Con{a,t}: False{}
77
78def empty_drop(-A: Data, +xs: List<&2,A>, +k: Nat) -> {is_empty(A,SC.drop(A,xs,k)) == Nat.is_le(SC.length(A,xs),k) : Bool}:
79  match xs k:
80    case Nil{} 0n: {==}
81    case Nil{} 1n+j: {==}
82    case Con{+a,+t} 0n: {==}
83    case Con{+a,+t} 1n+j: empty_drop(A,t,j)
84
85def double_add(+p: Nat) -> {Nat.double(p) == Nat.add(p,p) : Nat}:
86  match p:
87    case 0n: {==}
88    case 1n+q:
89      %Equal.sym(Nat,Nat.add(q,1n+q),1n+Nat.add(q,q),N.add_succ(q,q)) : {2n+Nat.double(q) == 1n+_ : Nat}
90      N.succ_cong(1n+Nat.double(q),1n+Nat.add(q,q),N.succ_cong(Nat.double(q),Nat.add(q,q),double_add(q)))
91
92def sub_double(+p: Nat) -> {Nat.sub(Nat.double(p),p) == p : Nat}:
93  %Equal.sym(Nat,Nat.double(p),Nat.add(p,p),double_add(p)) : {Nat.sub(_,p) == p : Nat}
94  N.add_sub_cancel(p,p)
95
96# 2^h is strictly above h - 1, i.e. n < 2^(n+1).
97def lt_pow2(+n: Nat) -> {Nat.is_lt(n,SC.pow2(n)) == True{} : Bool}:
98  match n:
99    case 0n: {==}
100    case 1n+q:
101      N.lt_le_trans(1n+q,1n+SC.pow2(q),Nat.double(SC.pow2(q)),lt_pow2(q),N.double_succ_le(SC.pow2(q),N.pow2_pos(q)))
102
103def lt_pow2_succ(+n: Nat) -> {Nat.is_lt(n,SC.pow2(1n+n)) == True{} : Bool}:
104  N.lt_trans(n,SC.pow2(n),SC.pow2(1n+n),lt_pow2(n),N.pow2_lt_succ(n))