blob: d8d4f10873d1654f4f0497acc98514fe8a15bf30 (
plain)
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
|
(in-package "ACL2")
(include-book "../../../../arithmetic-3/bind-free/top")
(include-book "../../../../arithmetic-3/floor-mod/floor-mod")
(set-non-linearp nil)
;;; The following program sums the integers from 1 to N on the early Mostek
;;; 6502 microprocessor. A is an 8-bit wide accumulator. N is a single byte
;;; of data in memory. C is a carry flag. We prove that the limited (8-bit)
;;; precision computation delivers the correct result, provided N*(N+1)/2
;;; is less than 256 and N is greater than 0.
;;; LDA #0 ; load A immediate with the constant 0
;;; CLC ; clear the carry flag
;;; LOOP ADC N ; add with carry N to A
;;; DEC N ; decrement N
;;; BNE LOOP ; branch if N is non-zero to LOOP
;;; Provide semantics for the 6502 DEC instruction.
(defun dec (x)
(if (zp x)
255
(1- x)))
;;; Mechanically derived
(defun wp-loop (n a c nsave)
(declare (xargs :measure (dec n)))
(if (equal (dec n) 0)
(equal (mod (+ c (+ a n)) 256)
(floor (* nsave (1+ nsave)) 2))
(wp-loop (dec n)
(mod (+ c (+ a n)) 256)
(floor (+ c (+ a n)) 256)
nsave)))
;;; Weakest precondition at beginning of program
(defun wp-1 (n nsave)
(wp-loop n 0 0 nsave))
(defthm wp-sum-loop-generalization
(implies (and (not (zp n))
(< (+ a (floor (* n (1+ n)) 2)) 256)
(natp a)
(equal c 0)
(natp nsave))
(equal (wp-loop n a c nsave)
(equal (+ a (floor (* n (1+ n)) 2))
(floor (* nsave (1+ nsave)) 2)))))
(defthm wp-loop-is-correct
(implies (and (not (zp n))
(equal nsave n)
(< (floor (* n (1+ n)) 2) 256))
(wp-1 n nsave)))
|
