← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/russinoff-kaufmann/supporting-materials/main.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/workshops/2000/russinoff-kaufmann/supporting-materials/main.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
; Need to define the "*" package, before (certify-book "main" 7):
 
4
; (ld "packages.lisp")
 
5
 
 
6
; Include the "*" model.
 
7
(include-book "constants")
 
8
 
 
9
; Include input-assumptions.
 
10
(include-book "inputs")
 
11
 
 
12
; Here is the desired relation between input and output, given appropriate
 
13
; constraints on other signals.
 
14
(defun result (in out)
 
15
  (equal out
 
16
         (logand (logand (bitn in 0) (bitn in 1))
 
17
                 (logand (bitn in 2) (bitn in 3)))))
 
18
 
 
19
; We sometimes assume the following relationships between inputs in our two
 
20
; models.  Eventually we will functionally instantiate the "*" functions with
 
21
; the "ACL2" functions, removing any such assumption from our main result.
 
22
(defmacro bindings (n)
 
23
  `(and (equal (*::longop) (longop ,n))
 
24
        (equal (*::in) (in ,n))))
 
25
 
 
26
; The following definition of spec states what must be true of the inputs in
 
27
; the "*" model in order to prove the desired result for the "*" model
 
28
; (spec-lemma-2 below).  It should be straightforward that spec holds of the
 
29
; "ACL2" model inputs (spec-lemma-1).
 
30
 
 
31
(defun spec (in longop)
 
32
  (declare (ignore in))
 
33
  (equal longop 1))
 
34
 
 
35
; This should be easy.
 
36
(defthm spec-lemma-1
 
37
  (implies (input-assumptions n)
 
38
           (spec (in n) (longop n))))
 
39
 
 
40
; Here is where all the effort goes, in general.  For our toy model the proof
 
41
; is very easy simply by enabling all the "*" functions.
 
42
(defthm spec-lemma-2
 
43
  (implies (spec (*::in) (*::longop))
 
44
           (result (*::in) (*::out)))
 
45
  :hints (("Goal" :in-theory
 
46
           (enable *::S01 *::S01_MUXED *::S01_MUXED_FLOPPED
 
47
                   *::S23 *::S23_FLOPPED *::S0123
 
48
                   *::LONGOP_FLOPPED *::OUT))))
 
49
 
 
50
; The rest of our development requires only the above facts about the functions
 
51
; we now disable, together with pipeline-lemma below.
 
52
(in-theory (disable result input-assumptions spec))
 
53
 
 
54
(encapsulate
 
55
 ()
 
56
 (local (include-book "pipe"))
 
57
 (defthm pipeline-lemma
 
58
   (implies (and (input-assumptions n)
 
59
                 (bindings n))
 
60
            (equal (out (+ 2 n)) (*::out)))
 
61
   :hints (("Goal"
 
62
            :use ((:definition input-assumptions*))))))
 
63
 
 
64
(defthm lemma-to-be-instantiated
 
65
  (implies (and (input-assumptions n)
 
66
                (bindings n)
 
67
                (spec (*::in) (*::longop)))
 
68
           (result (*::in)
 
69
                   (out (+ 2 n)))))
 
70
 
 
71
(defthm correctness-of-pipeline
 
72
  (implies (input-assumptions n)
 
73
           (result (in n)
 
74
                   (out (+ 2 n))))
 
75
  :hints (("Goal" :use ((:instance
 
76
                         (:functional-instance
 
77
                          lemma-to-be-instantiated
 
78
                          (*::in     (lambda () (in k)))
 
79
                          (*::longop (lambda () (longop k))))
 
80
                         (k n))))))