proofs/crypto/secp256k1/blist.bend
bend-collections-laws-crypto@1.0.0.0 · 95 lines · 12 definitions
1
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/u32and.bend as FB
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
10
11
12
13
14
15def head_eq(bs: List<&2, U32>) -> {B.head(bs) == CV.head(bs) : U32}:
16 match bs:
17 case Nil{}:
18 {==}
19 case b <> t:
20 {==}
21
22def tail_after(bs: List<&2, U32>) -> {B.tail(bs) == CV.after(1n, bs) : List<&2, U32>}:
23 match bs:
24 case Nil{}:
25 {==}
26 case b <> t:
27 {==}
28
29def suffix_after(n: Nat, bs: List<&2, U32>) -> {B.suffix(n, bs) == CV.after(n, bs) : List<&2, U32>}:
30 match n bs:
31 case 0n _:
32 {==}
33 case 1n+k Nil{}:
34 {==}
35 case 1n+k b <> t:
36 suffix_after(k, t)
37
38def prefix_first(n: Nat, bs: List<&2, U32>) -> {B.prefix(n, bs) == CV.first(n, bs) : List<&2, U32>}:
39 match n bs:
40 case 0n _:
41 {==}
42 case 1n+k Nil{}:
43 {==}
44 case 1n+ +k +b <> t:
45 Equal.cong(List<&2, U32>, List<&2, U32>, l => b <> l, B.prefix(k, t), CV.first(k, t), prefix_first(k, t))
46
47def after33(bs: List<&2, U32>) -> {CV.after(33n, bs) == CV.after(32n, CV.after(1n, bs)) : List<&2, U32>}:
48 match bs:
49 case Nil{}:
50 {==}
51 case b <> t:
52 {==}
53
54def len_tail(+n: Nat, bs: List<&2, U32>, +h: {B.has_len(1n+n, bs) == True{} : Bool}) -> {B.has_len(n, CV.after(1n, bs)) == True{} : Bool}:
55 match bs:
56 case Nil{}:
57 Empty.absurd({B.has_len(n, CV.after(1n, [])) == True{} : Bool}, Lg.false_true(h))
58 case b <> t:
59 h
60
61def pre_len(a: Nat, +b: Nat, xs: List<&2, U32>, +h: {B.has_len(Nat.add(a, b), xs) == True{} : Bool}) -> {B.has_len(a, CV.first(a, xs)) == True{} : Bool}:
62 match a xs:
63 case 0n _:
64 {==}
65 case 1n+k Nil{}:
66 Empty.absurd({B.has_len(1n+k, CV.first(1n+k, [])) == True{} : Bool}, Lg.false_true(h))
67 case 1n+k x <> t:
68 pre_len(k, b, t, h)
69
70def suf_len(a: Nat, +b: Nat, xs: List<&2, U32>, +h: {B.has_len(Nat.add(a, b), xs) == True{} : Bool}) -> {B.has_len(b, CV.after(a, xs)) == True{} : Bool}:
71 match a xs:
72 case 0n _:
73 h
74 case 1n+k Nil{}:
75 Empty.absurd({B.has_len(b, CV.after(1n+k, [])) == True{} : Bool}, Lg.false_true(h))
76 case 1n+k x <> t:
77 suf_len(k, b, t, h)
78
79def hl_is(+n: Nat, +bs: List<&2, U32>) -> {B.has_len(n, bs) == CV.length_is(n, bs) : Bool}:
80 BY.has_len_v(n, bs)
81
82
83def par01(+pre: U32) -> {Nat.is_lt(U32.to_nat(U32.and(pre, 1)), 2n) == True{} : Bool}:
84 %Equal.sym(Nat, U32.to_nat(U32.and(pre, 1)), C.low(1n, U32.to_nat(pre)), FB.andm(pre, 1n, 1, {==})) : {Nat.is_lt(_, 2n) == True{} : Bool}
85 WW.low_lt(1n, U32.to_nat(pre))
86
87def pl32(+rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {B.has_len(32n, B.prefix(32n, rest)) == True{} : Bool}:
88 %Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), prefix_first(32n, rest)) : {B.has_len(32n, _) == True{} : Bool}
89 pre_len(32n, 32n, rest, hl)
90
91def sl32(+rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {B.has_len(32n, B.suffix(32n, rest)) == True{} : Bool}:
92 %Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), suffix_after(32n, rest)) : {B.has_len(32n, _) == True{} : Bool}
93 suf_len(32n, 32n, rest, hl)
94
95