1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/blist.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/curve.bend as CV
5	import ../../../src/crypto/secp256k1/bytes.bend as B
6	import ../../lib/logic.bend as Lg
7	import ../../math/typed/width.bend as WW
8	import ./u32and.bend as FB
9	import ./bytes.bend as BY
10	
11	# Byte lists: src/crypto/secp256k1/bytes.bend's head, tail, prefix, suffix
12	# and has_len are spec/crypto/secp256k1/curve.bend's head, after, first and
13	# length_is.
14	
15	def 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	
22	def 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	
29	def 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	
38	def 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	
47	def 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	
54	def 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	
61	def 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	
70	def 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	
79	def 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	# the parity bit of the prefix byte
83	def 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	
87	def 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	
91	def 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	# ---- compressed ----