1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
;; Copyright (C) 2015, University of British Columbia
;; Written by Yan Peng (May 2019)
;;
;; License: A 3-clause BSD license.
;; See the LICENSE file distributed with ACL2
(in-package "SMT")
(include-book "inverter")
; cert_param: (uses-smtlink)
(value-triple (tshell-ensure))
(add-default-hints '((SMT::SMT-computed-hint clause)))
(defprod ringosc3
((n1 sig-path-p)
(n2 sig-path-p)
(n3 sig-path-p)
(inv1 inverter-p)
(inv2 inverter-p)
(inv3 inverter-p)))
(define ringosc3-constraints ((r ringosc3-p))
:returns (ok booleanp)
(and (equal (inverter->input (ringosc3->inv1 r))
(ringosc3->n3 r))
(equal (inverter->output (ringosc3->inv1 r))
(ringosc3->n1 r))
(equal (inverter->input (ringosc3->inv2 r))
(ringosc3->n1 r))
(equal (inverter->output (ringosc3->inv2 r))
(ringosc3->n2 r))
(equal (inverter->input (ringosc3->inv3 r))
(ringosc3->n2 r))
(equal (inverter->output (ringosc3->inv3 r))
(ringosc3->n3 r))
))
(define ringosc3-valid ((r ringosc3-p)
(tr any-trace-p))
:returns (ok booleanp)
(b* (((unless (ringosc3-constraints r)) nil)
(r (ringosc3-fix r))
(i1 (ringosc3->inv1 r))
(i1valid? (inverter-valid i1 tr))
((unless i1valid?) nil)
(i2 (ringosc3->inv2 r))
(i2valid? (inverter-valid i2 tr))
((unless i2valid?) nil)
(i3 (ringosc3->inv3 r))
(i3valid? (inverter-valid i3 tr))
((unless i3valid?) nil))
t)
)
(define ringosc3-count ((r ringosc3-p)
(curr any-table-p))
:returns (markers maybe-integer-p
:hints (("Goal" :in-theory (e/d (inverter-count
boolval)))))
:guard-hints (("Goal"
:in-theory (e/d (inverter-count) ())))
(b* ((r (ringosc3-fix r))
(i1 (ringosc3->inv1 r))
(i2 (ringosc3->inv2 r))
(i3 (ringosc3->inv3 r))
(i1-count (inverter-count i1 curr))
((if (equal i1-count (maybe-integer-fix nil)))
(maybe-integer-fix nil))
(i2-count (inverter-count i2 curr))
((if (equal i2-count (maybe-integer-fix nil)))
(maybe-integer-fix nil))
(i3-count (inverter-count i3 curr))
((if (equal i3-count (maybe-integer-fix nil)))
(maybe-integer-fix nil)))
(maybe-integer-some
(+ (maybe-integer-some->val i1-count)
(maybe-integer-some->val i2-count)
(maybe-integer-some->val i3-count))))
)
(define ringosc3-one-safe-state ((r ringosc3-p)
(curr any-table-p))
:returns (ok booleanp)
(b* ((r (ringosc3-fix r))
(count (ringosc3-count r curr))
((if (equal count (maybe-integer-fix nil))) nil))
(equal (maybe-integer-some->val count) 1))
)
(define ringosc3-one-safe-trace ((r ringosc3-p)
(tr any-trace-p))
:returns (ok booleanp)
:measure (len tr)
(b* ((r (ringosc3-fix r))
((unless (consp (any-trace-fix tr))) t)
(first (car (any-trace-fix tr)))
(rest (cdr (any-trace-fix tr)))
((unless (ringosc3-one-safe-state r first)) nil))
(ringosc3-one-safe-trace r rest)))
(acl2::without-waterfall-parallelism ; MattK. mod for ACL2(p)
(defthm ringosc3-one-safe-lemma
(implies (and (ringosc3-p r)
(any-trace-p tr)
(consp (any-trace-fix tr))
(consp (any-trace-fix (cdr (any-trace-fix tr))))
(ringosc3-constraints r)
(inverter-valid-step (ringosc3->inv1 r)
(car (any-trace-fix tr))
(car (any-trace-fix (cdr (any-trace-fix tr)))))
(inverter-valid (ringosc3->inv1 r)
(cdr (any-trace-fix tr)))
(inverter-valid-step (ringosc3->inv2 r)
(car (any-trace-fix tr))
(car (any-trace-fix (cdr (any-trace-fix tr)))))
(inverter-valid (ringosc3->inv2 r)
(cdr (any-trace-fix tr)))
(inverter-valid-step (ringosc3->inv3 r)
(car (any-trace-fix tr))
(car (any-trace-fix (cdr (any-trace-fix tr)))))
(inverter-valid (ringosc3->inv3 r)
(cdr (any-trace-fix tr)))
(ringosc3-one-safe-state r (car (any-trace-fix tr))))
(ringosc3-one-safe-state r (car (any-trace-fix (cdr (any-trace-fix
tr))))))
:hints (("Goal"
:smtlink
(:fty (inverter ringosc3 any-trace any-table sig-path-list sig-path
sig maybe-integer)
:functions ((ringosc3-one-safe-trace :formals ((r ringosc3-p)
(tr any-trace-p))
:returns ((ok booleanp))
:level 1)
(ringosc3-valid :formals ((r ringosc3-p)
(tr any-trace-p))
:returns ((ok booleanp))
:level 1)
(inverter-valid :formals ((i inverter-p)
(tr any-trace-p))
:returns ((ok booleanp))
:level 1)
(sigs-in-bool-table :formals ((sigs sig-path-listp)
(st any-table-p))
:returns ((ok booleanp))
:level 2)
(sigs-in-bool-trace :formals ((sigs sig-path-listp)
(tr any-trace-p))
:returns ((ok booleanp))
:level 1)
(inverter-valid :formals ((inverter inverter-p)
(tr any-trace-p))
:returns ((ok booleanp))
:level 0)
))
)))
)
(defthm ringosc3-one-safe
(implies (and (ringosc3-p r)
(any-trace-p tr)
(consp tr)
(ringosc3-valid r tr)
(ringosc3-one-safe-state r (car tr)))
(ringosc3-one-safe-trace r tr))
:hints (("Goal"
:induct (ringosc3-one-safe-trace r tr)
:in-theory (e/d (ringosc3-one-safe-trace
ringosc3-valid
inverter-valid)
(ringosc3-one-safe-lemma)))
("Subgoal *1/1.1"
:use ((:instance ringosc3-one-safe-lemma
(r r)
(tr tr)))
)))
|
