# M1 Programming and Proof Challenges

Template.lisp is an annotated ACL2 script for verifying the total correctness of `*g-program*` as a multiplier. Use it to verify the following M1 programs.

## Sum

Define an M1 program to sum the natural numbers from `n` down to `0`. You may assume `n` is a natural number. Prove that the result is
`(/ (* n (+ n 1)) 2)`.

## Sum of Squares

Define an M1 program to sum the squares of the natural numbers from `n` down to `0`. You may assume `n` is a natural number. Prove that the result is
`(+ (/ (expt n 3) 3) (/ (expt n 2) 2) (/ n 6))`.

## Factorial

Define an M1 program to compute the factorial of the natural number `n`. (You will have to define factorial; it is not native in ACL2.)

## Fibonacci

Define an M1 program to compute the Fibonacci function on its natural number input. Prove your program correct.

```Fib(0) = 0
Fib(1) = 1
Fib(2) = Fib(1)+Fib(0)
Fib(3) = Fib(2)+Fib(1)
...
```

Advice: M1 does not have recursion or method call, so you have to do this iteratively. When you verify your helper function you will have to think of the generalization that characterizes its output for all legal inputs, not just the initial case. When you verify your loop code you'll have to specify the final values of all of the locals you're using. You could try to figure out the closed form expressions for the locals. But a simpler approach is to define `fib-locals` to just return the list of the final values of all the locals, computed exactly the way your code does it.

## Even

Define an M1 program that determines if its argument, `n`, is even or odd. You may assume `n` is a natural number. To indicate that `n` is even, leave `1` on the stack. Otherwise, leave `0` on the stack.

Advice: A convenient expression of the idea ```n` is even'' in ACL2 is the expression
`(equal (mod n 2) 0)`.
When `n` is a natural number, `(equal (mod n 2) 0)` is `t` if `n` is even and is `nil` if `n` is odd.

## Sign

Define an M1 program to determine the sign of an integer `n`. You may assume that `n` is an integer. To indicate that `n` is negative, leave `-1` on the stack; to indicate that `n` is zero, leave `0` on the stack; to indicate that `n` is positive, leave `+1` on the stack. Prove that your program is correct.

## Division

Define an M1 program to compute the natural number quotient (i.e., the floor) of `n` divided by `d`, where `n` and `d` are natural numbers and `d` is not `0`. Prove that your program is correct.

Advice: In ACL2, the floor of `n` divided by `d` is `(floor n d)`. For example, `(floor 27 6)` is `4`.

Warning: This program will require nested loops and hence is not strictly in the template you've been using. But perhaps you can figure it out.