You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardexpand all lines: website/docs/tutorial/creating-synthesis-problem.md
+65-3
Original file line number
Diff line number
Diff line change
@@ -5,7 +5,7 @@ sidebar_position: 1
5
5
# Solving a Synthesis Problem
6
6
Before we dive into an end-to-end verified lifting application, let's familiarize ourselves with the basic concepts in Metalift with a synthesis problem.
7
7
8
-
Let us synthesize a function $f(x)$ such that for all integer $x$, $f(x) \geq 0$ and $f(x) \geq x$. Formally, we want to solve the following problem: $\exists{f}. \forall x \in \mathbb{N}. f(x) \geq 0 \wedge f(x) \geq x$. The $\forall$ **universal quantifier** is so key to verification that it's in our logo!
8
+
Let us synthesize a function $f(x)$ such that for all integer $x$, $f(x) \geq 0$ and $f(x) \geq x$. Formally, we want to solve the following problem: $\exists{f}. \forall x \in \mathbb{Z}. f(x) \geq 0 \wedge f(x) \geq x$. The $\forall$ **universal quantifier** is so key to verification that it's in our logo!
9
9
10
10
## Define the Verification Conditions
11
11
The first step to encoding this with Metalift is to define the conditions that we want to verify. These conditions can be specified using the __Metalift IR__, which includes a variety of common operations on types like booleans, integers, lists, and sets that Metalift knows the meaning of.
@@ -41,8 +41,70 @@ correct = ir.And(
41
41
)
42
42
```
43
43
44
+
As an early check, we can print out these conditions in the SMT language:
45
+
<!--phmdoctest-share-names-->
46
+
```python
47
+
print(correct.toSMT())
48
+
```
49
+
50
+
```
51
+
(and (>= (f x) 0) (>= (f x) x))
52
+
```
53
+
44
54
## Create a Program Grammar
45
-
TODO
55
+
Next, we will create a program grammar that defines the search space for the function $f(x)$. In this case, we will use a simple grammar that only allows the function to be defined in terms of arithmetic operations over the integer variable $x$. Grammars are defined using the same IR nodes, but with the addition of the `Choose` node that represents multiple IR options.
56
+
57
+
To build up the grammar, which must have a fixed depth and cannot be recursive, we iteratively re-define the `grammar` variable to capture deeper programs.
58
+
59
+
<!--phmdoctest-share-names-->
60
+
```python
61
+
grammar = x
62
+
63
+
for i inrange(2):
64
+
grammar = ir.Choose(
65
+
ir.Add(grammar, grammar),
66
+
ir.Sub(grammar, grammar),
67
+
ir.Mul(grammar, grammar)
68
+
)
69
+
```
70
+
71
+
Once the grammar is defined, we wrap it with a `Synth` node which declares a function to be synthesized:
72
+
73
+
<!--phmdoctest-share-names-->
74
+
```python
75
+
synthF = ir.Synth(
76
+
"f", # function name
77
+
grammar, # body
78
+
x, # arguments
79
+
)
80
+
```
46
81
47
82
## Synthesize!
48
-
TODO
83
+
Now that we have both a program search space and verification conditions defined, we can use the `synthesize` function to synthesize a function that satisfies the verification conditions. `synthesize` takes a variety of parameters to inject utility functions, define variables to verify over, and introduce additional predicates. But we'll just use it for a simple synthesis execution.
84
+
85
+
```python
86
+
from metalift.synthesize_auto import synthesize
87
+
result = synthesize(
88
+
"example", # name of the synthesis problem
89
+
[], # list of utility functions
90
+
[x], # list of variables to verify over
91
+
[synthF], # list of functions to synthesize
92
+
[], # list of predicates
93
+
correct, # verification condition
94
+
[synthF], # type metadata for functions to synthesize, just pass the Synth node otherwise
95
+
unboundedInts=True, # verify against the full range of integers (by default integers are restricted to a fixed number of bits)
96
+
)
97
+
98
+
print(result)
99
+
```
100
+
101
+
If we run this code, Metalift will use the Rosette synthesis engine to generate a function that satisfies the requirements.
102
+
103
+
```
104
+
====== verification
105
+
Verification Output: unsat
106
+
Verified PS and INV Candidates (FnDecl:(Function Int Int) f (Add:Int (Mul:Int x x) (Sub:Int x x)) x)
107
+
[(FnDecl:(Function Int Int) f (Add:Int (Mul:Int x x) (Sub:Int x x)) x)]
108
+
```
109
+
110
+
In this case, we get $f(x) = (x * x) + (x - x) = x * x$ which indeed satisfies the verification conditions!
0 commit comments