proofs/crypto/secp256k1/blist.bend source

proofs/crypto/secp256k1/blist.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/blist.src; edit the .srcimport Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../lib/logic.bend as Lgimport ../../math/typed/width.bend as WWimport ./u32and.bend as FBimport ./bytes.bend as BY# Byte lists: src/crypto/secp256k1/bytes.bend's head, tail, prefix, suffix# and has_len are spec/crypto/secp256k1/curve.bend's head, after, first and# length_is.def head_eq(bs: List<&2, U32>) -> {B.head(bs) == CV.head(bs) : U32}:  match bs:    case Nil{}:      {==}    case b <> t:      {==}def tail_after(bs: List<&2, U32>) -> {B.tail(bs) == CV.after(1n, bs) : List<&2, U32>}:  match bs:    case Nil{}:      {==}    case b <> t:      {==}def suffix_after(n: Nat, bs: List<&2, U32>) -> {B.suffix(n, bs) == CV.after(n, bs) : List<&2, U32>}:  match n bs:    case 0n _:      {==}    case 1n+k Nil{}:      {==}    case 1n+k b <> t:      suffix_after(k, t)def prefix_first(n: Nat, bs: List<&2, U32>) -> {B.prefix(n, bs) == CV.first(n, bs) : List<&2, U32>}:  match n bs:    case 0n _:      {==}    case 1n+k Nil{}:      {==}    case 1n+ +k +b <> t:      Equal.cong(List<&2, U32>, List<&2, U32>, l => b <> l, B.prefix(k, t), CV.first(k, t), prefix_first(k, t))def after33(bs: List<&2, U32>) -> {CV.after(33n, bs) == CV.after(32n, CV.after(1n, bs)) : List<&2, U32>}:  match bs:    case Nil{}:      {==}    case b <> t:      {==}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}:  match bs:    case Nil{}:      Empty.absurd({B.has_len(n, CV.after(1n, [])) == True{} : Bool}, Lg.false_true(h))    case b <> t:      hdef 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}:  match a xs:    case 0n _:      {==}    case 1n+k Nil{}:      Empty.absurd({B.has_len(1n+k, CV.first(1n+k, [])) == True{} : Bool}, Lg.false_true(h))    case 1n+k x <> t:      pre_len(k, b, t, h)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}:  match a xs:    case 0n _:      h    case 1n+k Nil{}:      Empty.absurd({B.has_len(b, CV.after(1n+k, [])) == True{} : Bool}, Lg.false_true(h))    case 1n+k x <> t:      suf_len(k, b, t, h)def hl_is(+n: Nat, +bs: List<&2, U32>) -> {B.has_len(n, bs) == CV.length_is(n, bs) : Bool}:  BY.has_len_v(n, bs)# the parity bit of the prefix bytedef par01(+pre: U32) -> {Nat.is_lt(U32.to_nat(U32.and(pre, 1)), 2n) == True{} : Bool}:  %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}  WW.low_lt(1n, U32.to_nat(pre))def pl32(+rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {B.has_len(32n, B.prefix(32n, rest)) == True{} : Bool}:  %Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), prefix_first(32n, rest)) : {B.has_len(32n, _) == True{} : Bool}  pre_len(32n, 32n, rest, hl)def sl32(+rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {B.has_len(32n, B.suffix(32n, rest)) == True{} : Bool}:  %Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), suffix_after(32n, rest)) : {B.has_len(32n, _) == True{} : Bool}  suf_len(32n, 32n, rest, hl)# ---- compressed ----