Solution (source code)

= Solution

In a least-significant-first <bit-serial comparator>, the new pair has higher significance than every pair already processed. Equal new <bits> preserve the earlier result; unequal new <bits> decide the new result regardless of earlier <bits>. Use a <left fold> starting at equality:

``
type Bit = Int
data LEG = Lt | Eq | Gt deriving (Eq, Show)

step :: LEG -> (Bit,Bit) -> LEG
step old (a,b)
  | a < b = Lt
  | a > b = Gt
  | otherwise = old

compare :: [Bit] -> [Bit] -> LEG
compare as bs = foldl step Eq (pairs as bs)
  where
    pairs [] [] = []
    pairs (a:as) [] = (a,0) : pairs as []
    pairs [] (b:bs) = (0,b) : pairs [] bs
    pairs (a:as) (b:bs) = (a,b) : pairs as bs
``

Inputs have the <precondition> that each `Bit` is `0` or `1`. Equal-length inputs are the physical circuit case; `pairs` also gives a defined unsigned meaning to unequal lengths by padding the shorter input with high-order zeros. Ordinary `zip` would silently discard significant unmatched <bits>.

After $k$ pairs the <fold> accumulator compares $A_k=\sum_{i<k}a_i2^i$ and $B_k=\sum_{i<k}b_i2^i$. Equal new <bits> add the same amount. If $a_k\ne b_k$, the new difference has magnitude $2^k$, exceeding the maximum magnitude $2^k-1$ of the earlier difference. This proves the accumulator invariant and gives
$$
\boxed{\operatorname{compare}(as,bs)=\operatorname{foldl}\ \operatorname{step}\ \mathrm{Eq}\ (\operatorname{pairs}(as,bs)).}
$$
For the four pairs in the source, the states are `Lt, Gt, Gt, Lt`, so the final result compares $6<13$ correctly.