Implementations (still in Python for now) at https://gist.github.com/ecree-solarflare/0665d5b46c2d8d08de2377fbd527de8d (I left out division, because it's so weak.)
I still can't prove + and - are correct, but they've passed every test case I've come up with so far. * seems pretty obviously correct as long as the + it uses is. Bitwise ops and shifts are trivial to prove. -Ed
