x) and functions (F)x)
In [1]:
:browse
In [2]:
:type 1+2
:type (+)
:type width
In [3]:
:set base=8
10
In [4]:
:set base=16
:set ascii=on
[0x48, 0x65, 0x6c, 0x6c, 0x6f] : [5][8]
In [5]:
:help
In [6]:
:set
In [7]:
p = True
q = False
In [8]:
xs : [7]Bit
xs = [False, True, False, True, False, False, True]
In [9]:
xs @ 0
In [10]:
xs ! 0
In [11]:
[1 .. 5] # [3, 6, 8]
In [12]:
[0, 1, 2, 3] << 2
In [13]:
[0, 1, 2, 3] <<< 2
In [14]:
ys : [2][4][4]Bit
ys = [[1, 2, 3, 4], [5, 6, 7, 8]]
In [15]:
ys @ 0
In [16]:
ys @@ [0,1]
In [17]:
width ys
In [18]:
[ 2*x + 3 | x <- [1, 2, 3, 4] ] # [15]
In [19]:
x, y, z : [8]
x = 123
y = 0xF4
z = 0b11110100
In [20]:
1 + 1
In [21]:
(1 : [2]) + 1
In [22]:
t = (13, "hello", True)
In [23]:
t.1
In [24]:
type Point3D = { x : [16], y : [16], z : [16] }
p1 = { x = 22, y = 35, z = 18 } : Point3D
In [25]:
p1.x
In [26]:
// Boolean operators defined on bits as well as pointwise on structures
b = True || False
w = 0xFFFF && 1
ws = [0x0000, 0xFFFF] ^ [0x1A1A, 0x0F0F]
p2 = ~p1
In [27]:
(b, w, ws, p2)
In [28]:
if 0xFF < 42 then 0xdead else 0xbeef
In [29]:
isValid x = withinRange && isEven where
withinRange = x > 5 && x < 10
isEven = (x && 1) == 0
In [30]:
XYandXplusY : [8] -> [8] -> ([8], [8])
XYandXplusY x y = (xy, x + y)
where xy = x * y
In [31]:
(\(x, y) -> 2 + x*y) : ([8], [8]) -> [8]
(Exercises 1:44-47)
(2 >= 3) : Bit
[0x02, 0x14, 0x05, 0x30] : [4][8]Bit
(3,5,True) : ([8],[32],Bool)
F : ([16],[16]) -> [16][2, 4, 5, 3] : {a} [4][a]Bit
tail : {a, b} [1 + a]b -> [a]b
In [32]:
nats = [0] # [ y + 1 | y <- nats ]
In [33]:
as = [0x3F, 0xE2, 0x65, 0xCA] # new
new = [ a ^ b ^ c | a <- as
| b <- drop`{1}as
| c <- drop`{3}as ]
In [34]:
take`{2}[2 .. 10]
In [35]:
drop`{2}[2 .. 10]
In [36]:
:type groupBy
In [37]:
:set ascii=off
groupBy`{2}[1 .. 100]
In [38]:
(split [1 .. 100]) : [2]_
In [39]:
zero : [2][2]Point3D
zero is handy for getting a value of all Trues
In [40]:
~zero : Point3D
In [41]:
ROT13 : {n} [n][8] -> [n][8]
ROT13 msg = [ shift x | x <- msg ]
where map = ['A' .. 'Z'] <<< 13
shift c = map @ (c - 'A')
In [42]:
map = ['A' .. 'Z'] <<< 13
In [43]:
:set ascii=on
map @@ [0,1,2,3,4,13]
In [44]:
shift c = map @ (c - 'A')
In [45]:
shift 'C'
In [46]:
('C' - 'A') == 2
In [47]:
map @ 2
In [48]:
[ shift x | x <- "HELLO" ]
ROT13 defined in ROT13.cry (in this repo)Cryptol> :l ROT13.cry
Loading module Cryptol
Loading module Main
Main> :set ascii=on
Main> ROT13("HELLOWORLD")
“URYYBJBEYQ"
Main> ROT13(ROT13("HELLOWORLD"))
"HELLOWORLD"Properties can express:
Bit: good for test vectors
In [49]:
property two_plus_two = 2 + 2 == 4
property ROT13_hello = ROT13("HELLO") == "URYYB"
Bit: good for broader statements
In [50]:
property plus_id_l x = 0 + x == x
property plus_assoc x y z = x + (y + z) == (x + y) + z
In [51]:
:check \(x : [8]) -> x + 1 != x
:check either takes an expression, or checks all properties in the file
In [52]:
:prove \(x : [8]) -> x + 1 != x
:check and :prove give counterexamples
In [53]:
:check \x -> x != 0x7
:prove can be much more effective
In [54]:
haystack x = x != 0xdeadbeef
In [55]:
:check haystack
In [56]:
:prove haystack
In [57]:
property plus_id_l x = 0 + x == x
In [58]:
:prove plus_id_l
In [59]:
:prove plus_id_l : [32] -> Bit
In [60]:
plus_id_l_1 : [1] -> Bit
plus_id_l_8 : [8] -> Bit
plus_id_l_32 : [32] -> Bit
plus_id_l_128 : [128] -> Bit
property plus_id_l_1 x = plus_id_l x
property plus_id_l_8 x = plus_id_l x
property plus_id_l_32 x = plus_id_l x
property plus_id_l_128 x = plus_id_l x
In [61]:
:prove
In [62]:
mmult : {a, b, c, w} (fin a, fin b, fin w)
=> [a][b][w] -> [b][c][w] -> [a][c][w]
mmult xss yss = [ [ sum (col * row) | col <- transpose yss ]
| row <- xss ]
sum : {a,n} (Arith a, fin n) => [n]a -> a
sum xs = sums!0
where sums = [zero] # [ x + y | x <- xs | y <- sums ]
// 3x3 identity matrix
mi = [[1,0,0],
[0,1,0],
[0,0,1]]
:sat to invert a matrix
In [63]:
ma : [3][3][72]
ma = [[4,2,3],
[8,5,2],
[5,8,9]]
In [64]:
:sat \x -> mmult ma x == mi
:prove