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
|
; Copyright (C) 2024, Matt Kaufmann
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; See README.txt for an overview of this example.
(in-package "ACL2")
; Define *mem-len* and support for the :LOGIC functions of the abstract stobj,
; mem, introduced below.
(include-book "logic")
(defstobj mem$c ; concrete stobj representing memory with an array
(mem$c-ar :type (array t (*mem-len*))))
(defun-nx mem$corr (mem$c x)
(declare (xargs :stobjs mem$c))
(equal x (nth 0 mem$c)))
(defun lookup$c (i mem$c)
; This is a little wrapper for mem$c-ari.
; We use cw to print evidence that mem$c-ari is being called.
(declare (xargs :stobjs mem$c
:guard (and (natp i)
(< i (mem$c-ar-length mem$c)))))
(prog2$ (cw "@@ Calling: ~x0~|" `(mem$c-ari ,i mem$c))
(mem$c-ari i mem$c)))
(defun update$c (i v mem$c)
; This is a little wrapper for update-mem$c-ari.
; We use cw to print evidence that update-mem$c-ari is being called.
(declare (xargs :stobjs mem$c
:guard (and (natp i)
(< i (mem$c-ar-length mem$c)))))
(prog2$ (cw "@@ Calling: ~x0~|" `(update-mem$c-ari ,i ,v mem$c))
(update-mem$c-ari i v mem$c)))
(progn
; These are the events that are automatically generated by the defabsstobj
; event below. They all prove automatically.
(DEFTHM CREATE-MEM{CORRESPONDENCE}
(MEM$CORR (CREATE-MEM$C) (CREATE-MEM$A))
:RULE-CLASSES NIL)
(DEFTHM CREATE-MEM{PRESERVED}
(MEM$AP (CREATE-MEM$A))
:RULE-CLASSES NIL)
(DEFTHM LOOKUP{CORRESPONDENCE}
(IMPLIES (AND (MEM$CORR MEM$C MEM)
(MEM-INDEXP I)
(MEM$AP MEM))
(EQUAL (LOOKUP$C I MEM$C)
(LOOKUP$A I MEM)))
:RULE-CLASSES NIL)
(DEFTHM LOOKUP{GUARD-THM}
(IMPLIES (AND (MEM$CORR MEM$C MEM)
(MEM-INDEXP I)
(MEM$AP MEM))
(AND (NATP I)
(< I (MEM$C-AR-LENGTH MEM$C))))
:RULE-CLASSES NIL)
(DEFTHM UPDATE{CORRESPONDENCE}
(IMPLIES (AND (MEM$CORR MEM$C MEM)
(MEM-INDEXP I)
(MEM$AP MEM))
(MEM$CORR (UPDATE$C I V MEM$C)
(UPDATE$A I V MEM)))
:RULE-CLASSES NIL)
(DEFTHM UPDATE{GUARD-THM}
(IMPLIES (AND (MEM$CORR MEM$C MEM)
(MEM-INDEXP I)
(MEM$AP MEM))
(AND (NATP I)
(< I (MEM$C-AR-LENGTH MEM$C))))
:RULE-CLASSES NIL)
(DEFTHM UPDATE{PRESERVED}
(IMPLIES (AND (MEM-INDEXP I) (MEM$AP MEM))
(MEM$AP (UPDATE$A I V MEM)))
:RULE-CLASSES NIL)
)
(defabsstobj mem ; abstract stobj, based on an array but attachable
:foundation mem$c
:recognizer (memp :logic mem$ap :exec mem$cp)
:creator (create-mem :logic create-mem$a :exec create-mem$c)
:corr-fn mem$corr
:exports ((lookup :logic lookup$a :exec lookup$c)
(update :logic update$a :exec update$c))
:attachable t)
; Next we prove typical read-over-write and write-over-write theorems about
; memory access.
(defthm lookup-update
(implies (and (mem-indexp i)
(mem-indexp j))
(equal (lookup i (update j v mem))
(if (equal i j)
v
(lookup i mem)))))
(defthm update-update-same
(implies (equal i1 i2)
(equal (update i2 v2 (update i1 v1 mem))
(update i2 v2 mem))))
(defthm update-update-different
(implies (and (mem-indexp i1)
(mem-indexp i2)
(not (equal i1 i2)))
(equal (update i2 v2 (update i1 v1 mem))
(update i1 v1 (update i2 v2 mem)))))
; This little test at certification time is skipped by include-book:
(value-triple (update 3 'three mem)
:stobjs-out '(mem))
; This little test at certification time is skipped by include-book:
(assert-event (equal (lookup 3 mem)
'three))
|
