mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-26 14:20:59 +03:00
lots of running examples
This commit is contained in:
parent
f80d791c97
commit
3eab3eb6cb
13
examples/append.cry
Normal file
13
examples/append.cry
Normal file
@ -0,0 +1,13 @@
|
||||
x : [_][8]
|
||||
x = [1,2,3,4,5,19,12,38,5,3]
|
||||
|
||||
y : [_][8]
|
||||
y = [19,3,27,5,12]
|
||||
|
||||
z = x # y
|
||||
|
||||
m = z @ (0 : [1]) //1
|
||||
w = z @ 2 //3
|
||||
|
||||
t = z @ 10 //19 (0x13)
|
||||
v = z @ 11 //3
|
48
examples/builtin_lifting.cry
Normal file
48
examples/builtin_lifting.cry
Normal file
@ -0,0 +1,48 @@
|
||||
//builtins lift over tuples, seqs, and records
|
||||
|
||||
//this file uses addition to model a builtin
|
||||
//but this should work for any builtin operators
|
||||
|
||||
x = [True,False]
|
||||
y = [False,True]
|
||||
|
||||
//make sure bitvectors are numbers
|
||||
property p1 = x == (2 : [2])
|
||||
|
||||
//same thing written 2 different ways
|
||||
property p2 = x + y == 3
|
||||
property p3 = x + y == [True,True]
|
||||
|
||||
|
||||
xx = [[True,False]]
|
||||
yy = [[False,True]]
|
||||
|
||||
//addition lifts pointwise over sequences
|
||||
property p4 = xx + yy == [3]
|
||||
|
||||
//negation is a unary operator that also lifts over sequences
|
||||
property p5 = ~ xx == yy
|
||||
|
||||
|
||||
xinf = [2 ... ]
|
||||
yinf = [3 ... ]
|
||||
|
||||
//addition lifts pointwise over infinite lists
|
||||
property p6 = (xinf + yinf) @ (0 : [0]) == (1 : [2])
|
||||
|
||||
//negation lifts pointwise over an infinite list
|
||||
property p7 = (~ xinf) @ (0 : [0]) == (1 : [2])
|
||||
|
||||
xrec = { x = 2 : [2], y = 2 : [2] } : {x : [2], y : [2]}
|
||||
|
||||
property p8 = xrec + xrec + xrec == xrec
|
||||
|
||||
//lift over tuples and records at the same time
|
||||
property p9 = (2,2,xrec) + (2,2,xrec) + (2,2,xrec) == (2:[2],2:[2],xrec)
|
||||
|
||||
//lift unary over tuples and lists
|
||||
property p10 = (~ { x = (1,2), y = [3,4,5] }) == {x = (0:[1],1:[2]), y = [4, 3, 2] : [3][3] }
|
||||
|
||||
|
||||
|
||||
|
5
examples/demote.cry
Normal file
5
examples/demote.cry
Normal file
@ -0,0 +1,5 @@
|
||||
x : {a}(fin a) => [a] -> [(a*2)+3]
|
||||
x v = 0 + 1
|
||||
|
||||
y = x (2 : [3])
|
||||
|
27
examples/props.cry
Normal file
27
examples/props.cry
Normal file
@ -0,0 +1,27 @@
|
||||
x = [True, False]
|
||||
y = [False, True]
|
||||
z = x + y
|
||||
|
||||
property p1 = z == 3
|
||||
|
||||
xx = [[True,False]]
|
||||
yy = [[False, True]]
|
||||
zz = xx + yy
|
||||
|
||||
|
||||
|
||||
t : {a} [a*3] -> [a*3][a*3]
|
||||
t d = zero
|
||||
/*
|
||||
|
||||
|
||||
t1 : [8] -> [2][2][2]
|
||||
t1 x = split (split x)
|
||||
|
||||
t2 : [8] -> ([4],[4])
|
||||
t2 x = splitAt x
|
||||
|
||||
t3 : [8] ->[8] -> [16]
|
||||
t3 x y = x # y
|
||||
|
||||
*/
|
10
examples/split.cry
Normal file
10
examples/split.cry
Normal file
@ -0,0 +1,10 @@
|
||||
x = [1,2,3,4] : [_][8]
|
||||
|
||||
y = (split x) : [2][2][8]
|
||||
|
||||
a = (y@0) @ 0
|
||||
b = (y@0) @ 1
|
||||
c = (y@1) @ 0
|
||||
d = (y@1) @ 1
|
||||
|
||||
|
9
examples/splitAt.cry
Normal file
9
examples/splitAt.cry
Normal file
@ -0,0 +1,9 @@
|
||||
x = [1,2,3,4] : [_][8]
|
||||
|
||||
y = (splitAt x) : ([2][8],[2][8])
|
||||
|
||||
a = y.0 @ 0
|
||||
b = y.0 @ 1
|
||||
c = y.1 @ 0
|
||||
d = y.1 @ 1
|
||||
|
12
examples/zero_weird.cry
Normal file
12
examples/zero_weird.cry
Normal file
@ -0,0 +1,12 @@
|
||||
x : {a}() => a -> [16]
|
||||
x v = zero v
|
||||
|
||||
property xprop v = x v == 0
|
||||
|
||||
y : [12] -> [4] -> [17]
|
||||
y a b = zero a b
|
||||
|
||||
property yprop v w = y v w == 0
|
||||
|
||||
t1 = x 13
|
||||
t2 = y 2 3
|
Loading…
Reference in New Issue
Block a user