def sb_split

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsrel.bend:69

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

69# sb(a + b, 0) = sb(a, b) ++ sb(b, 0)
70def sb_split(a: Nat, +b: Nat, +k: Nat) -> {sb(Nat.add(a, b), 0n, k) == List.append(&2, Nat, sb(a, b, k), sb(b, 0n, k)) : List<&2, Nat>}:
71  match a:
72    case 0n:
73      {==}
74    case 1n+ +i:
75      %Equal.sym(List<&2, Nat>, sb(Nat.add(i, b), 0n, k), List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)), sb_split(i, b, k)) : {CV.bit(Nat.add(i, b), k) <> _ == CV.bit(Nat.add(b, i), k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) : List<&2, Nat>}
76      %Equal.sym(Nat, Nat.add(i, b), Nat.add(b, i), NA.add_comm(i, b)) : {CV.bit(_, k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) == CV.bit(Nat.add(b, i), k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) : List<&2, Nat>}
77      {==}