Symbolic Execution not terminating

[weaversa]

I coded up a spec for A51 (inlined below). :prove hangs on a proof that has no symbolic inputs, only concrete inputs. Something fishy here.

Main> :l A51.cry
Loading module Cryptol
Loading module Main
Main> A51_uplink_correct 
True
Main> :check A51_uplink_correct 
Using exhaustive testing.
passed 1 tests.
QED
Main> :exhaust A51_uplink_correct 
Using exhaustive testing.
passed 1 tests.
QED
Main> :prove A51_uplink_correct
<hangs>

/***********************************************************
  A51 Specification
************************************************************/

A51_stream : [inf] -> [19] -> [22] -> [23] -> [inf]
A51_stream key R1 R2 R3 = R1s ^ R2s ^ R3s
  where
    (R1s, R1f) = lfsrki <| x^^19 + x^^5 + x^^2 + x^^1 + 1 |>  key R1c R1
    (R2s, R2f) = lfsrki <| x^^22 + x^^1 + 1 |>                key R2c R2
    (R3s, R3f) = lfsrki <| x^^23 + x^^15 + x^^2 + x^^1 + 1 |> key R3c R3
    majvs = [ majv (r1!10) (r2!11) (r3!12) | r1 <- R1f | r2 <- R2f | r3 <- R3f ]
    init = (~zero:[86]) # zero
    R1c = [ r1!10 == m | r1 <- R1f | m <- majvs ] || init
    R2c = [ r2!11 == m | r2 <- R2f | m <- majvs ] || init
    R3c = [ r3!12 == m | r3 <- R3f | m <- majvs ] || init

A51 : ([64], [22]) -> [inf][114]
A51(KS, IV) = bursts
  where
    keystream = drop`{187} (A51_stream (KS#IV#zero) 0 0 0)
    bursts = groupBy`{114} keystream

testkey = reverse(join(reverse [0x12, 0x23, 0x45, 0x67, 0x89, 0xab, 0xcd, 0xef]))
testiv = reverse(`0x134:[22])

downlink = take`{114} (join [0x53, 0x4E, 0xAA, 0x58, 0x2F, 0xE8, 0x15, 0x1A, 0xB6, 0xE1, 0x85, 0x5A, 0x72, 0x8C, 0x00])

uplink   = take`{114} (join [0x24, 0xFD, 0x35, 0xA3, 0x5D, 0x5F, 0xB6, 0x52, 0x6D, 0x32, 0xF9, 0x06, 0xDF, 0x1A, 0xC0])

property A51_downlink_correct = (A51(testkey, testiv)@0) == downlink
property A51_uplink_correct = (A51(testkey, testiv)@1) == uplink


/***********************************************************
  Keyed Irregular Stepping Fibonacci Motion Shift Registers
************************************************************/

lfsrki_step : {d} (fin d, d >=1) => [d+1] -> Bit -> Bit -> [d] -> [d]
lfsrki_step poly key cond fill = fill'
 where
   feedback_bit = if(poly@0) then prefix (^) (([key]#fill) && poly)
                             else error "polynomial does not have high-bit set."
   fill' = if cond then [feedback_bit]#(take fill) else fill

lfsrki : {d} (fin d, d >=1) => [d+1] -> [inf] -> [inf] -> [d] -> ([inf], [inf][d])
lfsrki poly keys conds init = (stream, fills)
  where
    lfsrki' = lfsrki_step poly
    fills = [init] # [ lfsrki' k c f | k <- keys | c <- conds | f <- fills]
    stream = [ f!0 | f <- fills ]


/***********************************************************
  Irregular Stepping Fibonacci Motion Shift Registers
************************************************************/

lfsri_step poly cond fill = lfsrki_step poly False cond fill

lfsri poly conds init = lfsrki poly zero conds init


/***********************************************************
  Keyed Regular Stepping Fibonacci Motion Shift Registers
************************************************************/

lfsrk_step poly key fill = lfsrki_step poly key False fill

lfsrk poly keys init = lfsrki poly keys (~zero) init


/***********************************************************
  Regular Stepping Fibonacci Motion Shift Registers
************************************************************/

lfsr_step : {d} (fin d, d >= 1) => [d+1] -> [d] -> [d]
lfsr_step poly fill = lfsrki_step poly False True fill

lfsr_run poly init = lfsrki poly zero (~zero) init

lfsr_stream : {d} (fin d, d >= 1) => [d+1] -> [d] -> [inf]
lfsr_stream poly init = stream where (stream, _) = lfsrki poly zero (~zero) init

lfsr_fills : {d} (fin d, d >= 1) => [d+1] -> [d] -> [inf][d]
lfsr_fills poly init = fills where (_, fills) = lfsrki poly zero (~zero) init


/***********************************************************
  Utility Functions
***********************************************************/

parity xs = ys!0
  where ys = [False] # [y ^ x | x <- xs | y <- ys ]

prefix f xs = ys!0
  where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ]

parity' = prefix (^)

majv a b c = (a && b) || (a && c) || (b && c)

[brianhuffman]

I reduced this down to a minimal example that still hangs:

:prove ((zero : [8]) # (zero:[inf])) @ 0

[weaversa]

That's strange.

:prove ([False] # zero:[inf])@0

works fine, but yeah,

:prove (zero:[1] # zero:[inf])@0

:prove (0:[1] # zero:[inf])@0

and

:prove (0b0 # zero:[inf])@0

All hang.

[brianhuffman]

Fixed in bb3ffde. The problem was a missing case in the symbolic simulator's implementation of #.

[weaversa]

Thank you!