1; This file tells the whole m1 story from scratch in a minimalist 2; setting. Then, that story is redeveloped in the books 3 4; m1.lisp 5; m1-lemmas.lisp 6; m1-compiler.lisp 7; m1-ifact.lisp 8 9#| 10(include-book "problem-set-1-answers") 11 12(begin-book t :ttags :all) 13|# 14 15(in-package "M1") 16 17; Here is the semantics of the M1 machine. In addition to the ACL2 primitive 18; functions in the "M1" package, we take advantage of the following 19; functions defined in "problem-set-1-answers.lisp": 20 21; push, top, pop, - intro material of Problem Set 1 22; nth - intro material of Problem Set 1 23; update-nth - Problem 1-14 24; make-state, pc, etc - intro material of Problem Set 1 25; opcode, arg1, arg2 - Problem 1-4 26 27(defun next-inst (s) 28 (nth (pc s) (program s))) 29 30; Now we define the semantics of each instruction. These 31; functions are called ``semantic functions.'' 32 33(defun execute-ICONST (inst s) 34 (make-state (+ 1 (pc s)) 35 (locals s) 36 (push (arg1 inst) (stack s)) 37 (program s))) 38 39(defun execute-ILOAD (inst s) 40 (make-state (+ 1 (pc s)) 41 (locals s) 42 (push (nth (arg1 inst) 43 (locals s)) 44 (stack s)) 45 (program s))) 46 47(defun execute-IADD (inst s) 48 (declare (ignore inst)) 49 (make-state (+ 1 (pc s)) 50 (locals s) 51 (push (+ (top (pop (stack s))) 52 (top (stack s))) 53 (pop (pop (stack s)))) 54 (program s))) 55 56(defun execute-ISTORE (inst s) 57 (make-state (+ 1 (pc s)) 58 (update-nth (arg1 inst) (top (stack s)) (locals s)) 59 (pop (stack s)) 60 (program s))) 61 62(defun execute-ISUB (inst s) 63 (declare (ignore inst)) 64 (make-state (+ 1 (pc s)) 65 (locals s) 66 (push (- (top (pop (stack s))) 67 (top (stack s))) 68 (pop (pop (stack s)))) 69 (program s))) 70 71(defun execute-IMUL (inst s) 72 (declare (ignore inst)) 73 (make-state (+ 1 (pc s)) 74 (locals s) 75 (push (* (top (pop (stack s))) 76 (top (stack s))) 77 (pop (pop (stack s)))) 78 (program s))) 79 80(defun execute-GOTO (inst s) 81 (make-state (+ (arg1 inst) (pc s)) 82 (locals s) 83 (stack s) 84 (program s))) 85 86(defun execute-IFLE (inst s) 87 (make-state (if (<= (top (stack s)) 0) 88 (+ (arg1 inst) (pc s)) 89 (+ 1 (pc s))) 90 (locals s) 91 (pop (stack s)) 92 (program s))) 93 94(defun do-inst (inst s) 95 (if (equal (op-code inst) 'ICONST) 96 (execute-ICONST inst s) 97 (if (equal (op-code inst) 'ILOAD) 98 (execute-ILOAD inst s) 99 (if (equal (op-code inst) 'ISTORE) 100 (execute-ISTORE inst s) 101 (if (equal (op-code inst) 'IADD) 102 (execute-IADD inst s) 103 (if (equal (op-code inst) 'ISUB) 104 (execute-ISUB inst s) 105 (if (equal (op-code inst) 'IMUL) 106 (execute-IMUL inst s) 107 (if (equal (op-code inst) 'GOTO) 108 (execute-GOTO inst s) 109 (if (equal (op-code inst) 'IFLE) 110 (execute-IFLE inst s) 111 s))))))))) 112 113 114(defun step (s) 115 (do-inst (next-inst s) s)) 116 117(defun run (sched s) 118 (if (endp sched) 119 s 120 (run (cdr sched) (step s)))) 121 122; =========================================================================== 123; Now I present an example of an M1 program and its execution. 124 125(defconst *ifact-program* 126 ; Imagine compiling: 127 ; a = 1; 128 ; while (n > 0) 129 ; { a = n * a; 130 ; n = n-1;}; 131 ; return a; 132 133 '((ICONST 1) ;;; 0 134 (ISTORE 1) ;;; 1 a = 1; 135 (ILOAD 0) ;;; 2 while ; loop: pc=2 136 (IFLE 10) ;;; 3 (n > 0) 137 (ILOAD 0) ;;; 4 { 138 (ILOAD 1) ;;; 5 139 (IMUL) ;;; 6 140 (ISTORE 1) ;;; 7 a = n * a; 141 (ILOAD 0) ;;; 8 142 (ICONST 1) ;;; 9 143 (ISUB) ;;; 10 144 (ISTORE 0) ;;; 11 n = n-1; 145 (GOTO -10) ;;; 12 } ; jump to loop 146 (ILOAD 1) ;;; 13 147 (HALT) ;;; 14 return a; 148 )) 149 150; You can just evaluate this test and get the answer shown. 151 152#| 153(run 154 '(0 0 0 0 0 0 0 0 0 0 ; 100 clock ticks 155 0 0 0 0 0 0 0 0 0 0 156 0 0 0 0 0 0 0 0 0 0 157 0 0 0 0 0 0 0 0 0 0 158 0 0 0 0 0 0 0 0 0 0 159 0 0 0 0 0 0 0 0 0 0 160 0 0 0 0 0 0 0 0 0 0 161 0 0 0 0 0 0 0 0 0 0 162 0 0 0 0 0 0 0 0 0 0 163 0 0 0 0 0 0 0 0 0 0) 164 (make-state 165 0 ; pc 166 '(5 0) ; locals: n=5, a=0 167 nil ; stack 168 *ifact-program* ; our program, above 169 )) 170 171; answer: 172(14 ; final pc 173 (0 120) ; final locals: n=0, a=120 174 (120) ; final stack 175 ((ICONST 1) ; our program, again 176 (ISTORE 1) 177 (ILOAD 0) 178 (IFLE 10) 179 (ILOAD 0) 180 (ILOAD 1) 181 (IMUL) 182 (ISTORE 1) 183 (ILOAD 0) 184 (ICONST 1) 185 (ISUB) 186 (ISTORE 0) 187 (GOTO -10) 188 (ILOAD 1) 189 (HALT))) 190|# 191 192; We can record this in a certified book as a theorem by just 193; equating the expression and its computed value: 194 195(defthm factorial-example-0 196 (equal (run 197 '(0 0 0 0 0 0 0 0 0 0 ; 100 clock ticks 198 0 0 0 0 0 0 0 0 0 0 199 0 0 0 0 0 0 0 0 0 0 200 0 0 0 0 0 0 0 0 0 0 201 0 0 0 0 0 0 0 0 0 0 202 0 0 0 0 0 0 0 0 0 0 203 0 0 0 0 0 0 0 0 0 0 204 0 0 0 0 0 0 0 0 0 0 205 0 0 0 0 0 0 0 0 0 0 206 0 0 0 0 0 0 0 0 0 0) 207 (make-state 208 0 ; pc 209 '(5 0) ; locals: n=5, a=0 210 nil ; stack 211 *ifact-program* ; our program, above 212 )) 213 '(14 ; final pc 214 (0 120) ; final locals: n=0, a=120 215 (120) ; final stack 216 ((ICONST 1) ; our program, again 217 (ISTORE 1) 218 (ILOAD 0) 219 (IFLE 10) 220 (ILOAD 0) 221 (ILOAD 1) 222 (IMUL) 223 (ISTORE 1) 224 (ILOAD 0) 225 (ICONST 1) 226 (ISUB) 227 (ISTORE 0) 228 (GOTO -10) 229 (ILOAD 1) 230 (HALT)))) 231 :rule-classes nil) 232 233; =========================================================================== 234; Now I make it easier to write schedules and write a schedule for ifact. 235 236; Here we use 237; app - Problem 1-10 238; repeat - Problem 1-12 239 240(defun ifact-loop-sched (n) 241 (if (zp n) 242 (repeat 0 4) 243 (app (repeat 0 11) 244 (ifact-loop-sched (- n 1))))) 245 246; This can be explained: to schedule the ifact program on n starting 247; at the loop pc = 2: If n is 0, schedule 4 steps, namely the 248; instructions at pcs 2, 3, 13, and 14, ending at the HALT. 249; Otherwise, if n is not 0, schedule the 11 instructions at pcs 2 250; through 12, ending back at pc = 2, and then schedule ifact for n-1. 251 252; We then use this to say how to schedule a complete ifact computation, 253; starting at pc = 0. 254 255(defun ifact-sched (n) 256 (app (repeat 0 2) 257 (ifact-loop-sched n))) 258 259; =========================================================================== 260; Now I write our example above in a slightly more precise and abstract 261; way. 262 263(defun ! (n) 264 (if (zp n) 265 1 266 (* n (! (- n 1))))) 267 268; And here is a function that computes factorial by running M1: 269 270(defun test-ifact (n) 271 (top 272 (stack 273 (run (ifact-sched n) 274 (make-state 0 275 (cons n (cons 0 nil)) 276 nil 277 *ifact-program*))))) 278 279(acl2::comp t) ; added by Matt K. for GCL 280 281(defthm factorial-example-1 282 (equal (test-ifact 5) 283 (! 5)) 284 :rule-classes nil) 285 286(defthm factorial-example-2 287 (equal (test-ifact 1000) 288 (! 1000)) 289 :rule-classes nil) 290; =========================================================================== 291 292; Problem 2a-1: Define the constant *even-program* as an M1 program that takes 293; a natural number, i, as local variable 0 and halts with 1 on the stack if i 294; is even and with 0 on the stack if i is odd. For example, if the program is 295; started with locals (18) then it pushes 1, but if started with (19) it pushes 296; 0. 297 298; My Answer: 299 300(defconst *even-program* 301 '((iload 0) 302 (ifle 12) 303 (iload 0) 304 (iconst 1) 305 (isub) 306 (ifle 6) 307 (iload 0) 308 (iconst 2) 309 (isub) 310 (istore 0) 311 (goto -10) 312 (iconst 0) 313 (halt) 314 (iconst 1) 315 (halt))) 316 317(defun even-sched (i) 318 (if (zp i) 319 (repeat 0 4) 320 (if (equal i 1) 321 (repeat 0 8) 322 (app (repeat 0 11) 323 (even-sched (- i 2)))))) 324 325(defun test-even (i) 326 (top 327 (stack 328 (run (even-sched i) 329 (make-state 0 330 (list i) 331 nil 332 *even-program*))))) 333 334(defthm test-even-theorem 335 (and (equal (test-even 18) 1) 336 (equal (test-even 19) 0) 337 (equal (test-even 235) 0) 338 (equal (test-even 234) 1)) 339 :rule-classes nil) 340 341; =========================================================================== 342 343; Now I develop a compiler for a simple language of arithmetic, 344; assignment, and while statements. 345 346; Here we'll use 347; member - Problem 1-15 348; index - Problem 1-16 349; len - Problem 1-9 350 351; The syntax of our language is 352 353; <expr> := <var>|<int-constant>|( <expr> <op> <expr> ) 354 355; <op> := + | - | * 356 357; <test> := ( <expr> > <expr>) 358 359; <stmt> := ( <var> = <expr> ) | 360; ( while <test> <stmt*>) | 361; ( return <expr> ) 362 363; <stmt*> := <stmt> | <stmt> <stmt*> 364 365; <program> := ( <stmt*> ) 366 367; <var> := any ACL2 symbol 368 369; <int-constant> := any ACL2 integer 370 371; Thus, an example program is: 372 373; ((a = 1) 374; (while (n > 0) 375; (a = (n * a)) 376; (n = (n - 1))) 377; (return a)) 378 379; For the purposes of this exercise, we will assume that every 380; program we wish to compile is syntactically well-formed. 381 382; We first define a function, collect-vars-in-stmt*, that sweeps over 383; a list of statements and collects all the variables it finds. It 384; adds the variables to the end of a running accumulator. That 385; accumulator will be initiallized to the list of formals of the 386; method we're compiling. The new variables accumulated onto it will 387; be the temporary variables of the method. The order of the 388; collected list will determine where the variables are allocated in 389; the locals. The first formal will be given index 0, the next index 390; 1, etc. 391 392(defun collect-at-end (list e) ;;; Add e to the end of list 393 (if (member e list) ;;; unless it is already in list. 394 list 395 (app list (cons e nil)))) 396 397; These two theorems are necessary for the proof of termination of 398; collect-vars-in-expr, below. 399 400(defthm nth-nil 401 (equal (nth n nil) nil)) 402 403(defthm acl2-count-nth 404 (implies (consp list) 405 (< (acl2-count (nth n list)) 406 (acl2-count list))) 407 :rule-classes :linear) 408 409(defun collect-vars-in-expr (vars expr) ;;; Sweep expr and collect 410 (if (atom expr) ;;; all variable names into 411 (if (symbolp expr) ;;; vars. 412 (collect-at-end vars expr) 413 vars) 414 (collect-vars-in-expr 415 (collect-vars-in-expr vars 416 (nth 0 expr)) 417 (nth 2 expr)))) 418 419; Note that if expr is not an atom, it is of the form 420; ( <expr> + <expr> ) or 421; ( <expr> - <expr> ) or 422; ( <expr> * <expr> ). 423 424; Hence, (nth 0 expr) is the first subexpression and (nth 2 expr) is 425; the second. 426 427; Now we collect the vars in a statement. This is defined mutually 428; recursively with the vars in a list of statements. 429 430(mutual-recursion 431 432(defun collect-vars-in-stmt* (vars stmt-list) 433 (if (endp stmt-list) 434 vars 435 (collect-vars-in-stmt* 436 (collect-vars-in-stmt vars (car stmt-list)) 437 (cdr stmt-list)))) 438 439(defun collect-vars-in-stmt (vars stmt) 440 (if (equal (nth 1 stmt) '=) 441 (collect-vars-in-expr 442 (collect-at-end vars (nth 0 stmt)) 443 (nth 2 stmt)) 444 (if (equal (nth 0 stmt) 'WHILE) 445 (collect-vars-in-stmt* 446 (collect-vars-in-expr vars (nth 1 stmt)) 447 (cdr (cdr stmt))) 448 (if (equal (nth 0 stmt) 'RETURN) 449 (collect-vars-in-expr vars (nth 1 stmt)) 450 vars)))) 451) 452 453; We will use the function index to determine the position of a 454; variable in the list of variables. 455 456; Now we begin the code generation. To compile an expression 457; like (<expr> op <expr>), we'll generate code that leaves the 458; values of the two subexpressions on the stack and then we'll 459; execute the bytecode that pops those two values and pushes the 460; result of executing op. 461 462; The bytecode program to execute op (assuming its arguments are 463; on the stack): 464 465(defun OP! (op) 466 (if (equal op '+) 467 '((IADD)) 468 (if (equal op '-) 469 '((ISUB)) 470 (if (equal op '*) 471 '((IMUL)) 472 '((ILLEGAL)))))) 473 474; Note that the output above is a bytecode program, i.e., a list of 475; instructions (in this case, always a trivial list of length 1). All 476; our functions for generating code generate bytecode programs so we 477; can combine them with concatentation. 478 479; The bytecode program to put the value of a variable on the stack: 480 481(defun ILOAD! (vars var) 482 (cons (cons 'ILOAD (cons (index var vars) nil)) 483 nil)) 484 485; The bytecode program to put the value of a constant on the stack: 486 487(defun ICONST! (n) 488 (cons (cons 'ICONST (cons n nil)) 489 nil)) 490 491; The bytecode program to put the value of an expression on the stack: 492 493(defun expr! (vars expr) 494 (if (atom expr) 495 (if (symbolp expr) 496 (ILOAD! vars expr) 497 (ICONST! expr)) 498 (app (expr! vars (nth 0 expr)) 499 (app (expr! vars (nth 2 expr)) 500 (OP! (nth 1 expr)))))) 501 502; The bytecode program to test the top of the stack and branch by offset 503; if it is less than or equal to 0: 504 505(defun IFLE! (offset) 506 (cons (cons 'IFLE (cons offset nil)) 507 nil)) 508 509; The bytecode program to jump by offset: 510 511(defun GOTO! (offset) 512 (cons (cons 'GOTO (cons offset nil)) 513 nil)) 514 515; The bytecode program to evaluate a while statement (given the 516; bytecode programs for the test and body): 517 518(defun while! (test-code body-code) 519 520; To compile (while test stmt1...stmtn) we first compile code that 521; leaves a positive on the stack if test is true and a non-positive on 522; the stack if test is false. Call that code test1, ... testk. Then 523; we compile the statements in the body. Call that code body1, ..., 524; bodyn. Note that the length of the test code is k and the length of 525; the body code is n. We return: 526 527; (test1 ; top of WHILE 528; ... 529; testk ; value of test is on the stack 530; (IFLE 2+n) ; if test false, jump past body code 531; body1 532; ... 533; bodyn 534; (GOTO -(n+1+k)) ; go back to top of WHILE 535; ) ; we're done with the WHILE 536 537 (app test-code 538 (app (IFLE! (+ 2 (len body-code))) 539 (app body-code 540 (GOTO! (- (+ (len test-code) 541 1 542 (len body-code)))))))) 543 544; The bytecode program to leave a positive on the stack if test is 545; true and a non-positive otherwise: 546 547(defun test! (vars test) 548 549; Test has to be of the form (x > y), where x and y are expressions. 550; If y is 0, then we can just leave the value of x on the stack, that 551; is, the test is true or false exactly according to whether the value 552; of x is positive or not positive. If y is not 0, we act like we saw 553; (x-y > 0), which is equivalent and which statisfies the first 554; condition. 555 556 (if (equal (nth 1 test) '>) 557 (if (equal (nth 2 test) 0) 558 (expr! vars (nth 0 test)) 559 (app (expr! vars (nth 0 test)) 560 (app (expr! vars (nth 2 test)) 561 '((ISUB))))) 562 '((ILLEGAL)))) 563 564; The bytecode program to pop the stack into the local allocated for var: 565 566(defun ISTORE! (vars var) 567 (cons (cons 'ISTORE (cons (index var vars) nil)) 568 nil)) 569 570; The bytecode programs for a list of statements and for a single statement: 571 572(mutual-recursion 573 574 (defun stmt*! (vars stmt-list) 575 (if (endp stmt-list) 576 nil 577 (app (stmt! vars (car stmt-list)) 578 (stmt*! vars (cdr stmt-list))))) 579 580 (defun stmt! (vars stmt) 581 (if (equal (nth 1 stmt) '=) 582 (app (expr! vars (nth 2 stmt)) 583 (ISTORE! vars (nth 0 stmt))) 584 (if (equal (nth 0 stmt) 'WHILE) 585 (while! 586 (test! vars (nth 1 stmt)) 587 (stmt*! vars (cdr (cdr stmt)))) 588 (if (equal (nth 0 stmt) 'RETURN) 589 (app (expr! vars (nth 1 stmt)) 590 '((HALT))) 591 '((ILLEGAL)))))) 592 ) 593 594; The bytecode program for stmt-list given the initial formals: 595 596(defun compile (formals stmt-list) 597 (stmt*! (collect-vars-in-stmt* formals stmt-list) 598 stmt-list)) 599 600; See Demo1.java 601 602(defthm example-compilation-1 603 (equal (compile '(n) 604 '((a = 1) 605 (while (n > 0) 606 (a = (n * a)) 607 (n = (n - 1))) 608 (return a))) 609 '((ICONST 1) 610 (ISTORE 1) 611 (ILOAD 0) 612 (IFLE 10) 613 (ILOAD 0) 614 (ILOAD 1) 615 (IMUL) 616 (ISTORE 1) 617 (ILOAD 0) 618 (ICONST 1) 619 (ISUB) 620 (ISTORE 0) 621 (GOTO -10) 622 (ILOAD 1) 623 (HALT))) 624 :rule-classes nil) 625 626; See Demo2.java 627 628(defthm example-compilation-2 629 (equal (compile '(n k) 630 '((a = 0) 631 (while (n > k) 632 (a = (a + 1)) 633 (n = (n - 1))) 634 (return a))) 635 '((ICONST 0) 636 (ISTORE 2) 637 (ILOAD 0) 638 (ILOAD 1) 639 (ISUB) 640 (IFLE 10) 641 (ILOAD 2) 642 (ICONST 1) 643 (IADD) 644 (ISTORE 2) 645 (ILOAD 0) 646 (ICONST 1) 647 (ISUB) 648 (ISTORE 0) 649 (GOTO -12) 650 (ILOAD 2) 651 (HALT))) 652 :rule-classes nil) 653 654(defthm example-execution-1 655 (equal (top 656 (stack 657 (run (repeat 0 1000) 658 (make-state 0 659 '(5 0) 660 nil 661 (compile '(n) 662 '((a = 1) 663 (while (n > 0) 664 (a = (n * a)) 665 (n = (n - 1))) 666 (return a))))))) 667 120) 668 :rule-classes nil) 669 670(defthm example-execution-2 671 (equal (top 672 (stack 673 (run (repeat 0 1000) 674 (make-state 0 675 '(10 4 0) 676 nil 677 (compile '(n k) 678 '((a = 0) 679 (while (n > k) 680 (a = (a + 1)) 681 (n = (n - 1))) 682 (return a))))))) 683 6) 684 :rule-classes nil) 685 686; =========================================================================== 687; Now I develop some rules that allow ACL2 to prove theorems 688; about M1 programs. 689 690; Arithmetic 691 692(include-book "arithmetic-3/extra/top-ext" :dir :system) 693 694; Abstract Data Type Stuff 695 696(defthm stacks 697 (and (equal (top (push x s)) x) 698 (equal (pop (push x s)) s) 699 700; These next two are needed because some push expressions evaluate to 701; list constants, e.g., (push 1 (push 2 nil)) becomes '(1 2) and '(1 702; 2) pattern-matches with (cons x s) but not with (push x s). 703 704 (equal (top (cons x s)) x) 705 (equal (pop (cons x s)) s))) 706 707(in-theory (disable push top pop)) 708 709(defthm states 710 (and (equal (pc (make-state pc locals stack program)) pc) 711 (equal (locals (make-state pc locals stack program)) locals) 712 (equal (stack (make-state pc locals stack program)) stack) 713 (equal (program (make-state pc locals stack program)) program) 714 715; And we add the rules to handle constant states: 716 717 (equal (pc (cons pc x)) pc) 718 (equal (locals (cons pc (cons locals x))) locals) 719 (equal (stack (cons pc (cons locals (cons stack x)))) stack) 720 (equal (program (cons pc (cons locals (cons stack (cons program x))))) 721 program))) 722 723 724(in-theory (disable make-state pc locals stack program)) 725 726; Step Stuff 727 728(defthm step-opener 729 (implies (consp (next-inst s)) 730 (equal (step s) 731 (do-inst (next-inst s) s)))) 732 733(in-theory (disable step)) 734 735; Schedules and Run 736 737(defthm run-app 738 (equal (run (app a b) s) 739 (run b (run a s)))) 740 741(defthm run-opener 742 (and (equal (run nil s) s) 743 (equal (run (cons th sched) s) 744 (run sched (step s))))) 745 746(in-theory (disable run)) 747 748; Nth and update-nth 749 750(defthm nth-add1! 751 (implies (natp n) 752 (equal (nth (+ 1 n) list) 753 (nth n (cdr list))))) 754 755(defthm nth-update-nth 756 (implies (and (natp i) (natp j)) 757 (equal (nth i (update-nth j v list)) 758 (if (equal i j) 759 v 760 (nth i list))))) 761 762(defthm update-nth-update-nth-1 763 (implies (and (natp i) (natp j) (not (equal i j))) 764 (equal (update-nth i v (update-nth j w list)) 765 (update-nth j w (update-nth i v list)))) 766 :rule-classes ((:rewrite :loop-stopper ((i j update-nth))))) 767 768(defthm update-nth-update-nth-2 769 (equal (update-nth i v (update-nth i w list)) 770 (update-nth i v list))) 771 772 773; =========================================================================== 774 775; Proof that the factorial code computes factorial. I lay this out as 776; a series of 7 steps. The steps are: 777 778; [1] Specify the concepts related to what you're doing. 779 780; [2] Write the program. 781 782; [3] Specify how long it takes to execute (starting with the 783; loop). In particular, define a scheduler function that 784; will run this program to completion. 785 786; [4] Test the program and your scheduler. 787 788; [5] Prove your program does what it does, starting with the 789; loop. 790 791; [6] Prove what we do is what we want. 792 793; [7] Put it all together. 794 795; Concretely, for the factorial code, here are the steps. 796 797; [1] Specify the concepts related to what you're doing. 798; Typically we do it at two levels, 799; (a) What we want. 800; (b) How we'll do it. 801 802; (a) What we want: 803 804(defun ! (n) 805 (if (zp n) 806 1 807 (* n (! (- n 1))))) 808 809; (b) How we'll do it: We'll compute (ifact n 1), where 810 811(defun ifact (n a) 812 (if (zp n) 813 a 814 (ifact (- n 1) (* n a)))) 815 816; [2] Write the program. 817 818; Below I show the bytecode program. It is the one generated by 819; our compiler. But I will deal with the bytecode directly, not 820; the source code. 821 822(defconst *ifact-program* 823 ; (compile-stmt-list 824 ; '(n) 825 ; '((a = 1) 826 ; (while (n > 0) 827 ; (a = (n * a)) 828 ; (n = (n - 1))) 829 ; (return a))) 830 831 '((ICONST 1) ;;; 0 832 (ISTORE 1) ;;; 1 (a = 1) 833 (ILOAD 0) ;;; 2 (while ; loop: pc=2 834 (IFLE 10) ;;; 3 (n > 0) 835 (ILOAD 0) ;;; 4 836 (ILOAD 1) ;;; 5 837 (IMUL) ;;; 6 838 (ISTORE 1) ;;; 7 (a = (n * a)) 839 (ILOAD 0) ;;; 8 840 (ICONST 1) ;;; 9 841 (ISUB) ;;; 10 842 (ISTORE 0) ;;; 11 (n = (n - 1)) 843 (GOTO -10) ;;; 12 ) ; jump to loop 844 (ILOAD 1) ;;; 13 845 (HALT) ;;; 14 (return a) 846 )) 847 848; [3] Specify how long it takes to execute (starting with the loop). 849; In particular, define a scheduler function that will 850; run this program to completion. We've already done this: 851 852(defun ifact-loop-sched (n) 853 (if (zp n) 854 (repeat 0 4) 855 (app (repeat 0 11) 856 (ifact-loop-sched (- n 1))))) 857 858(defun ifact-sched (n) 859 (app (repeat 0 2) 860 (ifact-loop-sched n))) 861 862; [4] Test the program and your scheduler. 863 864; We define a little ``test harness'' to let us compute ifact 865; on any natural, using the ifact program. 866 867(defun test-ifact (n) 868 (top 869 (stack 870 (run (ifact-sched n) 871 (make-state 0 872 (cons n (cons 0 nil)) ; n=n, a=0 873 nil 874 *ifact-program*))))) 875 876; Normally we would just try out a few examples, e.g., 877; (test-ifact 5) and expect to see 120 or (! 5). But for 878; posterity I will just write a trivial theorem to prove. 879 880(defthm test-ifact-examples 881 (and (equal (test-ifact 5) (! 5)) 882 (equal (test-ifact 10) (! 10)) 883 (equal (test-ifact 100) (! 100)))) 884 885; Just for the record, (! 100) is quite large; it has 158 decimal 886; digits. This shows that our little m1 machine inherents quite a lot 887; of power from its Lisp description. 888 889; [5] Prove your program does what it does, starting with the loop. 890 891(defthm ifact-loop-lemma 892 (implies (and (natp n) 893 (natp a)) 894 (equal (run (ifact-loop-sched n) 895 (make-state 2 896 (cons n (cons a nil)) 897 stack 898 *ifact-program*)) 899 (make-state 14 900 (cons 0 (cons (ifact n a) nil)) 901 (push (ifact n a) stack) 902 *ifact-program*)))) 903 904(defthm ifact-lemma 905 (implies (natp n) 906 (equal (run (ifact-sched n) 907 (make-state 0 908 (cons n (cons a nil)) 909 stack 910 *ifact-program*)) 911 (make-state 14 912 (cons 0 (cons (ifact n 1) nil)) 913 (push (ifact n 1) stack) 914 *ifact-program*)))) 915 916; We can now disable sched-ifact so that we never run the bytecode 917; again in proofs. 918 919(in-theory (disable ifact-sched)) 920 921; [6] Prove what we do is what we want. 922 923(defthm ifact-is-factorial 924 (implies (and (natp n) 925 (natp a)) 926 (equal (ifact n a) 927 (* (! n) a)))) 928 929; [7] Put it all together. 930 931(defthm ifact-correct 932 (implies (natp n) 933 (equal (run (ifact-sched n) 934 (make-state 0 935 (cons n (cons a nil)) 936 stack 937 *ifact-program*)) 938 (make-state 14 939 (cons 0 (cons (! n) nil)) 940 (push (! n) stack) 941 *ifact-program*)))) 942 943(defthm ifact-correct-corollary-1 944 (implies (natp n) 945 (equal (top 946 (stack 947 (run (ifact-sched n) 948 (make-state 0 949 (cons n (cons a nil)) 950 stack 951 *ifact-program*)))) 952 (! n)))) 953 954; We can make this look like the verification of a high-level program, 955; but of course it is not. We verified the output of the compiler, 956; not the input. 957 958(defthm ifact-correct-corollary-2 959 (implies (natp n) 960 (equal (top 961 (stack 962 (run (ifact-sched n) 963 (make-state 0 964 (cons n (cons a nil)) 965 stack 966 (compile 967 '(n) 968 '((a = 1) 969 (while (n > 0) 970 (a = (n * a)) 971 (n = (n - 1))) 972 (return a))))))) 973 (! n)))) 974 975; =========================================================================== 976 977; Now we develop the macros that make all this more palatable. 978 979; The semantic functions for each instruction return a new state 980; constructed from parts of an old one, s. Typically the new 981; state is just s with one or two components changed. The others 982; are fixed, for that instruction. 983 984; A good example is that of ILOAD: 985 986; (make-state (+ 1 (pc s)) 987; (locals s) 988; (push (nth (arg1 inst) 989; (locals s)) 990; (stack s)) 991; (program s)) 992 993; We can write a macro that allows us to express this as 994; 995; (modify s 996; :stack (push (nth (arg1 inst) 997; (locals s)) 998; (stack s))) 999 1000; The modify expression above expands EXACTLY to the make-state shown 1001; above it. Modify is just an abbreviation for a make-state. But we 1002; only have to write the parts that change in ``unusual'' ways. Since 1003; pc is almost always incremented by one, modify will always produce 1004; (+ 1 (pc s)) in the pc slot of the make-state, unless we supply the 1005; :pc keyword to modify along with the correct new pc. 1006 1007; So here is the modify macro. It generates a make-state. The first 1008; slot is the pc slot, the second is the locals, etc. For each of the 1009; keys :pc, :locals, :stack, and :program, if that key is supplied 1010; among the args to modify, then the make-state has the corresponding 1011; val in that key's slot. Otherwise, that key's slot is occupied by 1012; an expression that computes the value of that slot in state s. The 1013; :pc slot is an exception: the default value is the old value 1014; incremented by one. 1015 1016(defmacro modify (s &rest args) 1017 (list 'make-state 1018 (if (suppliedp :pc args) 1019 (actual :pc args) 1020 (list '+ 1 (list 'pc s))) 1021 (if (suppliedp :locals args) 1022 (actual :locals args) 1023 (list 'locals s)) 1024 (if (suppliedp :stack args) 1025 (actual :stack args) 1026 (list 'stack s)) 1027 (if (suppliedp :program args) 1028 (actual :program args) 1029 (list 'program s)))) 1030 1031(defthm example-modify-1 1032 (equal (modify s :stack (push (arg1 inst) (stack s))) 1033 (make-state (+ 1 (pc s)) 1034 (locals s) 1035 (push (arg1 inst) (stack s)) 1036 (program s))) 1037 :rule-classes nil) 1038 1039(defthm example-modify-2 1040 (equal (modify s 1041 :locals (update-nth (arg1 inst) 1042 (top (stack s)) 1043 (locals s)) 1044 :stack (pop (stack s))) 1045 (make-state 1046 (+ 1 (pc s)) 1047 (update-nth (arg1 inst) 1048 (top (stack s)) 1049 (locals s)) 1050 (pop (stack s)) 1051 (program s))) 1052 :rule-classes nil) 1053 1054(defthm example-modify-3 1055 (equal (modify s :pc (+ (arg1 inst) (pc s))) 1056 (make-state (+ (arg1 inst) (pc s)) 1057 (locals s) 1058 (stack s) 1059 (program s))) 1060 :rule-classes nil) 1061 1062; Because we frequently use such expressions as (arg2 inst) and (stack 1063; s) in the descriptions of new states, it is convenient to introduce 1064; some variables that are bound to those values whenever we are 1065; defining a semantic function. We therefore introduce a special form 1066; of defun to use when defining the semantics of an instruction. 1067 1068(defun pattern-bindings (vars arg-expressions) 1069 (if (endp vars) 1070 nil 1071 (cons (list (car vars) (car arg-expressions)) 1072 (pattern-bindings (cdr vars) (cdr arg-expressions))))) 1073 1074(defmacro semantics (pattern body) 1075 (list 'let (app (pattern-bindings (cdr pattern) 1076 '((arg1 inst) 1077 (arg2 inst) 1078 (arg3 inst))) 1079 '((-pc- (pc s)) 1080 (-locals- (locals s)) 1081 (-stack- (stack s)) 1082 (-program- (program s)))) 1083 body)) 1084 1085; The body might not refer to each of these bound variables. 1086; ACL2 normally causes an error if it sees an unused bound 1087; variable. We must tell it not to worry about that. 1088 1089(acl2::set-ignore-ok t) 1090 1091(defthm example-semantics-1 1092 (equal (semantics 1093 (ICONST c) 1094 (modify s :stack (push c -stack-))) 1095 (make-state 1096 (+ 1 (pc s)) 1097 (locals s) 1098 (push (arg1 inst) (stack s)) 1099 (program s))) 1100 :rule-classes nil) 1101 1102; So in the future, instead of writing 1103 1104; (defun execute-ICONST (inst s) 1105; (make-state (+ 1 (pc s)) 1106; (locals s) 1107; (push (arg1 inst) (stack s)) 1108; (program s))) 1109 1110; we could write 1111 1112; (defun execute-ICONST (inst s) 1113; (semantics (ICONST c) 1114; (modify s :stack (push c -stack-)))) 1115 1116; But in fact, we'll introduce yet another macro so we can just write: 1117 1118; (defsem (ICONST c) 1119; (modify s :stack (push c -stack-))) 1120 1121; and it will 1122; * generate the name execute-ICONST, 1123; * fill in the formals, and 1124; * use the semantics function to generate the body. 1125 1126; So now we define defsem... 1127 1128; The next function is easily understood by example. 1129; (concat-symbols 'EXECUTE- 'ICONST) will return the 1130; symbol EXECUTE-ICONST. 1131 1132; I have not told you how to create symbols because we don't need it -- except 1133; for this one use of going from an instruction opcode to the semantic function 1134; name. Just trust me that this function generates a symbol in the M1 package 1135; whose name is the concatenation of the names of the two parts. 1136 1137(defun concat-symbols (part1 part2) 1138 (intern-in-package-of-symbol 1139 (coerce 1140 (app (coerce (symbol-name part1) 'list) 1141 (coerce (symbol-name part2) 'list)) 1142 'string) 1143 'run)) 1144 1145; This function creates a defun form, with an optional declaration. 1146 1147(defun make-defun (name args dcl body) 1148 (if dcl 1149 (list 'defun name args dcl body) 1150 (list 'defun name args body))) 1151 1152; Thus, (make-defun 'foo '(x) nil '(+ 1 x)) returns 1153 1154; (defun foo (x) (+ 1 x)) 1155 1156; But, (make-defun 'foo '(x y) '(declare (ignore y)) '(+ 1 x)) 1157; returns 1158 1159; (defun foo (x y) (declare (ignore y)) (+ 1 x)) 1160 1161(defmacro defsem (pattern body) 1162 (make-defun (concat-symbols 'execute- (car pattern)) 1163 '(inst s) 1164 (if (equal (len pattern) 1) 1165 '(declare (ignore inst)) 1166 nil) 1167 (list 'semantics pattern body))) 1168 1169