~/jendhub

def internal_u32_add_wrap

bend-mathlib@0.8.1.0 · u32.bend:621

import bend-mathlib@0.8.1.0/u32.bend as U32
import Base

621def internal_u32_add_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), m) : Nat}:
622  match a b:
623    case U32{+x} U32{+y}:
624      %e : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), _) : Nat}
625      word_add_wrap(32n, x, y)

Uses (10)

Used by (1)