~/Dropbox/talks/key-workshop-july-2015/demos$ acl2-7.1 Welcome to Clozure Common Lisp Version 1.11-dev-r16378M-trunk (DarwinX8664)! ACL2 Version 7.1 built May 6, 2015 18:48:38. Copyright (C) 2015, Regents of the University of Texas ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the LICENSE file distributed with ACL2. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Includes support for hash cons, memoization, and applicative hash tables. See the documentation topic note-7-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lsp". ACL2 Version 7.1. Level 1. Cbd "/Users/kaufmann/". System books directory "/Users/kaufmann/acl2/v7-1/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 7.1. Level 1. Cbd "/Users/kaufmann/Dropbox/talks/key-workshop-july-2015/demos/". System books directory "/Users/kaufmann/acl2/v7-1/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "models/jvm/m5/jvm-fact-setup" :dir :system) Summary Form: ( INCLUDE-BOOK "models/jvm/m5/jvm-fact-setup" ...) Rules: NIL Time: 0.63 seconds (prove: 0.00, print: 0.00, other: 0.63) "/Users/kaufmann/acl2/v7-1/books/models/jvm/m5/jvm-fact-setup.lisp" ACL2 !>(in-package "M5") "M5" M5 !>(defun demo-fact (n) (let ((sched (fact-sched 0 n))) (list (list 'steps (len sched)) (list 'ans (top (stack (top-frame 0 (run sched (make-state (list (cons 0 (make-thread (push (make-frame 0 nil (push n nil) '((INVOKESTATIC "Demo" "fact" 1)) 'UNLOCKED "Demo") nil) 'SCHEDULED nil))) *demo-heap* *demo-class-table*))))))))) Since DEMO-FACT is non-recursive, its admission is trivial. We observe that the type of DEMO-FACT is described by the theorem (AND (CONSP (DEMO-FACT N)) (TRUE-LISTP (DEMO-FACT N))). We used primitive type reasoning. Summary Form: ( DEFUN DEMO-FACT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DEMO-FACT M5 !>(lookup-method "fact" "Demo" *demo-class-table*) ("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN)) M5 !>(demo-fact 5) ((STEPS 50) (ANS 120)) M5 !>(demo-fact 17) ((STEPS 158) (ANS -288522240)) M5 !>(! 17) ; factorial of 17 (previous name: fact) 355687428096000 M5 !>(int-fix (! 17)) ; low 32 bits of 17 factorial -288522240 M5 !>(defthm fact-is-correct (implies (poised-to-invoke-fact th s n) (equal (run (fact-sched th n) s) (modify th s :pc (+ 3 (pc (top-frame th s))) :stack (push (int-fix (! n)) (pop (stack (top-frame th s))))))) :hints (("Goal" :induct (induction-hint th s n)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. We have been told to use induction. One induction scheme is suggested by the induction hint. We will induct according to a scheme suggested by (INDUCTION-HINT TH S N). This suggestion was produced using the :induction rule INDUCTION-HINT. If we let (:P N S TH) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N) (MAKE-STATE (BIND TH (MAKE-THREAD (PUSH (MAKE-FRAME 8 (LIST (TOP (STACK (TOP-FRAME TH S)))) (PUSH (+ -1 (TOP (STACK (TOP-FRAME TH S)))) (PUSH (TOP (STACK (TOP-FRAME TH S))) NIL)) (METHOD-PROGRAM '("fact" (INT) NIL (ILOAD_0) (IFLE 12) (ILOAD_0) (ILOAD_0) (ICONST_1) (ISUB) (INVOKESTATIC "Demo" "fact" 1) (IMUL) (IRETURN) (ICONST_1) (IRETURN))) 'UNLOCKED "Demo") (PUSH (MAKE-FRAME (+ 3 (PC (TOP (CALL-STACK TH S)))) (LOCALS (TOP (CALL-STACK TH S))) (POP (STACK (TOP (CALL-STACK TH S)))) (PROGRAM (TOP (CALL-STACK TH S))) (SYNC-FLG (TOP (CALL-STACK TH S))) (CUR-CLASS (TOP (CALL-STACK TH S)))) (POP (CALL-STACK TH S)))) 'SCHEDULED (RREF TH S)) (THREAD-TABLE S)) (HEAP S) (CLASS-TABLE S)) TH)) (:P N S TH)) (IMPLIES (ZP N) (:P N S TH))). This induction is justified by the same argument used to admit INDUCTION-HINT. Note, however, that the unmeasured variable S is being instantiated. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM FACT-IS-CORRECT ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION !) (:DEFINITION BINARY-APPEND) (:DEFINITION BIND-FORMALS) (:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-HEAPREF) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION DEREF) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFLE) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IMUL) (:DEFINITION EXECUTE-INVOKESTATIC) (:DEFINITION EXECUTE-IRETURN) (:DEFINITION EXECUTE-ISUB) (:DEFINITION FACT-SCHED) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION POPN) (:DEFINITION REPEAT) (:DEFINITION REVERSE) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART ARG2) (:EXECUTABLE-COUNTERPART ARG3) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART INT-FIX) (:EXECUTABLE-COUNTERPART METHOD-PROGRAM) (:EXECUTABLE-COUNTERPART METHOD-SYNC) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART PUSH) (:EXECUTABLE-COUNTERPART REVERSE) (:EXECUTABLE-COUNTERPART TOP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:INDUCTION INDUCTION-HINT) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE BIND-FORMALS-OPENER) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA4A) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE POPN-OPENER) (:REWRITE REPEAT-OPENER) (:REWRITE RUN-APPEND) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION !) (:TYPE-PRESCRIPTION INTEGERP-FACTORIAL) (:TYPE-PRESCRIPTION INTP)) Time: 0.19 seconds (prove: 0.18, print: 0.00, other: 0.00) Prover steps counted: 54552 FACT-IS-CORRECT M5 !>(quit) ~/Dropbox/talks/key-workshop-july-2015/demos$