I’ve been working through a formal proof of a BTree implementation in small amounts of spare time in Idris, and both getting better at working with proofs and discovering new parallels between the imperative and functional universe. In this case, I’m going to detail how I think about proofs of imperative code in Idris.

Last time I wrote, I had come up with what amounts to a Free monad that could be used to simulate imperative systems, and therefore expose those systems to the mercy of requirements to prove things.

As an aside, one reason I write these is that I’m not confident with math, and pretty lazy, but also afraid of embarrassment. If I post publicly, I often find and fix both bugs and flaws in my reasoning, which helps my game improve.

I investigated whether I could impose limitations via proofs on actual operation of the imperative code, and the result was great:

Given:

`double : () -> CounterOps () double _ = do  ctr <- getCounter ()  addCounter ctr  pure ()  make4 : () -> CounterOps () make4 _ = do  addCounter 1  double ()  double ()  pure ()  tryit : Int -> Int tryit n =  ioSysRun n make4`

I was able to turn some interactive proving into the ugly (due to the use of Int rather than Nat, and my own ineptitude at cleaning up proof obligations yet):

`{- Less interesting proof targets stubbed ... I'm aware that this - particular proof here requires claims that - (a : Int) -> a + 1 > a and (a : Int) -> a * 4 > a - but wasn't focused on it here. -}prim__2x4x : (a : Int) -> ((2 * (2 * a)) = (4 * a)) prim__2x4x a with (intNatCastEq a (cast a))  prim__2x4x a | Yes prf =  rewrite prf in  rewrite sym (prim__addInt2X (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt a))))) in  rewrite sym (prim__addInt4X (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt a))))) in  rewrite sym (prim__addInt2X (prim__addInt (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt a)))) (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt a)))))) in  Refl{- Proof that make4 turns n into (n+1) * 4 -}tryitReturnsNP1X4 : (n : Int) -> tryit n = (4 * (n + 1)) tryitReturnsNP1X4 n with (intNatCastEq n (cast n))  tryitReturnsNP1X4 n | Yes prf =  rewrite prf in  rewrite prim__addInt2X (prim__addInt (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt n)))) 1) in  rewrite sym (prim__2x4x (prim__addInt (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt n)))) 1)) in  rewrite prim__addInt2X (prim__mulInt 2 (prim__addInt (prim__truncBigInt_Int (toIntegerNat (fromIntegerNat (prim__sextInt_BigInt n)))) 1)) in  Refl`

It may seem trivial but there are important implications here. Note that you could do this for any kind of imperative system, regardless of complexity, as long as you can model the interface between the program and that system. It’s kind of mind boggling that I was able to take an imperative program (not really knowing what’s inside it a-priori) and subject its effects on its environment to proof.

This is interesting in itself, but most systems are very complicated. Even in the above, I’ve cheated regarding the Int range since it’s limited but I wanted to verify that I could analyze the semantics of imperative code running in the monad. There is something we can do however with systems we’ve already got and stuff already built into them.

Instead of just an int I’ll make a record that contains an error state:

`public export record CounterSystem where  constructor MkCounterSystem  value : Int  error : Maybe String  public export emptyCounterSystem : (n : Int) -> CounterSystem emptyCounterSystem n = MkCounterSystem n Nothing  public export CounterOps : Type -> Type CounterOps = IotOps CounterSystem`

And I’ll add a way of translating assert in the original to something sensible.

`public export assert : String -> Bool -> CounterOps () assert diag cond =  if cond then   IOP (\sys => sys) (\sys => Pure ())  else   IOP (\sys => set_error (Just diag) sys) (\sys => Pure ())`

Wow! Now the state of our system depends whether the code we’re analyzing passes all assertions!

`double : () -> CounterOps () double _ = do  ctr <- getCounter ()  addCounter ctr  — Assert that we never have an odd value after double  newCtr <- getCounter ()  assert    "Result was odd"   (B.and (intToBits (cast newCtr)) one == cast 0) pure ()`

And state a proof goal:

`noAssertions : (n : Int) -> (error (tryit n) = Nothing) noAssertions n =  ?noAssertionsProof`

It’s an ugly mess but it’s also completely unrolled to start decomposing into proofs. Note that if you see this process seize up at some point and not unroll any more functions or leave things opaque, it’s likely that an intervening function is not total. Since mod is not total, I ran into just that in making this example before switching it for B.and, so beware and pay attention to totality.

`- + Counter.noAssertionsProof [P]  ` — n : Int  — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — — —  Counter.noAssertionsProof :   error     (case        case          case            ifThenElse              (and                (intToBits                  (prim__sextInt_BigInt                    (prim__addInt                      (prim__addInt n 1)                      (prim__addInt n 1))))                (cast 1) == cast 0)                (Delay (IOP (\sys => sys) (\sys3 => Pure ())))                (Delay (IOP (\sys4 =>                           set_error (Just “Result was odd”) sys4)                  (\sys5 => Pure ())))          of            Pure a => f a            IOP op g => IOP op (\sys => g (op sys) >>= f)        of          Pure a => f a          IOP op g => IOP op (\sys => g (op sys) >>= f)      of        Pure a => sys        IOP t g => interp (g (t sys)) (t sys)    ) = Nothing`

So there it is. If you can prove that ((n + 1) + (n + 1)) is not odd, then set_error lies along the other path and we win. Either way, if we’re unable to prove we can’t, then we can be pretty sure that there’s either a way to reach set_error or that we don’t understand the code well enough to be 100% certain there isn’t.

It is usually ok to not be precisely 100% certain of your code in some ways … (lots of real system are like this (most large C++ codebases accumulate unsolved mysteries like a patient with a latent, never fully cured virus and erlang is designed with abnormal termination as flow control) but I’ve come to the desire to move that needle closer to 100% in my old age, and Idris, haskell, elm, purescript and kin are also helping me become more precise and analytical with my code. Each effort of this kind rubs off in small ways on everything I do, so I recommend trying it out even just to discover that math and proofs aren’t as alien as you once thought and to infect your reasoning with the question “which way makes proving this easier” because that will help you test, write assertions, debug and be readable as well.

An old programmer learning new tricks.

## More from art yerkes

An old programmer learning new tricks.

## Build an Analytics Dashboard with Django and Arctype

Get the Medium app