def native_roundtrip

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:18

import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication

18def native_roundtrip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
19  match a:
20    case U32{+w}:
21      %Equal.sym(U32,U32.from_nat(Word.to_nat(32n,w)),U32{WordArithmetic.encode(Word.to_nat(32n,w),32n)},
22        WordArithmetic.native_encoding(Word.to_nat(32n,w))) : {_ == U32{w} : U32}
23      %Equal.sym(Word(32n),WordArithmetic.encode(Word.to_nat(32n,w),32n),w,Multiplication.word_roundtrip(32n,w)) : {U32{_} == U32{w} : U32}
24      {==}