/usr/share/acl2-7.2dfsg/books/system/verified-termination-and-guards.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | ; Copyright (C) 2014, Regents of the University of Texas
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This book was originally created by David Rager (April, 2012) to serve as a
; place to verify the termination and guards of ACL2 system functions. This
; book is included in system/top.lisp; either might usefully be included when
; reasoning about system functions.
; Note that calling verify-termination also verifies the guards of any function
; that has a guard specified. In the event that there is no guard specified,
; then one must also call verify-guards to verify that the implicit guard of
; "t" is strong enough. See :doc verify-termination for further details.
(in-package "ACL2")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The following section was written by Matt Kaufmann.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(verify-termination collect-by-position) ; and guards
; Copied exactly (11/18/2015) from ACL2 source file axioms.lisp, towards guard
; verification for make-lambda-application:
(local
(encapsulate
()
; We wish to prove symbol-listp-all-vars1, below, so that we can verify the
; guards on all-vars1. But it is in a mutually recursive clique. Our strategy
; is simple: (1) define the flagged version of the clique, (2) prove that it is
; equal to the given pair of official functions, (3) prove that it has the
; desired property and (4) then obtain the desired property of the official
; function by instantiation of the theorem proved in step 3, using the theorem
; proved in step 2 to rewrite the flagged flagged calls in that instance to the
; official ones.
; Note: It would probably be better to make all-vars1/all-vars1-lst local,
; since it's really not of any interest outside the guard verification of
; all-vars1. However, since we are passing through this file more than once,
; that does not seem to be an option.
(local
(defun all-vars1/all-vars1-lst (flg lst ans)
(if (eq flg 'all-vars1)
(cond ((variablep lst) (add-to-set-eq lst ans))
((fquotep lst) ans)
(t (all-vars1/all-vars1-lst 'all-vars-lst1 (cdr lst) ans)))
(cond ((endp lst) ans)
(t (all-vars1/all-vars1-lst 'all-vars-lst1 (cdr lst)
(all-vars1/all-vars1-lst 'all-vars1 (car lst) ans)))))))
(local
(defthm step-1-lemma
(equal (all-vars1/all-vars1-lst flg lst ans)
(if (equal flg 'all-vars1) (all-vars1 lst ans) (all-vars1-lst lst ans)))))
(local
(defthm step-2-lemma
(implies (and (symbol-listp ans)
(if (equal flg 'all-vars1)
(pseudo-termp lst)
(pseudo-term-listp lst)))
(symbol-listp (all-vars1/all-vars1-lst flg lst ans)))))
(defthm symbol-listp-all-vars1
(implies (and (symbol-listp ans)
(pseudo-termp lst))
(symbol-listp (all-vars1 lst ans)))
:hints (("Goal" :use (:instance step-2-lemma (flg 'all-vars1)))))))
(verify-termination make-lambda-application)
(verify-termination >=-len) ; and guards
(verify-termination all->=-len) ; and guards
(verify-termination strip-cadrs) ; and guards
(verify-termination alist-to-doublets) ; and guards
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; The following section was written by David L. Rager.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(verify-termination plausible-dclsp1)
(verify-termination plausible-dclsp)
(verify-termination fetch-dcl-fields2)
(verify-termination fetch-dcl-fields1)
(verify-termination fetch-dcl-fields)
(verify-termination fetch-dcl-field)
(verify-termination strip-keyword-list)
(verify-termination strip-dcls1)
(verify-termination strip-dcls)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|