Add some simple proofs

[calin1304]

Added some claims I came up with as an exercise

1. For any X, Y equal integers, X - Y = 0.
2. For any X, Y integers, maximum of X and Y is greater than or equal to X and to Y
3. The sum of even integers is even.

[ehildenb]

This isn't true. Consider the definition of #signed (in data.md)

    rule #signed(ITYPE, N) => N                  requires 0            <=Int N andBool N <Int #pow1(ITYPE) 
    rule #signed(ITYPE, N) => N -Int #pow(ITYPE) requires #pow1(ITYPE) <=Int N andBool N <Int #pow (ITYPE) 

So if we have that notBool (0 <=Int X -Int Y andBool X - Int Y <Int #pow1(ITYPE)), and we also have that #pow1(ITYPE) <=Int X -Int Y andBool X -Int Y <Int #pow(ITYPE), we should be returning (X -Int Y) -Int #pow(ITYPE), but your simplification rule returns X -Int Y.

[ehildenb]

You can add a requires clause to your second rule which says 0 <=Int X -Int Y andBool X -Int Y <Int #pow1(ITYPE), but that would be saying the same thing as the original rule in the semantics.

So instead, we should make it so the prover can know that 0 <=Int X -Int Y andBool X -Int Y <Int #pow1(ITYPE) is true. Which proof is this lemma needed for?

[ehildenb]

Write a functional spec:

claim <instrs> run(#signed(ITYPE, X -Int Y)) => done(X -Int Y) ... </k> requires #inUnsignedRange(ITYPE, X -Int Y)

[ehildenb]

Suggested change

	requires
	#inUnsignedRange(ITYPE, X) andBool
	#inUnsignedRange(ITYPE, Y)
	requires #inUnsignedRange(ITYPE, X)
	andBool #inUnsignedRange(ITYPE, Y)

[ehildenb]

For #signed(ITYPE, 0), it probably can't tell that 0 <Int #pow1(ITYPE), even though ITYPE can only be i32 or i64.

rule 0 <Int #pow1(_) => true [simplification]

and see if this works on Ana's branch.

Make sure to check the defniition of #pow1 and make sure this is true.