← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/acl2s/cgen/top.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/acl2s/cgen/top.lisp
 
1
#|$ACL2s-Preamble$;
 
2
;;Author - Harsh Raju Chamarthi (harshrc)
 
3
(include-book ;; Newline to fool ACL2/cert.pl dependency scanner
 
4
 "../portcullis")
 
5
(begin-book t :ttags :all);$ACL2s-Preamble$|#
 
6
 
 
7
 
 
8
 
 
9
 
 
10
;; EXAMPLES:
 
11
;; See testing-regression.lsp
 
12
 
 
13
;; USAGE:
 
14
;; (include-book "acl2s/cgen/top" :dir :system :ttags :all)
 
15
;; (acl2s-defaults :set testing-enabled t) ;default is :naive
 
16
 
 
17
 
 
18
; The following shows the various configuration parameters that you
 
19
; can customize.
 
20
; The usual format is (acl2s-defaults :get <param>) for getting the
 
21
; current value of the parameter named <param>. The setter is similar
 
22
; you can see examples below, where most useful parameters are set
 
23
; with their default values. Copy and change what you want, these are
 
24
; embedded events, so you can put them in books. To know more about
 
25
; these parameters, simply do :doc <param> at the ACL2 prompt.
 
26
 
 
27
;; (acl2s-defaults :set testing-enabled :naive) ;other values are T,NIL
 
28
;; (acl2s-defaults :set verbosity-level 1) 
 
29
;; (acl2s-defaults :set num-trials 1000)
 
30
;; (acl2s-defaults :set num-counterexamples 3)
 
31
;; (acl2s-defaults :set num-witnesses 3)
 
32
;; (acl2s-defaults :set search-strategy :simple) ;other value is :incremental
 
33
;; (acl2s-defaults :set sampling-method :random) 
 
34
;; (acl2s-defaults :set subgoal-timeout 10) ;0 turns off timeout
 
35
 
 
36
 
 
37
;; Note: The use of ttags is primarily for engineering
 
38
;; purposes. Usually you would include this book while
 
39
;; developing/designing proofs and when you have all QEDs,
 
40
;; simply remove this book.
 
41
 
 
42
 
 
43
(in-package "ACL2S")
 
44
 
 
45
(include-book "acl2s-parameter")
 
46
(include-book "prove-cgen" :ttags :all)
 
47
(include-book "../defdata/top" :ttags :all)
 
48
 
 
49
 
 
50
(defun defdata-testing-enabled-ev (D kwd-alist wrld)
 
51
  (declare (ignore D wrld))
 
52
  `((local (acl2s-defaults :set testing-enabled 
 
53
                           ,(defdata::get1 :testing-enabled kwd-alist)))))
 
54
 
 
55
; Add the above form at the beginning of defdata events 
 
56
(table defdata-defaults-table 
 
57
       :pre-hook-fns 
 
58
       (cons 'defdata-testing-enabled-ev 
 
59
             (defdata::get1 :pre-hook-fns (table-alist 'defdata-defaults-table world))))
 
60
 
 
61
(make-event 
 
62
 (er-progn
 
63
  (assign cgen::event-stack nil)
 
64
  (assign cgen::cgen-state nil)
 
65
  (value '(value-triple :invisible)))
 
66
 :check-expansion t)
 
67
 
 
68
(defttag t)
 
69
(defattach (acl2::initialize-event-user cgen::initialize-event-user-cgen-gv) :skip-checks t)
 
70
(defattach (acl2::finalize-event-user cgen::finalize-event-user-cgen-gv) :skip-checks t)
 
71
(defattach (cgen::print-testing-summary cgen::print-testing-summary-fn) :skip-checks t)
 
72
(defttag nil)
 
73
 
 
74
 
 
75
; For now lets keep the nats not more than 1000 to avoid stack-overflow
 
76
; on non-tail-recursive functions. If you dont like these, comment
 
77
; them out, or write your own custom test enumerators and attach them
 
78
(defdata-attach pos :test-enumerator nth-pos-testing)
 
79
 
 
80
(defdata-attach integer :test-enumerator nth-integer-testing)
 
81
(defdata-attach nat :test-enumerator nth-nat-testing)
 
82
(defdata-attach neg :test-enumerator nth-neg-testing)
 
83
 
 
84
 
 
85
;Note on xdoc: <= or < cannot be used inside defxdoc!!
 
86
 
 
87
(defun test?-fn (form hints override-defaults state)
 
88
; Jan 9th 2013, dont print summary unless there was a counterexample.
 
89
  (declare (xargs :mode :program
 
90
                  :stobjs (state)))
 
91
;        :sig ((any hints keyword-value-listp state) -> (mv erp any state))
 
92
  (b* ((ctx 'test?)
 
93
 
 
94
       (cgen::cgen-state (cgen::make-cgen-state-fn form override-defaults (w state)))       
 
95
;       (?defaults (cget params))
 
96
       ;(testing-enabled (cget testing-enabled))
 
97
       (vl              (cgen::cget verbosity-level))
 
98
       (pts?            (cgen::cget print-cgen-summary))
 
99
       (hints (append '() ;acl2::*bash-skip-forcing-round-hints*
 
100
                      (acl2::add-string-val-pair-to-string-val-alist
 
101
                       "Goal" :do-not (list 'quote '(acl2::generalize acl2::fertilize))
 
102
                       (acl2::add-string-val-pair-to-string-val-alist
 
103
                        "Goal" :do-not-induct T hints))))
 
104
 
 
105
       ((mv res cgen::cgen-state state) (prove/cgen form hints cgen::cgen-state state))
 
106
 
 
107
       ((er &) (cond ((not (cgen::cgen-state-p cgen::cgen-state)) (value nil))
 
108
                     ((and (<= (acl2::access cgen::gcs% (cgen::cget gcs) :cts) 0)
 
109
                           (not pts?))
 
110
;no point in printing a summary if we specifically ask not to if no cts was found.
 
111
                      (value nil))
 
112
                     (t (cgen::print-testing-summary cgen::cgen-state ctx state))))
 
113
 
 
114
       
 
115
       ((mv cts-found? state)   
 
116
        (cond ((eq res :falsifiable) (prog2$
 
117
                                      (cgen::cw? (cgen::normal-output-flag vl)
 
118
                                           "~%Test? found a counterexample.~%")
 
119
                                      (mv T state)))
 
120
              ((eq res t) (prog2$
 
121
                           (cgen::cw? (and pts? (cgen::normal-output-flag vl))
 
122
                                "~|Test? failed (probably due to a hard error).~%")
 
123
                           (mv nil state)))
 
124
;Success means the prover actually proved the conjecture under consideration
 
125
              ((eq res nil) (prog2$
 
126
                             (cgen::cw? (and pts? (cgen::normal-output-flag vl))
 
127
                                  "~%Test? proved the conjecture under consideration~s0. ~
 
128
 Therefore, no counterexamples exist. ~%" (if hints "" " (without induction)"))
 
129
                             (mv NIL state)))
 
130
; either prove failed, or we didnt call prove. Either way if we didnt find a cts
 
131
; then we say the test? succeeded! But dont print if print-cgen-summary is nil.
 
132
              (t (prog2$
 
133
                  (cgen::cw? (and pts? (cgen::normal-output-flag vl))
 
134
                       "~%Test? succeeded. No counterexamples were found.~%")
 
135
                  (mv NIL state)))))
 
136
 
 
137
       )
 
138
      
 
139
    (mv cts-found? '(value-triple :invisible) state )))
 
140
 
 
141
(defmacro test? (form &rest kwd-val-lst)
 
142
  (let* ((vl-entry (assoc-keyword :verbosity-level kwd-val-lst))
 
143
         (vl (and vl-entry (cadr vl-entry)))
 
144
         (debug (and (natp vl) (cgen::debug-flag vl)))
 
145
         (hints-entry (assoc-keyword :hints kwd-val-lst))
 
146
         (hints (and hints-entry (cadr hints-entry))))
 
147
    `(with-output
 
148
      :stack :push
 
149
      ,(if debug :on :off) :all
 
150
      :gag-mode ,(not debug)
 
151
     (make-event
 
152
      (test?-fn ',form ',hints ',kwd-val-lst state)))))
 
153
 
 
154
 
 
155
(include-book "xdoc/top" :dir :system)
 
156
 
 
157
(defxdoc acl2::cgen
 
158
  :parents (acl2::debugging acl2::acl2-sedan)
 
159
  :short "Counterexample Generation a.k.a Disproving for ACL2"
 
160
  :long 
 
161
"
 
162
<h3>Using Cgen</h3>
 
163
<p>
 
164
Cgen is available and enabled in all ACL2 Sedan session modes except <i>Compatible</i>.
 
165
If it is not already available, you can use Cgen simply be submitting the following
 
166
commands:
 
167
@({
 
168
  (include-book \"acl2s/cgen/top\" :dir :system :ttags :all)
 
169
  (acl2s-defaults :set testing-enabled t)
 
170
})
 
171
</p>
 
172
 
 
173
<h3>Introduction</h3> 
 
174
 
 
175
<p> Cgen is a powerful debugging facility that can be used to test/check
 
176
formulas for counterexamples automatically. It is implemented as a set of
 
177
books, tightly coupled with the @(see defdata) framework. Thus for the most
 
178
profitable use of Cgen, one should specify all type-like monadic predicates
 
179
using @('defdata') or at least register such predicates as defdata types using
 
180
@('register-type').  When Cgen is in effect via the @('testing-enabled')
 
181
parameter, every checkpoint subgoal arising in event contexts such as @('thm'),
 
182
@('defthm') and @('verify-guards') is checked (searched) for
 
183
counterexamples. So although you can integrate Cgen seamlessly in your
 
184
interactive proof workflow, we recommend the use of the specially designed
 
185
macro, <i>test?</i>.  </p>
 
186
 
 
187
<h3>To prove use <tt>thm</tt>, to disprove use <tt>test?</tt></h3> 
 
188
 
 
189
<p> One can use @('test?') as a drop-in replacement for @('thm')
 
190
to disprove conjectures.  @('test?') guarantees that
 
191
counterexamples are printed in terms of the top goal's
 
192
variables. See @(see test?) for more details and examples.</p>
 
193
 
 
194
<h3>More Powerful Theorem Proving</h3> 
 
195
 
 
196
<p>
 
197
Cgen also defeats false generalizations. We have seen many
 
198
examples where defthms succeed with @('testing-enabled') because
 
199
Cgen falsified a bad generalization, thereby causing ACL2 to
 
200
@('backtrack') and modify its proof search path.
 
201
</p>
 
202
 
 
203
<h4>Example</h4>
 
204
<p>Examine the proof output to see the backtracking.</p>
 
205
@({
 
206
  (acl2s-defaults :set testing-enabled t) ;try first with nil
 
207
  (defthm no-duplicates-remove
 
208
    (implies (and (true-listp list)
 
209
                  (no-duplicatesp list))
 
210
             (no-duplicatesp (remove x list))))
 
211
})
 
212
 
 
213
 
 
214
<h3>Control Parameters</h3>
 
215
 
 
216
<p> The Cgen library can be configured via a collection of parameters using the
 
217
  @('acl2s-defaults') macro using the <tt>:get</tt> or <tt>:set</tt> keyword
 
218
  arguments. In particular, see @('num-trials'), @('verbosity-level'),
 
219
  @('testing-enabled'). All the control parameters are package-agnostic.  </p>
 
220
 
 
221
<h3> Advanced Notes </h3>
 
222
 
 
223
<p> If you interrupt a @('test?'),@('thm'), or @('defthm'), in a session with
 
224
@('testing-enabled'), using say Ctrl-C or ACL2s's interrupt command, then there
 
225
is a good chance of polluting the transient Cgen global state. This situation
 
226
might also occur if you are using @(see brr). In such cases you can remedy the
 
227
problem, using @(see cgen::flush). Simply submit the command @('(cgen::flush)')
 
228
in the session editor or the ACL2 prompt. </p>
 
229
 
 
230
<p>The API functions/macros for Cgen library reside in the ACL2S package. Use
 
231
list (<tt>*acl2s-exports*</tt>) to import these symbols into your own
 
232
package.</p>
 
233
 
 
234
<h3>More details</h3> 
 
235
 
 
236
<p> To understand more about how testing works, please refer to the following
 
237
<a href=\"http://arxiv.org/abs/1105.4394v2\">paper</a> </p>
 
238
"
 
239
 )
 
240
 
 
241
(defxdoc cgen::flush
 
242
  :parents (acl2::cgen)
 
243
  :short "Flush/Reset the Cgen state globals to sane values."
 
244
  :long "
 
245
  Flush the transient Cgen state globals (<tt>cgen::event-stack</tt>, <tt>cgen::cgen-state</tt>) to <tt>nil</tt>.
 
246
  <code>
 
247
   Usage (at the top-level):
 
248
     (cgen::flush)
 
249
  </code>
 
250
"
 
251
)
 
252
 
 
253
 
 
254
(defxdoc test?
 
255
  :parents (acl2::cgen)
 
256
  :short "Test/Check a conjecture for counterexamples."
 
257
  :long
 
258
"
 
259
<h3>Examples</h3>
 
260
@({
 
261
  (acl2s::test? (equal (reverse (reverse x)) x))
 
262
 
 
263
  (test? (implies (and (posp (car x))
 
264
                       (posp (cdr x)))
 
265
                  (= (cdr x) (len x))))
 
266
    
 
267
  
 
268
  (defun perm (x y)
 
269
    (if (endp x)
 
270
      (endp y)
 
271
      (and (member (car x) y)
 
272
           (perm (cdr x) (remove1 (car x) y)))))
 
273
  
 
274
  (test?
 
275
    (implies (and (consp X)
 
276
                  (member a Y))
 
277
             (equal (perm (remove a X)
 
278
                          (remove a Y))
 
279
                    (perm X Y))))
 
280
})
 
281
 
 
282
Note: test? is in ACL2S package.
 
283
  
 
284
<h4>Usage:</h4>
 
285
@({
 
286
   (test? form 
 
287
          [:hints hints]
 
288
          [acl2s-defaults keyword options]
 
289
   )
 
290
})
 
291
 
 
292
<h3>Introduction</h3> 
 
293
 
 
294
<p> @('test?') is a powerful counterexample generation facility,
 
295
based on random testing, that is intended to be used to increase
 
296
confidence in the truth of a conjecture by providing extensive
 
297
testing.</p>
 
298
 
 
299
<p> @('test?') combines random testing with the power of ACL2 via our data
 
300
definition framework (@(see defdata)). It guarantees that any counterexamples
 
301
generated are truly counterexamples to the original conjecture. A
 
302
counterexample is just a binding that maps the variables in the original
 
303
conjecture to values in the ACL2 universe. In cases where the value of
 
304
variables are irrelevant, we bind the variables to the symbol @('?') : these
 
305
bindings still provide counterexamples, but should raise alarms, since chances
 
306
are that there is a specification error. </p>
 
307
 
 
308
<p> If no counterexample is found, there are three possibilities. First, it is
 
309
possible that the conjecture is false, in which case increasing the amount of
 
310
testing we do may lead to the discovery of a counterexample.  Second, it is
 
311
also possible that ACL2 proves that the conjecture is true, in which case we
 
312
print a message reporting success.  Finally, the conjecture may be true, but
 
313
ACL2 cannot prove it.  For all of these three cases, we consider testing to
 
314
have succeeded, so @('test?') will report success. </p>
 
315
 
 
316
<p>@('test?') is an embedded event and can be used in ACL2 @(see acl2::books). But it
 
317
is recommended to use them only in the design and in the debug phase, since its
 
318
use requires trust-tags.</p>
 
319
 
 
320
<h3> Control Parameters </h3> 
 
321
 
 
322
<p> We can furthur control the behavior of test? using keyword options or
 
323
@('acl2s-defaults'). All the parameters in @('acl2s-defaults') are available as
 
324
keyword options to the @('test?') macro and they override the current defaults.
 
325
The most important parameters to tweak are
 
326
@(see num-trials), @(see verbosity-level), @(see testing-enabled).</p>
 
327
 
 
328
<h3>More Examples</h3>
 
329
@({
 
330
  (defdata small-pos (enum '(1 2 3 4 5 6 7 8 9)))
 
331
  (test? 
 
332
    (implies (and (integerp c1)
 
333
                  (integerp c2)
 
334
                  (integerp c3)
 
335
                  (small-posp x1)
 
336
                  (small-posp x2)
 
337
                  (small-posp x3)
 
338
                  (< x1 x2)
 
339
                  (< x2 x3)
 
340
                  (equal 0 (+ c1 c2 c3))
 
341
                  (equal 0 (+ (* c1 x1) (* c2 x2) (* c3 x3))))
 
342
             (and (= 0 c1) (= 0 c2) (= 0 c3))))
 
343
 
 
344
 
 
345
  (defun square-root1 (i ri)
 
346
    (declare (xargs :mode :program))
 
347
    (if (>= (floor i ri) ri)
 
348
        ri
 
349
        (square-root1 i (floor (+ ri (floor i ri)) 2))))
 
350
  
 
351
  (defun square-root (i)
 
352
    (declare (xargs :mode :program))
 
353
    (square-root1 i (floor i 2)))
 
354
  
 
355
  (defun square (x)
 
356
     (* x x))
 
357
   
 
358
   
 
359
  (test?
 
360
    (implies (natp i)
 
361
             (and (<= (square (square-root i)) i)
 
362
                  (< i (square (1+ (square-root i)))))))
 
363
  
 
364
 
 
365
 
 
366
 
 
367
  (defdata triple (list pos pos pos))
 
368
  
 
369
  (defun trianglep (v)
 
370
    (and (triplep v)
 
371
         (< (third v) (+ (first v) (second v)))
 
372
         (< (first v) (+ (second v) (third v)))
 
373
         (< (second v) (+ (first v) (third v)))))
 
374
  
 
375
  (defun shape (v)
 
376
    (if (trianglep v)
 
377
        (cond ((equal (first v) (second v))
 
378
               (if (equal (second v) (third v))
 
379
                   \"equilateral\"
 
380
                 \"isosceles\"))
 
381
              ((equal (second v) (third v)) \"isosceles\")
 
382
              ((equal (first v) (third v)) \"isosceles\")
 
383
              (t \"scalene\"))
 
384
      \"error\"))
 
385
  
 
386
  (acl2s-defaults :set num-trials 1000000)
 
387
  (acl2s-defaults :set testing-enabled :naive)
 
388
  
 
389
  (test? 
 
390
   (implies (and (triplep x)
 
391
                 (trianglep x)
 
392
                 (> (third x) 256)
 
393
                 (= (third x)
 
394
                    (* (second x) (first x))))
 
395
            (not (equal \"isosceles\" (shape x)))))
 
396
  
 
397
  (acl2s-defaults :set num-trials 1000)
 
398
  
 
399
  (acl2s-defaults :set testing-enabled t)
 
400
  
 
401
  
 
402
  (include-book \"arithmetic/top-with-meta\" :dir :system)
 
403
  
 
404
  (test?
 
405
   (implies (and (triplep x)
 
406
                 (trianglep x)
 
407
                 (> (third x) 256)
 
408
                 (= (third x)
 
409
                    (* (second x) (first x))))
 
410
            (not (equal \"isosceles\" (shape x)))))
 
411
  
 
412
})
 
413
 
 
414
 
 
415
<h3> Advanced Notes </h3>
 
416
 
 
417
<p> If you interrupt a @('test?') using say Ctrl-C, then there is a good chance
 
418
of polluting the transient Cgen global state. In such cases you can remedy the
 
419
problem, using @(see cgen::flush). Simply submit the command @('(cgen::flush)')
 
420
in the session editor or the ACL2 prompt. </p>
 
421
 
 
422
<p> We note that in order to be able to generate counterexamples, we do not
 
423
allow ACL2 to use any of the following processes: induction, generalization,
 
424
and cross-fertilization. We do allow destructor-elimination, though in rare
 
425
cases, user defined elim rules may generalize the conjecture. Such situations
 
426
are recognized.  If you want to enable the above processes, use @('thm')
 
427
instead, but note that counterexamples shown might not be of the top-level
 
428
conjecture.  </p>
 
429
 
 
430
    
 
431
"
 
432
)
 
433
 
 
434
 
 
435
(defxdoc prove/cgen
 
436
  :parents (acl2::cgen)
 
437
  :short "top-level API function for Cgen/testing."
 
438
  :long
 
439
"<h3>Introduction</h3> 
 
440
 
 
441
<p> This is the main API function to test/check a form for counterexamples with
 
442
the full power of prove (and hints), i.e. @('prove/cgen') actually calls
 
443
@('prove') as a subfunction. You can accomplish the same thing using @('thm,
 
444
defthm') with the acl2s defaults parameter @('testing-enabled') set to @('T'),
 
445
but this function gives the user/caller more control: the user is responsible
 
446
to pass @('cgen-state') (use @('make-cgen-state') to construct one), that
 
447
provides the <i>context</i> for cgen/testing; the results and statistics
 
448
summarizing Cgen/testing are collected in cgen-state and this is returned to
 
449
the caller. </p>
 
450
 
 
451
<h3>General Form:</h3>
 
452
@({(prove/cgen form hints cgen-state state) => (mv erp cgen-state state)})
 
453
 
 
454
<p> The @('erp') part of result is @('nil'), if call to @('prove') was
 
455
successful, it is @(':falsifiable') if there is at least one
 
456
counterexample (not necessarily top-level), it is @('t') if there was a error
 
457
in trans-eval call of prove (usually a hard/raw lisp error), it is @(':?')
 
458
otherwise, which points out that we could neither prove nor disprove the
 
459
conjecture under consideration </p>
 
460
 
 
461
<h3>Example</h3> 
 
462
 
 
463
<p> For an example of the use of @('prove/cgen'), you can study the
 
464
implementation of the @('test?') macro itself found in cgen/top.lisp. To see
 
465
the structure of @('cgen-state'), you can study the
 
466
@('print-testing-summary-fn') function which deconstructs it and prints its
 
467
information in a human-readable form. </p>
 
468
"
 
469
)