IP.cry

// Constraining properties based on String-specific inputs

// In Cryptol, `String n` is just an alias for `[n][8]` (ASCII)
type IPv4String = String 15

// Print four octets as an IPv4-formatted string
printIp : [4][8] -> IPv4String
printIp ip = x # "." # y # "." # z # "." # w
  where
    [x, y, z, w] = [ printByte b | b <- ip ]

printByte : [8] -> String 3
printByte b = [x, y, z]
  where (x, xr) = (b  / 100 + '0', b  % 100)
        (y, yr) = (xr / 10  + '0', xr % 10 )
        z       =  yr       + '0'

// We want to prove something about f, which takes an IP formatted as
// a string. For the sake of demonstration, let's just have it return
// False whenver the dots aren't in the right place.
f : IPv4String -> Bit
f ip = "..." == ip @@ [3, 7, 11]

// Now we state our theorem using four octets as input, printing them
// as a string, and then passing that string to `f`
fIsSafe : [4][8] -> Bit
property fIsSafe ip = f (printIp ip)

// Main> :prove fIsSafe
// Q.E.D.