Skip to content

Commit ae0cb0c

Browse files
glguyglguy
committed
Add a test-case for w4_unint_rme
1 parent 47f07e0 commit ae0cb0c

File tree

3 files changed

+183
-0
lines changed

3 files changed

+183
-0
lines changed

‎intTests/test_w4_unint_rme/Code.cry‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
module Code where
2+
3+
type constraint ValidRnd rnd = rnd <= 16
4+
5+
Ascon_p : {rnd} (ValidRnd rnd) => State -> State
6+
Ascon_p S = foldl round S (drop`{back=rnd} Const)
7+
8+
round : State -> [64] -> State
9+
round S ci = pL (pS (pC S ci))
10+
11+
type State = [5][64]
12+
13+
pC : State -> [64] -> State
14+
pC [S0, S1, S2, S3, S4] ci = [S0, S1, S2 ^ ci, S3, S4]
15+
16+
Const : [16][64]
17+
Const =
18+
[ 0x000000000000003c
19+
, 0x000000000000002d
20+
, 0x000000000000001e
21+
, 0x000000000000000f
22+
, 0x00000000000000f0
23+
, 0x00000000000000e1
24+
, 0x00000000000000d2
25+
, 0x00000000000000c3
26+
, 0x00000000000000b4
27+
, 0x00000000000000a5
28+
, 0x0000000000000096
29+
, 0x0000000000000087
30+
, 0x0000000000000078
31+
, 0x0000000000000069
32+
, 0x000000000000005a
33+
, 0x000000000000004b
34+
]
35+
36+
pS : State -> State
37+
pS S = transpose (map SBox (transpose S))
38+
39+
SBox : [5] -> [5]
40+
SBox i = SBoxTable@i
41+
42+
SBoxTable : [32][5]
43+
SBoxTable =
44+
map drop
45+
[ 0x04, 0x0b, 0x1f, 0x14, 0x1a, 0x15, 0x09, 0x02
46+
, 0x1b, 0x05, 0x08, 0x12, 0x1d, 0x03, 0x06, 0x1c
47+
, 0x1e, 0x13, 0x07, 0x0e, 0x00, 0x0d, 0x11, 0x18
48+
, 0x10, 0x0c, 0x01, 0x19, 0x16, 0x0a, 0x0f, 0x17
49+
]
50+
51+
pL : State -> State
52+
pL [S0, S1, S2, S3, S4] =
53+
[ sigma S0 19 28
54+
, sigma S1 61 39
55+
, sigma S2 1 6
56+
, sigma S3 10 17
57+
, sigma S4 7 41
58+
]
59+
where
60+
sigma : [64] -> [6] -> [6] -> [64]
61+
sigma x i j = x ^ x>>>i ^ x>>>j

‎intTests/test_w4_unint_rme/prims.saw‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
print "Bitwise operations &&";
2+
prove_print (w4_unint_rme []) {{ (0x0F && 131) == 3 }};
3+
print ".";
4+
prove_print (w4_unint_rme []) {{ (0x0F || 131) == 143 }};
5+
print ".";
6+
prove_print (w4_unint_rme []) {{ (0x0F ^ 0xFF) == 240 }};
7+
print ".";
8+
prove_print (w4_unint_rme []) {{ ~0x0F == 240 }};
9+
10+
11+
print "Arithmetic +";
12+
prove_print (w4_unint_rme []) {{ (12:[8]) + 32 == 44 }};
13+
print ".";
14+
prove_print (w4_unint_rme []) {{ (252:[8]) + 32 == 28 }};
15+
16+
print "Arithmetic -";
17+
prove_print (w4_unint_rme []) {{ (12:[8]) - 3 == 9 }};
18+
print ".";
19+
prove_print (w4_unint_rme []) {{ (12:[8]) - 32 == 236 }};
20+
21+
print "Arithmetic *";
22+
prove_print (w4_unint_rme []) {{ (12:[8]) * 3 == 36 }};
23+
print ".";
24+
prove_print (w4_unint_rme []) {{ (12:[8]) * 200 == 96 }};
25+
26+
print "Arithmetic /";
27+
prove_print (w4_unint_rme []) {{ (12:[4]) / 3 == 4 }};
28+
print ".";
29+
prove_print (w4_unint_rme []) {{ (12:[4]) / -3 == 0 }};
30+
31+
print "Arithmetic %";
32+
prove_print (w4_unint_rme []) {{ (19:[8]) % 3 == 1 }};
33+
print ".";
34+
prove_print (w4_unint_rme []) {{ (-19:[8]) % 3 == 0 }};
35+
36+
print "Arithmetic lg2";
37+
prove_print (w4_unint_rme []) {{ lg2 (8:[8]) == 3 }};
38+
print ".";
39+
prove_print (w4_unint_rme []) {{ lg2 (-8:[8]) == 8 }};
40+
41+
print "Sequences";
42+
43+
prove_print (w4_unint_rme []) {{ (4:[4]) # (4:[4]) == (68:[8]) }};
44+
print ".";
45+
prove_print (w4_unint_rme []) {{ \(x:[2]) (y:[3]) -> take (x # y) == x }};
46+
print ".";
47+
prove_print (w4_unint_rme []) {{ \(x:[2]) (y:[3]) -> drop (x # y) == y }};
48+
print ".";
49+
prove_print (w4_unint_rme []) {{ \(x:[4]) (y:[1]) -> tail (y # x) == x }};
50+
print ".";
51+
prove_print (w4_unint_rme []) {{ join [2:[2],3:[2]] == 11 }};
52+
print ".";
53+
prove_print (w4_unint_rme []) {{ split 0xFFFF == [15, 15, 15, 15] }};
54+
print ".";
55+
prove_print (w4_unint_rme []) {{ \(x:[7]) -> reverse (reverse x) == x }};
56+
57+
print "Sequences @";
58+
59+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]@ 0 == 1 }};
60+
print ".";
61+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]@ 1 == 2 }};
62+
print ".";
63+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]@ (2:[2]) == 3 }};
64+
print ".";
65+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]@ (2:[8]) == 3 }};
66+
print ".";
67+
fails (prove_print (w4_unint_rme []) {{ [1,2,3:[8]]@ 5 == 3 }});
68+
69+
print "Sequences !";
70+
71+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]! 0 == 3 }};
72+
print ".";
73+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]! 1 == 2 }};
74+
print ".";
75+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]! (2:[2]) == 1 }};
76+
print ".";
77+
prove_print (w4_unint_rme []) {{ [1,2,3:[8]]! (2:[8]) == 1 }};
78+
print ".";
79+
fails (prove_print (w4_unint_rme []) {{ [1,2,3:[8]]! 5 == 1 }});
80+
81+
print "Shifting, rotating";
82+
83+
prove_print (w4_unint_rme []) {{ (16:[8]) >> 3 == 2 }};
84+
print ".";
85+
prove_print (w4_unint_rme []) {{ (15:[8]) >> 3 == 1 }};
86+
print ".";
87+
prove_print (w4_unint_rme []) {{ 0xF0 >> 4 == 15 }};
88+
print ".";
89+
prove_print (w4_unint_rme []) {{ 0xF0 >> 8 == 0 }};
90+
91+
prove_print (w4_unint_rme []) {{ (15:[8]) << 3 == 120 }};
92+
print ".";
93+
prove_print (w4_unint_rme []) {{ (15:[8]) << 7 == 128 }};
94+
print ".";
95+
prove_print (w4_unint_rme []) {{ (1:[8]) << 8 == 0 }};
96+
print ".";
97+
prove_print (w4_unint_rme []) {{ (128:[8]) <<< 2 == 2 }};
98+
print ".";
99+
prove_print (w4_unint_rme []) {{ (2:[8]) >>> 2 == 128 }};
100+
print ".";
101+
prove_print (w4_unint_rme []) {{ (4:[8]) >>> 3 == 128 }};
102+
103+
104+
print "Misc";
105+
prove_print (w4_unint_rme []) {{ min (4:[8]) 5 == 4 }};
106+
print ".";
107+
prove_print (w4_unint_rme []) {{ max (4:[8]) 5 == 5 }};
108+
109+
110+
print "Unint";
111+
import "Code.cry";
112+
print ".";
113+
prove_print (w4_unint_rme ["round"])
114+
{{ \x ->
115+
Ascon_p`{16} x
116+
==
117+
foldl (\x y -> round x (zext y)) x
118+
[0x3c,0x2d,0x1e,0x0f,0xf0,0xe1,0xd2,0xc3,0xb4,0xa5,0x96,0x87,0x78,0x69,0x5a,0x4b]
119+
}};
120+
121+
print "Done";

‎intTests/test_w4_unint_rme/test.sh‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
$SAW prims.saw

0 commit comments

Comments
 (0)