1 import Base 2 import ../../../spec/crypto/curve25519/field.bend as FS 3 import ../../../spec/crypto/curve25519/x25519.bend as SX 4 import ../../../spec/crypto/ed25519.bend as SE 5 import ../../../src/crypto/curve25519/field.bend as F 6 import ../../../src/crypto/curve25519/x25519.bend as X 7 import ../../../src/crypto/ed25519/point.bend as PT 8 import ../../lib/nat.bend as N 9 import ../../lib/logic.bend as L 10 import ../../lib/word.bend as WD 11 import ../curve25519/limbs.bend as LM 12 import ../curve25519/fieldops.bend as FO 13 import ../curve25519/mulw.bend as MW 14 import ../curve25519/cong.bend as G 15 import ../curve25519/rel.bend as RL 16 import ../curve25519/xbits.bend as XB 17 18 # edwards25519 point operations of src/crypto/ed25519/point.bend against 19 # spec/crypto/ed25519.bend: the point relation Rp (each coordinate RL.R), 20 # kept by addition, doubling, selection and double-and-add scalar 21 # multiplication, for every point. 22 23 def v(+x: U32) -> Nat: 24 U32.to_nat(x) 25 26 def DP(-A: Data, -B: Data) -> Data: 27 Sigma<&2, &2, A, _ => B> 28 29 def fst(-A: Data, -B: Data, +p: DP(A, B)) -> A: 30 match p: 31 case (a, b): 32 a 33 34 def snd(-A: Data, -B: Data, +p: DP(A, B)) -> B: 35 match p: 36 case (a, b): 37 b 38 39 def Rp(+pp: Nat, +p: PT.Pt, +q: SE.EPt) -> Data: 40 match p q: 41 case PT.Pt{x, y, z, t} SE.EPt{a, b, c, d}: 42 DP(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)))) 43 44 def mk(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b), +rz: RL.R(pp, z, c), +rt: RL.R(pp, t, d)) -> Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d}): 45 (rx, (ry, (rz, rt))) 46 47 def rX(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, x, a): 48 fst(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h) 49 50 def rY(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, y, b): 51 fst(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h)) 52 53 def rZ(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, z, c): 54 fst(RL.R(pp, z, c), RL.R(pp, t, d), snd(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h))) 55 56 def rT(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, t, d): 57 snd(RL.R(pp, z, c), RL.R(pp, t, d), snd(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h))) 58 59 # relation-level field operations 60 def o(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: RL.R(pp, x, a)) -> {LM.okb(32n, x, 255n) == True{} : Bool}: 61 RL.r_o(pp, x, a, r) 62 63 def c(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: RL.R(pp, x, a)) -> G.ceq(pp, FS.value(x), a): 64 RL.r_c(pp, x, a, r) 65 66 def radd(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.add(x, y), FS.fadd(1n+pp, a, b)): 67 (FO.add_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_add(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry))) 68 69 def rsub(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.sub(x, y), FS.fsub(1n+pp, a, b)): 70 (FO.sub_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_sub(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry))) 71 72 def rmul(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.mul(x, y), FS.fmul(1n+pp, a, b)): 73 (MW.mul_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_mul(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry))) 74 75 def rsq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a)) -> RL.R(pp, F.sq(x), FS.fmul(1n+pp, a, a)): 76 rmul(one, h1, pp, hP, x, x, a, a, rx, rx) 77 78 # ---- addition ---- 79 80 def add_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> Rp(pp, PT.add(cs, p, q), SE.add(1n+pp, D, sp, sq)): 81 match p q sp sq: 82 case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}: 83 +P = {1n+pp : Nat} 84 +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 85 +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 86 +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 87 +rt1 = rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 88 +rx2 = rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) 89 +ry2 = rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) 90 +rz2 = rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) 91 +rt2 = rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) 92 +ra = rmul(one, h1, pp, hP, F.sub(y1, x1), F.sub(y2, x2), FS.fsub(P, b1, a1), FS.fsub(P, b2, a2), rsub(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), rsub(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2)) 93 +rb = rmul(one, h1, pp, hP, F.add(y1, x1), F.add(y2, x2), FS.fadd(P, b1, a1), FS.fadd(P, b2, a2), radd(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), radd(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2)) 94 +rc = rmul(one, h1, pp, hP, F.mul(t1, PT.cs_d2(cs)), t2, FS.fmul(P, d1, FS.fadd(P, D, D)), d2, rmul(one, h1, pp, hP, t1, PT.cs_d2(cs), d1, FS.fadd(P, D, D), rt1, rd2), rt2) 95 +rdd = rmul(one, h1, pp, hP, F.add(z1, z1), z2, FS.fadd(P, c1, c1), c2, radd(one, h1, pp, hP, z1, z1, c1, c1, rz1, rz1), rz2) 96 +ea = F.mul(F.sub(y1, x1), F.sub(y2, x2)) 97 +EA = FS.fmul(P, FS.fsub(P, b1, a1), FS.fsub(P, b2, a2)) 98 +eb = F.mul(F.add(y1, x1), F.add(y2, x2)) 99 +EB = FS.fmul(P, FS.fadd(P, b1, a1), FS.fadd(P, b2, a2)) 100 +ec = F.mul(F.mul(t1, PT.cs_d2(cs)), t2) 101 +EC = FS.fmul(P, FS.fmul(P, d1, FS.fadd(P, D, D)), d2) 102 +ed = F.mul(F.add(z1, z1), z2) 103 +ED = FS.fmul(P, FS.fadd(P, c1, c1), c2) 104 +re = rsub(one, h1, pp, hP, eb, ea, EB, EA, rb, ra) 105 +rf = rsub(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc) 106 +rg = radd(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc) 107 +rh = radd(one, h1, pp, hP, eb, ea, EB, EA, rb, ra) 108 +e = F.sub(eb, ea) 109 +f = F.sub(ed, ec) 110 +g = F.add(ed, ec) 111 +h = F.add(eb, ea) 112 +EE = FS.fsub(P, EB, EA) 113 +FF = FS.fsub(P, ED, EC) 114 +GG = FS.fadd(P, ED, EC) 115 +HH = FS.fadd(P, EB, EA) 116 mk(pp, F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h), FS.fmul(P, EE, FF), FS.fmul(P, GG, HH), FS.fmul(P, FF, GG), FS.fmul(P, EE, HH), rmul(one, h1, pp, hP, e, f, EE, FF, re, rf), rmul(one, h1, pp, hP, g, h, GG, HH, rg, rh), rmul(one, h1, pp, hP, f, g, FF, GG, rf, rg), rmul(one, h1, pp, hP, e, h, EE, HH, re, rh)) 117 118 # ---- doubling ---- 119 120 def double_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +sp: SE.EPt, +hp: Rp(pp, p, sp)) -> Rp(pp, PT.double(p), SE.double(1n+pp, sp)): 121 match p sp: 122 case PT.Pt{+x1, +y1, +z1, +t1} SE.EPt{+a1, +b1, +c1, +d1}: 123 +P = {1n+pp : Nat} 124 +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 125 +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 126 +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) 127 +a = F.sq(x1) 128 +A = FS.fmul(P, a1, a1) 129 +ra = rsq(one, h1, pp, hP, x1, a1, rx1) 130 +b = F.sq(y1) 131 +B = FS.fmul(P, b1, b1) 132 +rb = rsq(one, h1, pp, hP, y1, b1, ry1) 133 +zz = F.sq(z1) 134 +ZZ = FS.fmul(P, c1, c1) 135 +rzz = rsq(one, h1, pp, hP, z1, c1, rz1) 136 +cc = F.add(zz, zz) 137 +CC = FS.fadd(P, ZZ, ZZ) 138 +rcc = radd(one, h1, pp, hP, zz, zz, ZZ, ZZ, rzz, rzz) 139 +h = F.add(a, b) 140 +HH = FS.fadd(P, A, B) 141 +rh = radd(one, h1, pp, hP, a, b, A, B, ra, rb) 142 +xy = F.add(x1, y1) 143 +XY = FS.fadd(P, a1, b1) 144 +rxy = radd(one, h1, pp, hP, x1, y1, a1, b1, rx1, ry1) 145 +e = F.sub(h, F.sq(xy)) 146 +EE = FS.fsub(P, HH, FS.fmul(P, XY, XY)) 147 +re = rsub(one, h1, pp, hP, h, F.sq(xy), HH, FS.fmul(P, XY, XY), rh, rsq(one, h1, pp, hP, xy, XY, rxy)) 148 +g = F.sub(a, b) 149 +GG = FS.fsub(P, A, B) 150 +rg = rsub(one, h1, pp, hP, a, b, A, B, ra, rb) 151 +f = F.add(cc, g) 152 +FF = FS.fadd(P, CC, GG) 153 +rf = radd(one, h1, pp, hP, cc, g, CC, GG, rcc, rg) 154 mk(pp, F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h), FS.fmul(P, EE, FF), FS.fmul(P, GG, HH), FS.fmul(P, FF, GG), FS.fmul(P, EE, HH), rmul(one, h1, pp, hP, e, f, EE, FF, re, rf), rmul(one, h1, pp, hP, g, h, GG, HH, rg, rh), rmul(one, h1, pp, hP, f, g, FF, GG, rf, rg), rmul(one, h1, pp, hP, e, h, EE, HH, re, rh)) 155 156 # ---- selection ---- 157 158 def sel_eq0(+one: Nat, +h1: {one == 1n : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +pp: Nat, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> {PT.select(0, p, q) == p : PT.Pt}: 159 match p q sp sq: 160 case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}: 161 +ox1 = o(pp, x1, a1, rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 162 +oy1 = o(pp, y1, b1, rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 163 +oz1 = o(pp, z1, c1, rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 164 +ot1 = o(pp, t1, d1, rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 165 +ox2 = o(pp, x2, a2, rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 166 +oy2 = o(pp, y2, b2, rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 167 +oz2 = o(pp, z2, c2, rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 168 +ot2 = o(pp, t2, d2, rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 169 %Equal.sym(List<&2, U32>, F.select(0, x1, x2), x1, FO.select0(one, h1, 32n, x1, x2, ox1, ox2)) : {PT.Pt{_, F.select(0, y1, y2), F.select(0, z1, z2), F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt} 170 %Equal.sym(List<&2, U32>, F.select(0, y1, y2), y1, FO.select0(one, h1, 32n, y1, y2, oy1, oy2)) : {PT.Pt{x1, _, F.select(0, z1, z2), F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt} 171 %Equal.sym(List<&2, U32>, F.select(0, z1, z2), z1, FO.select0(one, h1, 32n, z1, z2, oz1, oz2)) : {PT.Pt{x1, y1, _, F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt} 172 %Equal.sym(List<&2, U32>, F.select(0, t1, t2), t1, FO.select0(one, h1, 32n, t1, t2, ot1, ot2)) : {PT.Pt{x1, y1, z1, _} == PT.Pt{x1, y1, z1, t1} : PT.Pt} 173 {==} 174 175 def sel_eq1(+one: Nat, +h1: {one == 1n : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +pp: Nat, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> {PT.select(1, p, q) == q : PT.Pt}: 176 match p q sp sq: 177 case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}: 178 +ox1 = o(pp, x1, a1, rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 179 +oy1 = o(pp, y1, b1, rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 180 +oz1 = o(pp, z1, c1, rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 181 +ot1 = o(pp, t1, d1, rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)) 182 +ox2 = o(pp, x2, a2, rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 183 +oy2 = o(pp, y2, b2, rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 184 +oz2 = o(pp, z2, c2, rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 185 +ot2 = o(pp, t2, d2, rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)) 186 %Equal.sym(List<&2, U32>, F.select(1, x1, x2), x2, FO.select1(one, h1, 32n, x1, x2, ox1, ox2)) : {PT.Pt{_, F.select(1, y1, y2), F.select(1, z1, z2), F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt} 187 %Equal.sym(List<&2, U32>, F.select(1, y1, y2), y2, FO.select1(one, h1, 32n, y1, y2, oy1, oy2)) : {PT.Pt{x2, _, F.select(1, z1, z2), F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt} 188 %Equal.sym(List<&2, U32>, F.select(1, z1, z2), z2, FO.select1(one, h1, 32n, z1, z2, oz1, oz2)) : {PT.Pt{x2, y2, _, F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt} 189 %Equal.sym(List<&2, U32>, F.select(1, t1, t2), t2, FO.select1(one, h1, 32n, t1, t2, ot1, ot2)) : {PT.Pt{x2, y2, z2, _} == PT.Pt{x2, y2, z2, t2} : PT.Pt} 190 {==} 191 192 def sel_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +s: U32, +b: Nat, +hs: {v(s) == b : Nat}, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> Rp(pp, PT.select(s, p, q), SE.pick(b, sp, sq)): 193 match b: 194 case 0n: 195 %Equal.sym(U32, s, 0, XB.u0(s, hs)) : Rp(pp, PT.select(_, p, q), sp) 196 %Equal.sym(PT.Pt, PT.select(0, p, q), p, sel_eq0(one, h1, p, q, sp, sq, pp, hp, hq)) : Rp(pp, _, sp) 197 hp 198 case 1n: 199 %Equal.sym(U32, s, 1, XB.u1(s, hs)) : Rp(pp, PT.select(_, p, q), sq) 200 %Equal.sym(PT.Pt, PT.select(1, p, q), q, sel_eq1(one, h1, p, q, sp, sq, pp, hp, hq)) : Rp(pp, _, sq) 201 hq 202 case 2n+z: 203 Empty.absurd(Rp(pp, PT.select(s, p, q), sq), L.false_true(hb)) 204 205 # ---- double-and-add ---- 206 207 def smul_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +n: Nat, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +bs: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +p: PT.Pt, +sp: SE.EPt, +hp: Rp(pp, p, sp), +q: PT.Pt, +sq: SE.EPt, +hq: Rp(pp, q, sq)) -> Rp(pp, PT.smul(n, cs, bs, p, q), SE.smul(1n+pp, D, n, FS.value(bs), sp, sq)): 208 match n: 209 case 0n: 210 hq 211 case 1n+ +t: 212 +q2 = PT.double(q) 213 +sq2 = SE.double(1n+pp, sq) 214 +hq2 = double_rel(one, h1, pp, hP, q, sq, hq) 215 +r = PT.add(cs, q2, p) 216 +sr = SE.add(1n+pp, D, sq2, sp) 217 +hr = add_rel(one, h1, pp, hP, cs, D, rd2, q2, p, sq2, sp, hq2, hp) 218 +hs = sel_rel(one, h1, pp, X.kbit(bs, t), SX.kbit(FS.value(bs), t), XB.kbit_val(bs, t, hbs), XB.kbit_le(bs, t, hbs), q2, r, sq2, sr, hq2, hr) 219 smul_rel(one, h1, pp, hP, t, cs, D, rd2, bs, hbs, p, sp, hp, PT.select(X.kbit(bs, t), q2, r), SE.pick(SX.kbit(FS.value(bs), t), sq2, sr), hs)