Bridging your code with formal proof via monads

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!

I can add an assertion:

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.