(*<*)
theory ex06
imports Small_Step Big_Step
begin
(*>*)
text {* \ExerciseSheet{6}{25.~11.~2011} *}
text {* \Exercise{Small step equivalence}
We define an equivalence relation @{text "\"} on programs that uses
the small-step semantics. Unlike with @{text "\"}, we also demand that
the programs take the same number of steps.
The following relation is the n-steps reduction relation:
*}
inductive
n_steps :: "com * state \ nat \ com * state \ bool"
("_ \^_ _" [60,1000,60]999)
where
zero_steps: "cs \^0 cs" |
one_step: "cs \ cs' \ cs' \^n cs'' \ cs \^(Suc n) cs''"
(*<*)
inductive_cases zero_stepsE[elim!]: "cs \^0 cs'"
thm zero_stepsE
inductive_cases one_stepE[elim!]: "cs \^(Suc n) cs''"
thm one_stepE
(*>*)
text {* Prove the following lemmas: *}
lemma small_steps_n: "cs \* cs' \ (\n. cs \^n cs')"
(*<*)
by (induct rule: star.induct) (auto intro: n_steps.intros)
(*>*)
lemma n_small_steps: "cs \^n cs' \ cs \* cs'"
(*<*)
apply (induct n arbitrary: cs)
apply (auto intro: Star.step)
done
(*>*)
text {* The equivalence relation is defined as follows: *}
definition
small_step_equiv :: "com \ com \ bool" (infix "\" 50) where
"c \ c' == (\s t n. (c,s) \^n (SKIP, t) = (c', s) \^n (SKIP, t))"
text {* Prove the following lemma: *}
lemma small_eqv_implies_big_eqv: "c \ c' \ c \ c'"
(*<*)
proof -
assume seqv: "c \ c'"
show "c \ c'"
proof (intro allI iffI)
fix s t
assume "(c, s) \ t"
then have "(c, s) \* (SKIP, t)" by (rule big_to_small)
with small_steps_n
obtain n where "(c, s) \^n (SKIP, t)" by blast
with seqv have "(c', s) \^n (SKIP, t)"
by (auto simp: small_step_equiv_def)
then have "(c', s) \* (SKIP, t)"
by (rule n_small_steps)
thus "(c', s) \ t" by (rule small_to_big)
next (* ugly duplication -- could be avoided, but using equivalence
reasoning, but we dont care for now *)
fix s t
assume "(c', s) \ t"
then have "(c', s) \* (SKIP, t)" by (rule big_to_small)
with small_steps_n
obtain n where "(c', s) \^n (SKIP, t)" by blast
with seqv have "(c, s) \^n (SKIP, t)"
by (auto simp: small_step_equiv_def)
then have "(c, s) \* (SKIP, t)"
by (rule n_small_steps)
thus "(c, s) \ t" by (rule small_to_big)
qed
qed
(*>*)
text {* How about the reverse implication? *}
(*<*)
lemma "\ SKIP \ (SKIP; SKIP)"
unfolding small_step_equiv_def
by (metis Semi1 SkipE zero_steps zero_stepsE)
(*>*)
text {* \Exercise{A different instruction set architecture}
We consider a different instruction set which evaluates
boolean expressions on the stack, similar to arithmetic expressions:
\begin{itemize}
\item
The boolean value @{term False} is represented by the number @{text 0},
the boolean value @{term True} is represented by any number not equal
to @{text 0}.
\item
For every boolean operation exists a corresponding instruction which,
similar to arithmetic instructions, operates on values on top of the
stack.
\item
The new instruction set introduces a conditional jump which pops the
top-most element from the stack and jumps over a given amount of
instructions, if the popped value corresponds to @{text False}, and
otherwise goes to the next instruction.
\end{itemize}
Modify the theory @{text Compiler} by defining a suitable set of
instructions, by adapting the execution model and the compiler and
by updating the correctness proof.
*}
text {* Solution based on a slightly outdated version, so **modification**
annotations may not be accurate! *}
subsection "Instructions and Stack Machine"
datatype instr =
PUSH_N int | PUSH_V vname | ADD |
STORE vname |
JMPF nat |
JMPB nat |
(*** BEGIN MODIFICATION ***)
(*** dropped unnecessary jump instructions, and added these instructions: *)
PUSH_B bool | NOT | AND | LESS |
JMP0 nat
(*** END MODIFICATION ***)
types stack = "int list"
config = "nat\state\stack"
abbreviation "hd2 xs == hd(tl xs)"
abbreviation "tl2 xs == tl(tl xs)"
inductive exec1 :: "instr list \ config \ config \ bool"
("(_/ \ (_ \/ _))" [50,0,0] 50)
for P :: "instr list"
where
"\ i < size P; P!i = PUSH_N n \ \
P \ (i,s,stk) \ (i+1,s, n#stk)" |
"\ i < size P; P!i = PUSH_V x \ \
P \ (i,s,stk) \ (i+1,s, s x # stk)" |
"\ i < size P; P!i = ADD \ \
P \ (i,s,stk) \ (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
"\ i < size P; P!i = STORE n \ \
P \ (i,s,stk) \ (i+1,s(n := hd stk),tl stk)" |
"\ i < size P; P!i = JMPF n \ \
P \ (i,s,stk) \ (i+1+n,s,stk)" |
"\ i < size P; P!i = JMPB n; n \ i+1 \ \
P \ (i,s,stk) \ (i+1-n,s,stk)" |
(*** BEGIN MODIFICATION ***)
"\ i < size P; P!i = PUSH_B b \ \
P \ (i,s,stk) \ (i+1,s, (if b then 1 else 0)#stk)" |
"\ i < size P; P!i = NOT \ \
P \ (i,s,stk) \ (i+1,s, (if hd stk \ 0 then 0 else 1) # tl stk)" |
"\ i < size P; P!i = AND \ \
P \ (i,s,stk) \ (i+1,s, (if hd2 stk \ 0 then if hd stk \ 0 then 1 else 0 else 0) # tl2 stk)" |
"\ i < size P; P!i = LESS \ \
P \ (i,s,stk) \ (i+1,s, (if hd2 stk < hd stk then 1 else 0) # tl2 stk)" |
"\ i < size P; P!i = JMP0 n \ \
P \ (i,s,stk) \ (if hd stk > 0 then i+1 else i+1+n,s,tl stk)"
(*** END MODIFICATION ***)
code_pred exec1 .
declare exec1.intros[intro]
inductive exec :: "instr list \ config \ config \ bool" ("_/ \ (_ \*/ _)" 50)
where
refl: "P \ c \* c" |
step: "P \ c \ c' \ P \ c' \* c'' \ P \ c \* c''"
declare exec.intros[intro]
lemmas exec_induct = exec.induct[split_format(complete)]
code_pred exec .
subsection{* Verification infrastructure *}
lemma exec_trans: "P \ c \* c' \ P \ c' \* c'' \ P \ c \* c''"
apply(induct rule: exec.induct)
apply blast
by (metis exec.step)
lemma exec1_subst: "P \ c \ c' \ c' = c'' \ P \ c \ c''"
by auto
lemmas exec1_simps = exec1.intros[THEN exec1_subst]
text{* Below we need to argue about the execution of code that is embedded in
larger programs. For this purpose we show that execution is preserved by
appending code to the left or right of a program. *}
lemma exec1_appendR: assumes "P \ c \ c'" shows "P@P' \ c \ c'"
proof-
from assms show ?thesis
by cases (simp_all add: exec1_simps nth_append)
-- "All cases proved with the final simp-all"
qed
lemma exec_appendR: "P \ c \* c' \ P@P' \ c \* c'"
apply(induct rule: exec.induct)
apply blast
by (metis exec1_appendR exec.step)
lemma exec1_appendL:
assumes "P \ (i,s,stk) \ (i',s',stk')"
shows "P' @ P \ (size(P')+i,s,stk) \ (size(P')+i',s',stk')"
proof-
from assms show ?thesis
by cases (simp_all add: exec1_simps)
qed
lemma exec_appendL:
"P \ (i,s,stk) \* (i',s',stk') \
P' @ P \ (size(P')+i,s,stk) \* (size(P')+i',s',stk')"
apply(induct rule: exec_induct)
apply blast
by (blast intro: exec1_appendL exec.step)
text{* Now we specialise the above lemmas to enable automatic proofs of
@{prop "P \ c \* c'"} where @{text P} is a mixture of concrete instructions and
pieces of code that we already know how they execute (by induction), combined
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
The details should be skipped on a first reading.
If the pc points beyond the first instruction or part of the program, drop it: *}
lemma exec_Cons_Suc[intro]:
"P \ (i,s,stk) \* (j,t,stk') \
instr#P \ (Suc i,s,stk) \* (Suc j,t,stk')"
apply(drule exec_appendL[where P'="[instr]"])
apply simp
done
lemma exec_appendL_if[intro]:
"size P' <= i
\ P \ (i - size P',s,stk) \* (i',s',stk')
\ P' @ P \ (i,s,stk) \* (size P' + i',s',stk')"
apply(drule exec_appendL[where P'=P'])
apply simp
done
text{* Split the execution of a compound program up into the excution of its
parts: *}
lemma exec_append_trans[intro]:
"P \ (0,s,stk) \* (i',s',stk') \
size P \ i' \
P' \ (i' - size P,s',stk') \* (i'',s'',stk'') \
j'' = size P + i''
\
P @ P' \ (0,s,stk) \* (j'',s'',stk'')"
by(metis exec_trans[OF exec_appendR exec_appendL_if])
declare Let_def[simp] (*nat_number[simp]*)
subsection "Compilation"
fun acomp :: "aexp \ instr list" where
"acomp (N n) = [PUSH_N n]" |
"acomp (V n) = [PUSH_V n]" |
"acomp (Plus a\<^isub>1 a\<^isub>2) = acomp a\<^isub>1 @ acomp a\<^isub>2 @ [ADD]"
lemma acomp_correct[intro]:
"acomp a \ (0,s,stk) \* (size(acomp a),s,aval a s#stk)"
apply(induct a arbitrary: stk)
apply(fastsimp)+
done
(*** BEGIN MODIFICATION ***)
(*** dropped 2nd and 3rd argument from bcomp (requires further changes at
*** all occurrences of bcomp),
*** translate boolean expression into new instructions *)
fun bcomp :: "bexp \ instr list" where
"bcomp (Bc v) = [PUSH_B v]" |
"bcomp (Not b) = bcomp b @ [NOT]" |
"bcomp (And b\<^isub>1 b\<^isub>2) = bcomp b\<^isub>1 @ bcomp b\<^isub>2 @ [AND]" |
"bcomp (Less a\<^isub>1 a\<^isub>2) = acomp a\<^isub>1 @ acomp a\<^isub>2 @ [LESS]"
(*** END MODIFICATION ***)
value "bcomp (And (Less (V ''0'') (V ''1'')) (Not(Less (V ''2'') (V ''3''))))"
(*** BEGIN MODIFICATION ***)
(*** completely rewrote the proof from scratch *)
lemma bcomp_correct[intro]:
"bcomp b \ (0,s,stk) \* (size(bcomp b),s,(if bval b s then 1 else 0) # stk)"
by (induct b arbitrary: stk) fastsimp+
(*** END MODIFICATION ***)
(*** BEGIN MODIFICATION ***)
(*** added additional jumps in compilation of IF and WHILE,
*** replaced backjump offset (in WHILE) with "2" (used to be "1") *)
fun ccomp :: "com \ instr list" where
"ccomp SKIP = []" |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b
in cb @ [JMP0 (size cc\<^isub>1 + 1)] @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
"ccomp (WHILE b DO c) =
(let cc = ccomp c; cb = bcomp b
in cb @ [JMP0 (size cc + 1)] @ cc @ [JMPB (size cb + size cc + 2)])"
(*** END MODIFICATION ***)
value "ccomp (IF Less (V ''4'') (N 1) THEN ''4'' ::= Plus (V ''4'') (N 1) ELSE ''3'' ::= V ''4'')"
value "ccomp (WHILE Less (V ''4'') (N 1) DO (''4'' ::= Plus (V ''4'') (N 1)))"
subsection "Preservation of sematics"
lemma ccomp_correct:
"(c,s) \ t \ ccomp c \ (0,s,stk) \* (size(ccomp c),t,stk)"
proof(induct arbitrary: stk rule: big_step_induct)
case (Assign x a s)
show ?case by (fastsimp simp:fun_upd_def)
next
case (Semi c1 s1 s2 c2 s3)
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
have "?cc1 @ ?cc2 \ (0,s1,stk) \* (size ?cc1,s2,stk)"
using Semi.hyps(2) by (fastsimp)
moreover
have "?cc1 @ ?cc2 \ (size ?cc1,s2,stk) \* (size(?cc1 @ ?cc2),s3,stk)"
using Semi.hyps(4) by (fastsimp)
ultimately show ?case by simp (blast intro: exec_trans)
next
case (WhileTrue b s1 c s2 s3)
let ?cc = "ccomp c"
let ?cb = "bcomp b"
let ?cw = "ccomp(WHILE b DO c)"
(*** BEGIN MODIFICATION ***)
(*** added "+ 1" on the right-hand side *)
have "?cw \ (0,s1,stk) \* (size ?cb + size ?cc + 1,s2,stk)"
(*** END MODIFICATION ***)
using WhileTrue(1,3) by fastsimp
moreover
(*** BEGIN MODIFICATION ***)
(*** added "+ 1" on the right-hand side,
*** added simplification rule nth_append to fastsimp *)
have "?cw \ (size ?cb + size ?cc + 1,s2,stk) \* (0,s2,stk)"
by (fastsimp simp add: nth_append)
(*** END MODIFICATION ***)
moreover
have "?cw \ (0,s2,stk) \* (size ?cw,s3,stk)" by(rule WhileTrue(5))
ultimately show ?case by(blast intro: exec_trans)
qed fastsimp+
subsection "Nontermination"
definition machine_div :: "instr list \ config \ bool" (infix "\" 55) where
"P \ c = (\ C. C 0 = c \ (\i. P \ C i \ C(Suc i)))"
(*<*)
end
(*>*)