~/jendhub

def ws.gshr_hi_v

bend-osdev-word64@0.1.1.0 · proof_shift.bend:447

import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

447# a shift right by n <= k: the low half is the high half shifted by k - n
448def ws.gshr_hi_v(+n: Nat, +k: Nat, +hw: Word(n)) -> {P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)) == Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)) : Nat}:
449  Equal.trans(Nat, P.wv.V(n, Word.zero(n), ws.shr(n, Nat.sub(k, n), hw)), Nat.add(Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), U.U32Nat.dbl(n, 0n)), Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw)), U.U32Nat.dbl(n, v)), Word.to_nat(n, Word.zero(n)), 0n, UL.word_zero_value(n)), ns.d0(n, Word.to_nat(n, ws.shr(n, Nat.sub(k, n), hw))))

Uses (13)

Used by (2)