Implement instruction execution
[jade-mouse] / synthesis-base.rkt
1 #lang rosette/safe
2
3 (require rosette/lib/angelic
4 rosette/lib/match)
5
6 ; Most of the setup taken from Whitequark's synthesis demo
7 ; https://gist.github.com/whitequark/1f7cc43c1cc2b179a1d4a668f0089804
8
9 (provide ??prog verify-prog synthesize-prog optimize-prog)
10
11 (define (??prog ??insn fuel)
12 (if (= fuel 0) null
13 (cons (??insn) (??prog ??insn (- fuel 1)))))
14
15 ; program verifier
16 (define (verify-prog make-state run-insn prog asserts)
17 (define S (make-state))
18 (define S* (make-state))
19 (define solution
20 (verify
21 #:guarantee
22 (begin
23 (for-each (curry run-insn S*) prog)
24 (asserts S S*))))
25 (if (unsat? solution) #t
26 (begin
27 (displayln (evaluate S solution))
28 (displayln (evaluate S* solution))
29 solution)))
30
31 ; program synthesizer
32 (define (synthesize-prog make-state run-insn sketch asserts)
33 (define S (make-state))
34 (define S* (make-state))
35 (define solution
36 (synthesize
37 #:forall S
38 #:guarantee
39 (begin
40 (for-each (curry run-insn S*) sketch)
41 (asserts S S*))))
42 (if (unsat? solution) #f
43 (begin
44 (evaluate sketch solution))))
45
46 (define (optimize-prog max-fuel make-state run-insn sketch-gen asserts)
47 (define (worker fuel)
48 (printf "fuel ~s~n" fuel)
49 (or (synthesize-prog make-state run-insn (sketch-gen fuel) asserts)
50 (if (>= fuel max-fuel) #f
51 (worker (+ fuel 1)))))
52 (worker 0))