proofs/word_arithmetic.bend source
proofs/word_arithmetic.bend on the hub · documented module
# Modular arithmetic identities used before applying bounded Nat conversion.import Baseimport ./natural_addition.bend as Additionimport ./u32_successor.bend as U32Successorlaw carry: for +n: Nat for +a: Word(n) for +b: Word(n) {Word.adc(n,a,b,False{},True{}) == Word.inc(n,Word.add(n,a,b)) : Word(n)}def carry(n,a,b): match n: case 0n: {==} case 1n+ +p: match a b: case WCon{False{},at} WCon{False{},bt}: {==} case WCon{False{},+at} WCon{True{},+bt}: %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)} {==} case WCon{True{},+at} WCon{False{},+bt}: %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)} {==} case WCon{True{},at} WCon{True{},bt}: {==}law inc_left: for +n: Nat for +a: Word(n) for +b: Word(n) {Word.add(n,Word.inc(n,a),b) == Word.inc(n,Word.add(n,a,b)) : Word(n)}def inc_left(n,a,b): match n: case 0n: {==} case 1n+ +p: match a b: case WCon{False{},at} WCon{False{},bt}: {==} case WCon{False{},+at} WCon{True{},+bt}: %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)} {==} case WCon{True{},+at} WCon{False{},+bt}: %inc_left(p,at,bt) : {WCon{False{},Word.add(p,Word.inc(p,at),bt)} == WCon{False{},_} : Word(1n+p)} {==} case WCon{True{},+at} WCon{True{},+bt}: %Equal.sym(Word(p),Word.adc(p,at,bt,False{},True{}),Word.inc(p,Word.add(p,at,bt)),carry(p,at,bt)) : {WCon{True{},Word.add(p,Word.inc(p, at),bt)} == WCon{True{},_} : Word(1n+p)} %inc_left(p,at,bt) : {WCon{True{},Word.add(p,Word.inc(p,at),bt)} == WCon{True{},_} : Word(1n+p)} {==}def encode(a: Nat,+width: Nat) -> Word(width): match a: case 0n: Word.zero(width) case 1n+p: Word.inc(width,encode(p,width))law encode_add: for +a: Nat for +b: Nat for +width: Nat {Word.add(width,encode(a,width),encode(b,width)) == encode(Nat.add(a,b),width) : Word(width)}def encode_add(a,b,width): match a: case 0n: %Equal.sym(Word(width),Word.add(width,Word.zero(width),encode(b,width)),Word.add(width,encode(b,width),Word.zero(width)), Word.add_comm(width,Word.zero(width),encode(b,width))) : {_ == encode(b,width) : Word(width)} U32Successor.adc_zero(width,encode(b,width)) case 1n+ +p: %Equal.sym(Word(width),Word.add(width,Word.inc(width,encode(p,width)),encode(b,width)),Word.inc(width,Word.add(width,encode(p,width), encode(b,width))),inc_left(width,encode(p,width),encode(b,width))) : {_ == Word.inc(width,encode(Nat.add(p,b),width)) : Word(width)} %encode_add(p,b,width) : {Word.inc(width,Word.add(width,encode(p,width),encode(b,width))) == Word.inc(width,_) : Word(width)} {==}law double_carry: for +n: Nat for +w: Word(n) for +c: Bool {Word.adc(n,w,w,False{},c) == Word.shl.put(n,c,w) : Word(n)}def double_carry(n,w,c): match n: case 0n: {==} case 1n+ +p: match w c: case WCon{False{},+t} False{}: %double_carry(p,t,False{}) : {WCon{False{},Word.adc(p,t,t,False{},False{})} == WCon{False{},_} : Word(1n+p)} {==} case WCon{False{},+t} True{}: %double_carry(p,t,False{}) : {WCon{True{},Word.adc(p,t,t,False{},False{})} == WCon{True{},_} : Word(1n+p)} {==} case WCon{True{},+t} False{}: %double_carry(p,t,True{}) : {WCon{False{},Word.adc(p,t,t,False{},True{})} == WCon{False{},_} : Word(1n+p)} {==} case WCon{True{},+t} True{}: %double_carry(p,t,True{}) : {WCon{True{},Word.adc(p,t,t,False{},True{})} == WCon{True{},_} : Word(1n+p)} {==}def shift_put(+n: Nat,+w: Word(n)) -> {Word.shl(n,w) == Word.shl.put(n,False{},w) : Word(n)}: match n: case 0n: {==} case 1n+p: WCon{b,t} = w {==}def double_word(+n: Nat,+w: Word(n)) -> {Word.add(n,w,w) == Word.shl(n,w) : Word(n)}: %Equal.sym(Word(n),Word.shl(n,w),Word.shl.put(n,False{},w),shift_put(n,w)) : {Word.add(n,w,w) == _ : Word(n)} double_carry(n,w,False{})def encode_double(+a: Nat,+width: Nat) -> {encode(Nat.double(a),width) == Word.shl(width,encode(a,width)) : Word(width)}: %Addition.double(a) : {encode(_,width) == Word.shl(width,encode(a,width)) : Word(width)} %encode_add(a,a,width) : {_ == Word.shl(width,encode(a,width)) : Word(width)} double_word(width,encode(a,width))law native_encoding: for +a: Nat {U32.from_nat(a) == U32{encode(a,32n)} : U32}def native_encoding(a): match a: case 0n: {==} case 1n+ +p: %native_encoding(p) : {U32.inc(U32.from_nat(p)) == U32.inc(_) : U32} {==}def native_add(+a: Nat,+b: Nat) -> {U32.add(U32.from_nat(a),U32.from_nat(b)) == U32.from_nat(Nat.add(a,b)) : U32}: %Equal.sym(U32,U32.from_nat(Nat.add(a,b)),U32{encode(Nat.add(a,b),32n)},native_encoding(Nat.add(a,b))) : {U32.add(U32.from_nat(a), U32.from_nat(b)) == _ : U32} %Equal.sym(U32,U32.from_nat(a),U32{encode(a,32n)},native_encoding(a)) : {U32.add(_,U32.from_nat(b)) == U32{encode(Nat.add(a,b),32n)} : U32} %Equal.sym(U32,U32.from_nat(b),U32{encode(b,32n)},native_encoding(b)) : {U32.add(U32{encode(a,32n)},_) == U32{encode(Nat.add(a,b),32n)} : U32} %encode_add(a,b,32n) : {U32{Word.add(32n,encode(a,32n),encode(b,32n))} == U32{_} : U32} {==}