Skip to content

Commit a949f7c

Browse files
glguyglguy
authored
Merge pull request #2628 from GaloisInc/w4-rme
Add w4_unint_rme proof script
2 parents b328560 + ae0cb0c commit a949f7c

File tree

9 files changed

+201
-2
lines changed

9 files changed

+201
-2
lines changed

‎CHANGES.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,9 @@ This release supports [version
9898
configuring the solver result cache's timeout for database lookups and
9999
inserts.
100100

101+
* Adds `w4_unint_rme` proof script for using RME extended with uninterpreted
102+
functions to resolve goals.
103+
101104
# Version 1.4 -- date still TBD
102105

103106
This release supports [version

‎deps/rme‎

‎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

‎saw-central/src/SAWCentral/Builtins.hs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1126,6 +1126,9 @@ w4_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices []
11261126
w4_unint_bitwuzla :: [Text] -> ProofScript ()
11271127
w4_unint_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla
11281128

1129+
w4_unint_rme :: [Text] -> ProofScript ()
1130+
w4_unint_rme = wrapW4Prover RME [] Prover.proveWhat4_rme
1131+
11291132
w4_unint_boolector :: [Text] -> ProofScript ()
11301133
w4_unint_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector
11311134

‎saw-central/src/SAWCentral/Prover/What4.hs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ import What4.ProblemFeatures
3636
import qualified SAWCoreWhat4.What4 as W
3737
import SAWCoreWhat4.FirstOrder
3838
import qualified What4.Expr.Builder as B
39+
import Data.RME.What4 (rmeAdapter)
3940

4041

4142
----------------------------------------------------------------
@@ -128,13 +129,14 @@ proveWhat4_z3,
128129
proveWhat4_bitwuzla, proveWhat4_boolector,
129130
proveWhat4_cvc4, proveWhat4_cvc5,
130131
proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices,
131-
proveWhat4_abc ::
132+
proveWhat4_abc, proveWhat4_rme ::
132133
Bool {- ^ Hash-consing of What4 terms -}->
133134
SATQuery {- ^ The query to be proved -} ->
134135
TopLevel (Maybe CEX, Text)
135136

136137
proveWhat4_z3 = proveWhat4_sym z3Adapter
137138
proveWhat4_bitwuzla = proveWhat4_sym bitwuzlaAdapter
139+
proveWhat4_rme = proveWhat4_sym rmeAdapter
138140
proveWhat4_boolector = proveWhat4_sym boolectorAdapter
139141
proveWhat4_cvc4 = proveWhat4_sym cvc4Adapter
140142
proveWhat4_cvc5 = proveWhat4_sym cvc5Adapter

‎saw-script/src/SAWScript/Interpreter.hs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3917,6 +3917,13 @@ primitives = Map.fromList
39173917
[ "Prove the current goal using What4 (Bitwuzla backend). Leave the"
39183918
, "given list of names as uninterpreted."
39193919
]
3920+
3921+
, prim "w4_unint_rme" "[String] -> ProofScript ()"
3922+
(pureVal w4_unint_rme)
3923+
Current
3924+
[ "Prove the current goal using What4 (RME backend). Leave the"
3925+
, "given list of names as uninterpreted."
3926+
]
39203927

39213928
, prim "w4_unint_z3" "[String] -> ProofScript ()"
39223929
(pureVal w4_unint_z3)

‎saw.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -484,6 +484,7 @@ library saw-central
484484
macaw-x86-symbolic,
485485
parameterized-utils,
486486
rme,
487+
rme-what4,
487488
what4 >= 0.4,
488489
what4-transition-system,
489490
-- apparently no longer used:

0 commit comments

Comments
 (0)