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.
% 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))))))))))))