def sb_lo

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

101def sb_lo(i: Nat, +d: Nat, +x: Nat, +r: Nat) -> {sb(i, 0n, Nat.add(x, C.shift(Nat.add(i, d), r))) == sb(i, 0n, x) : List<&2, Nat>}:
102  match i:
103    case 0n:
104      {==}
105    case 1n+ +j:
106      %Equal.sym(Nat, C.shift(Nat.add(1n+j, d), r), C.shift(Nat.add(j, 1n+d), r), sh_idx(j, d, r)) : {C.bit(C.high(j, Nat.add(x, _))) <> sb(j, 0n, Nat.add(x, C.shift(Nat.add(1n+j, d), r))) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
107      %Equal.sym(Nat, C.shift(Nat.add(1n+j, d), r), C.shift(Nat.add(j, 1n+d), r), sh_idx(j, d, r)) : {C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))) <> sb(j, 0n, Nat.add(x, _)) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
108      %Equal.sym(List<&2, Nat>, sb(j, 0n, Nat.add(x, C.shift(Nat.add(j, 1n+d), r))), sb(j, 0n, x), sb_lo(j, 1n+d, x, r)) : {C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))) <> _ == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
109      %Equal.sym(Nat, C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))), C.bit(C.high(j, x)), bit_lo(j, d, x, r)) : {_ <> sb(j, 0n, x) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
110      {==}