PVS dump file compiler.dmp
To extract the specifications and proofs, download this file to
compiler.dmp and from a running PVS type the command
M-x undump-pvs-files
You will be prompted for the dump file name (compiler.dmp) and the
directory in which to dump the extracted files.
<![CDATA[
% Patch files loaded: ("patch03" "patch02" "patch01" "patch")
$$$compiler.pvs
list_aux[t: TYPE]: THEORY
BEGIN
append(l1,l2: list[t]): RECURSIVE list[t] =
CASES l1 OF
null: l2,
cons(hd, tl): cons(hd, append(tl, l2))
ENDCASES
MEASURE (LAMBDA (l1,l2: list[t]): length(l1))
END list_aux
compiler: THEORY
BEGIN USING list_aux
%--------- TERMS (of both source and target languages) ----------------
variable: TYPE
arb: variable % where needed?
term: DATATYPE
BEGIN
mk_var(var_val: variable): is_var?
mk_const(const_val: int): is_const?
END term
env: TYPE = [variable -> int]
term_value(t: term, e: env): int =
CASES t OF
mk_var(v): e(v),
mk_const(i): i
ENDCASES
%--------- SOURCE LANGUAGE --------------------------------------------
% cf s-var, s-var-list
crude_source_stmt: TYPE = [# lhs: variable, rhs: list[term] #]
% cf. exclusive-varp and exclusive-var-listp, legal-source-statement,
% legal-source-program
good_source_stmt?(s: crude_source_stmt): bool =
every((LAMBDA (t: term): is_var?(t) => var_val(t) /= lhs(s)), rhs(s))
AND NOT null?(rhs(s))
source_stmt: TYPE = (good_source_stmt?)
source_prog: TYPE = list[source_stmt]
% cf. compute-value
source_rhs_val(l: list[term], e: env): RECURSIVE int =
CASES l OF
null: 0,
cons(t, expr): source_rhs_val(expr, e) + term_value(t, e)
ENDCASES
MEASURE (LAMBDA (l: list[term]), (e: env): length(l))
% cf. interpret-source does both the following
source_stmt_interp(s: source_stmt, e: env): env =
e WITH [(lhs(s)) := source_rhs_val(rhs(s), e)]
source_interpreter(p: source_prog, e: env): RECURSIVE env =
CASES p OF
null: e,
cons(stmt, rest): source_interpreter(rest, source_stmt_interp(stmt, e))
ENDCASES
MEASURE (LAMBDA (p:source_prog), (e:env) : length(p))
%--------- TARGET LANGUAGE --------------------------------------------
opcode: TYPE = {LOAD, ADD}
% cf s-cvar, s-const, s-avar, s-addend, form1-stmtp and form2-stmtp,
% legal-target-statement
target_instr: TYPE = [# op: opcode, dest: variable, src: term #]
% cf. compute-target-rhs, single-step
target_instr_interp(i:target_instr, e: env): env =
e WITH [(dest(i)) := CASES op(i) OF
LOAD: term_value(src(i), e),
ADD: e(dest(i)) + term_value(src(i), e)
ENDCASES]
% cf. legal-target-program
target_prog: TYPE = list[target_instr]
% cf. interpret-target
target_interpreter(t:target_prog, e: env): RECURSIVE env =
CASES t OF
null: e,
cons(instr, rest): target_interpreter(rest, target_instr_interp(instr, e))
ENDCASES
MEASURE (LAMBDA (t:target_prog), (e:env): length(t))
%------- COMPILER ----------------------------------------------------
% cf. generate-add-assigns
generate_adds(target: variable, l: list[term]): RECURSIVE target_prog =
CASES l OF
null: null,
cons(t, rest): cons( (# op := ADD, dest := target, src := t #),
generate_adds(target, rest))
ENDCASES
MEASURE (LAMBDA (target: variable), (l: list[term]): length(l))
% cf. compile statement
compile_stmt(s: source_stmt): target_prog =
cons( (# op := LOAD, dest := lhs(s), src := mk_const(0) #),
generate_adds(lhs(s), rhs(s)))
% cf. compile
compiler(sp: source_prog): RECURSIVE target_prog =
CASES sp OF
null: null,
cons(hd, tl): append(compile_stmt(hd), compiler(tl))
ENDCASES
MEASURE length
%------- VERIFICATION -----------------------------------------------
prior_value_irrelevant_aux: LEMMA FORALL (v:variable), (l: list[term]), (e: env), (x:int):
LET s = (# lhs := v, rhs := l #) IN
good_source_stmt?(s) =>
source_rhs_val(l, e) = source_rhs_val(l, e with [(v) := x])
prior_value_irrelevant: LEMMA FORALL (s: source_stmt), (e: env), (x:int):
source_rhs_val(rhs(s), e) = source_rhs_val(rhs(s), e WITH [(lhs(s)) := x])
single_dest?(dest: variable, tp: target_prog): bool =
NOT null?(tp) AND every((LAMBDA (i: target_instr): dest(i)=dest), tp)
independence: LEMMA FORALL (dest, v:variable), (t:target_prog), (e: env):
single_dest?(dest, t) and dest/=v => target_interpreter(t, e)(v) = e(v)
good_compile_aux: LEMMA (FORALL (dest:variable), (expr:list[term]):
LET s = (# lhs := dest, rhs := expr #) IN
good_source_stmt?(s) => single_dest?(dest, compile_stmt(s)))
good_compile: LEMMA (FORALL (s: source_stmt):
single_dest?(lhs(s), compile_stmt(s)))
correct_expr_aux: LEMMA FORALL (v:variable), (l: list[term]), (e:env) :
good_source_stmt?((# lhs := v, rhs := l #)) =>
source_rhs_val(l,e) + e(v) =
target_interpreter(generate_adds(v, l), e)(v)
correct_expr: LEMMA FORALL (s:source_stmt), (e:env) :
source_rhs_val(rhs(s),e) + e(lhs(s)) =
target_interpreter(generate_adds(lhs(s), rhs(s)), e)(lhs(s))
% cf. target-step1 but not really the same, 'cos they don't have
% something sorresponding exactly to source_stmt_interp
correct_step: LEMMA FORALL (s: source_stmt), (e:env) :
source_stmt_interp(s,e) = target_interpreter(compile_stmt(s), e)
% cf. interpret-target-decomposition
target_append: LEMMA FORALL (t1,t2:list[target_instr]), (e: env):
target_interpreter(append(t1, t2), e) = target_interpreter(t2, target_interpreter(t1, e))
% cf. main-correctness-theorem
correctness: THEOREM FORALL (sp:source_prog), (e:env):
source_interpreter(sp, e) = target_interpreter(compiler(sp), e)
% nothing corresponding to the stuff on p135--137
END compiler
$$$compiler.prf
(|list_aux| (|append_TCC2| "" (APPLY (THEN* (TCC) (REPLACE*) (TCC))) NIL))(|compiler| (|source_prog_TCC1| "" (TCC) (("" (TCC) (("" (INST 1 "(# lhs:= arb, rhs:=cons[term](mk_const(0),null) #)") (("" (ASSERT) (("" (PROPAX) NIL))))))))) (|source_rhs_val_TCC1| "" (TERM-TCC) NIL) (|source_interpreter_TCC1| "" (TCC) (("" (REPLACE*) (("" (TCC) NIL))))) (|target_interpreter_TCC1| "" (SKOLEM!) (("" (FLATTEN) (("" (REPLACE -1) (("" (EXPAND "length" 1 2) (("" (ASSERT) NIL))))))))) (|generate_adds_TCC1| "" (SKOLEM!) (("" (FLATTEN) (("" (REPLACE -1) (("" (EXPAND "length" 1 2) (("" (ASSERT) NIL))))))))) (|compiler_TCC1| "" (SKOLEM!) (("" (FLATTEN) (("" (REPLACE -1) (("" (EXPAND "length" 1 2) (("" (ASSERT) NIL))))))))) (|prior_value_irrelevant_aux| "" (APPLY (INDUCT-AND-REWRITE-DEFS! "l" 1 "term_value")) NIL) (|prior_value_irrelevant| "" (SKOSIMP) (("" (USE "prior_value_irrelevant_aux") (("" (ASSERT) (("" (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1") (("" (ASSERT) NIL))))))))) (|independence| "" (APPLY (INDUCT-AND-REWRITE-DEFS "t" 1)) NIL) (|good_compile_aux| "" (APPLY (INDUCT-AND-REWRITE-DEFS "expr" 1)) NIL) (|good_compile| "" (SKOSIMP) (("" (USE "good_compile_aux" ("expr" "rhs(s!1)")) (("" (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1") (("" (ASSERT) (("" (PROPAX) NIL))))))))) (|correct_expr_aux| "" (INDUCT "l" 1) (("1" (TCC) NIL) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE-THEORY "compiler") (("2" (ASSERT) (("2" (INST -1 "v!1" "e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)]") (("2" (PROP) (("1" (REPLACE -1 :DIR RL) (("1" (DELETE -1) (("1" (ASSERT) (("1" (LEMMA "prior_value_irrelevant") (("1" (INST -1 "(# lhs := v!1, rhs := cons2_var!1 #)" _ _) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (TCC) NIL))))))))))) ("2" (TCC) NIL) ("3" (TCC) NIL))))))))))))) (|correct_expr| "" (SKOSIMP) (("" (USE "correct_expr_aux") (("" (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1") (("" (ASSERT) (("" (PROPAX) NIL))))))))) (|correct_step| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY) (("" (DELETE 2) (("" (CASE-REPLACE "x!1=lhs(s!1)") (("1" (TCC) (("1" (REWRITE "prior_value_irrelevant" :SUBST ("x" 0)) (("1" (USE "correct_expr") (("1" (ASSERT) NIL))))))) ("2" (EXPAND "source_stmt_interp") (("2" (USE "independence") (("2" (USE "good_compile") (("2" (INST?) (("2" (ASSERT) (("2" (PROPAX) NIL))))))))))))))))))) (|target_append| "" (APPLY (INDUCT-AND-REWRITE-DEFS "t1" 1)) NIL) (|correctness| "" (APPLY (INDUCT-AND-REWRITE-DEFS "sp" 1 "target_append" "correct_step")) NIL) (|good_pieces| "" (AUTO-REWRITE "compiler.good_source_stmt?" "notequal./=" "list_props.every" "list_props.length") (("" (AUTO-REWRITE) (("" (INDUCT "l" 1) (("1" (SKOSIMP*) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (APPLY (THEN* (INST?) (LIFT-IF) (PROP) (SKOSIMP*)) "~%Applying instantiation, if-lifting, propositional
simplification, and skolemization,") NIL))))))))))))
]]>