Branch relaxation with monotonic time travel

main.lhs

Here's a block of code in some imaginary assembly language:

   jmp A
   block1
   jmp A
   block2
   jmp A
   block3
.A ...

If "jmp A" branches more than 127 bytes it's a 3 byte instruction, otherwise 2 bytes.
But the size of the branch instruction depends on the branch displacement which depends
on the instruction size circularly. We want a fixed point of

> {-# LANGUAGE ApplicativeDo #-}

> import Control.Applicative
> import Data.Function

> infixr :<

> assemble7 :: (Bool, Bool, Bool) -> (Bool, Bool, Bool)
> assemble7 (shortJump1, shortJump2, shortJump3) =
>   let jmpSize1 = if shortJump1 then 2 else 3
>       jmpSize2 = if shortJump2 then 2 else 3
>       jmpSize3 = if shortJump3 then 2 else 3

>       shortJump1' = jmpSize1 + blockSize1 + jmpSize2 + blockSize2 + jmpSize3 + blockSize3 < 128
>       shortJump2' = jmpSize2 + blockSize2 + jmpSize3 + blockSize3 < 128
>       shortJump3' = jmpSize3 + blockSize3 < 128

>       blockSize1 = 64
>       blockSize2 = 30
>       blockSize3 = 28
>   in (shortJump1', shortJump2', shortJump3')

Sometimes this might cause non-termination. How can we impose a policy on the programmer to make sure
this never happens?

Note that `shortJump[123]` are effectively forward references. If we use `fix` on `assemble7` then
it basically picks up the values generated on the previous iteration. One way to ensure convergence
is to impose this condition: all forward references are going to go through an operator `box` which
actually computes the minimum (considering `Bool` as an instance of `Ord`) value of its argument seen
on any iteration, starting optimistically with `True`. Because all forward references go through
a monotonic function like this we're guaranteed convergence. There are a few ways of doing this but
I'm going to replace our logical variables with streams:

> data Stream a = a :< Stream a deriving Show

> instance Functor Stream where
>   fmap f (x :< xs) = f x :< fmap f xs

> instance Applicative Stream where
>   pure x = x :< pure x
>   liftA2 f (x :< xs) (y :< ys) = f x y :< liftA2 f xs ys

> assemble longJump =
>   let branchLocation = 0
>       codeLength = 125 + if longJump then 3 else 2
>       destination = branchLocation + codeLength
>   in destination - branchLocation > 127

> streamScanl :: (a -> b -> a) -> a -> Stream b -> Stream a
> streamScanl f a ~(x :< xs) = a :< streamScanl f (f a x) xs

> streamHead (a :< _) = a

> streamTake 0 _ = []
> streamTake n (x :< xs) = x : streamTake (n - 1) xs

Here is `box` doing a delay of 1 and computing the "cumulative" min:

> box :: Stream Bool -> Stream Bool
> box = streamScanl (&&) True

Sorry it's ugly, I couldn't get `ApplicativeDo` to do this. I hope you see that
conceptually it's `assemble7` "lifted" to streams.

> assemble8 :: Stream (Bool, Bool, Bool) -> Stream (Bool, Bool, Bool)
> assemble8 shortJumps =
>   let shortJump1 = (\(a, _, _) -> a) <$> shortJumps
>       shortJump2 = (\(_, b, _) -> b) <$> shortJumps
>       shortJump3 = (\(_, _, c) -> c) <$> shortJumps

>       jmpSize1 = (\s -> if s then 2 else 3) <$> box shortJump1
>       jmpSize2 = (\s -> if s then 2 else 3) <$> box shortJump2
>       jmpSize3 = (\s -> if s then 2 else 3) <$> box shortJump3

The crucial thing to note here is that we'd prefer `shortJump[123]'` to be `True` but we can accept both `False` and
`True` so this code is compatible with `box`:

>       shortJump1' = (\j1 j2 j3 -> j1 + blockSize1 + j2 + blockSize2 + j3 + blockSize3 < 128) <$> jmpSize1 <*> jmpSize2 <*> jmpSize3
>       shortJump2' = (\j2 j3 -> j2 + blockSize2 + j3 + blockSize3 < 128) <$> jmpSize2 <*> jmpSize3
>       shortJump3' = (\j3 -> j3 + blockSize3 < 128) <$> jmpSize3

>       blockSize1 = 64
>       blockSize2 = 30
>       blockSize3 = 30
>   in (\a b c -> (a, b, c)) <$> shortJump1' <*> shortJump2' <*> shortJump3'

Now we walk our stream until we find convergence:

> solve :: (Eq a) => (Stream a -> Stream a) -> a
> solve f = 
>   let findEqual (x :< y :< ys) | x == y = x
>       findEqual (x :< xs) = findEqual xs 
>   in findEqual (fix f)

This example is trivial and converges in one step

> main = do
>   print $ solve assemble8

Anyway, this is a convoluted way of doing all this. But here's my main point: there's a logic lurking here. Consider
code like

f (a, b, c) = 
  let a' = a || b || c
      b' = a || c
      c' = not a && not b
  in  (a', b', c')

A fixed point solves a system of logical equations

a = a ∨ b ∧ c
b = a ∧ c
c = ¬ a ∧ ¬ b

Now introduce boxes. I'm too lazy to lift by hand so here's unlifted pseudocode:

  f (a, b, c) = 
    let a' = box (a || b || c)
        b' = box (a || c)
        c' = box (not a && not b)
    in  (a', b', c')

We're solving equations like:

a = □ (a ∨ b ∧ c)
b = □ (a ∨ c)
c = □ (¬ a ∧ ¬ b)

But what does □ mean in a purely logical context?

Well, I'm pretty sure □ is the modal operator from provability logic (GL).
See https://arxiv.org/abs/1401.4002 for one angle on this.
See my own blog post http://blog.sigfpe.com/2017/07/self-referential-logic-via-self.html for another.
(That post also gives examples that take longer to converge.)
The stream interpretation is (disguised) in Boolos' book on Provability Logic.

So my claim is this: provability logic is the logic of convergent monotonic time
travel à la @ezyang as suggested here: https://twitter.com/ezyang/status/1341946859053608961