Skip to content

Commit

Permalink
Fix a few broken proofs (rec. eq moves to wordLang)
Browse files Browse the repository at this point in the history 
Progress on #90

Some of proofs are still broken in mysterious ways:
 - bvl_to_bviProof: do_app_adjust, compile_exps_correct
 - clos_to_bvl: Op case of compile_exps_correct
  • Loading branch information
@myreen
myreen committed Nov 20, 2016
1 parent 986e9d1 commit 8bb786c
Show file tree
Hide file tree
Showing 7 changed files with 190 additions and 165 deletions.
2 changes: 1 addition & 1 deletion compiler/backend/proofs/Holmakefile
View file
@@ -1,4 +1,4 @@
INCLUDES = .. ../semantics ../../.. ../../../semantics ../../../semantics/proofs ../../targets ../reg_alloc/proofs ../gc $(HOLDIR)/examples/machine-code/hoare-triple ../../eval ../bignum
INCLUDES = .. ../semantics ../../.. ../../../semantics ../../../semantics/proofs ../../targets ../reg_alloc/proofs ../gc $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/machine-code/multiword ../../eval ../bignum

OPTIONS = QUIT_ON_FAILURE

Expand Down
1 change: 1 addition & 0 deletions compiler/backend/proofs/bvl_constProofScript.sml
View file
Expand Up @@ -125,6 +125,7 @@ val SmartOp_thm = Q.store_thm("SmartOp_thm",
\\ fs [dest_Op_Const_def,evaluate_def,do_app_def] \\ rw []
\\ rfs [] \\ fs [is_simple_thm] \\ rfs [] \\ rw []
\\ fs [dest_Op_Const_def,evaluate_def,do_app_def] \\ rw []
\\ fs [isClos_def] \\ every_case_tac \\ fs []
\\ eq_tac \\ rw []);

val evaluate_env_rel = Q.store_thm("evaluate_env_rel",
Expand Down
45 changes: 37 additions & 8 deletions compiler/backend/proofs/bvl_to_bviProofScript.sml
View file
Expand Up @@ -89,7 +89,7 @@ val bv_ok_def = tDefine "bv_ok" `
val bv_ok_ind = theorem"bv_ok_ind";

val bv_ok_SUBSET_IMP = Q.prove(
`!refs x refs2.
`!(refs:num|->'a) x (refs2:num|->'a).
bv_ok refs x /\ FDOM refs SUBSET FDOM refs2 ==> bv_ok refs2 x`,
HO_MATCH_MP_TAC bv_ok_ind \\ full_simp_tac(srw_ss())[bv_ok_def]
\\ full_simp_tac(srw_ss())[SUBSET_DEF,EVERY_MEM]);
Expand Down Expand Up @@ -144,7 +144,9 @@ val do_app_ok_lemma = Q.prove(
`state_ok r /\ EVERY (bv_ok r.refs) a /\
(do_app op a r = Rval (q,t)) ==>
state_ok t /\ bv_ok t.refs q`,
Cases_on `op` \\ full_simp_tac(srw_ss())[bvlSemTheory.do_app_def] \\ BasicProvers.EVERY_CASE_TAC
`?f. f () = op` by (qexists_tac `K op` \\ fs [])
\\ Cases_on `op` \\ full_simp_tac(srw_ss())[bvlSemTheory.do_app_def]
\\ BasicProvers.EVERY_CASE_TAC
\\ TRY (full_simp_tac(srw_ss())[] \\ SRW_TAC [] [bv_ok_def]
\\ full_simp_tac(srw_ss())[closSemTheory.get_global_def]
\\ full_simp_tac(srw_ss())[state_ok_def,bv_ok_def] \\ NO_TAC)
Expand Down Expand Up @@ -182,19 +184,38 @@ val do_app_ok_lemma = Q.prove(
simp[] >> res_tac >> full_simp_tac(srw_ss())[] >>
simp[SUBSET_DEF])
THEN1 (
simp[bv_ok_def] >>
rename1 `_ () = FromList n`
\\ simp[bv_ok_def] >>
imp_res_tac v_to_list_ok >>
full_simp_tac(srw_ss())[EVERY_MEM])
THEN1
(full_simp_tac(srw_ss())[LET_DEF,state_ok_def]
(rename1 `_ () = Ref`
\\ full_simp_tac(srw_ss())[LET_DEF,state_ok_def]
\\ SRW_TAC [] [bv_ok_def,FLOOKUP_DEF,EVERY_MEM]
\\ BasicProvers.EVERY_CASE_TAC
\\ full_simp_tac(srw_ss())[EVERY_MEM] \\ RES_TAC \\ full_simp_tac(srw_ss())[]
\\ REPEAT STRIP_TAC \\ RES_TAC \\ fs []
THEN1 (match_mp_tac bv_ok_SUBSET_IMP
\\ asm_exists_tac \\ fs [] \\ fs [SUBSET_DEF])
\\ rw [] \\ fs [] \\ fs [FAPPLY_FUPDATE_THM]
\\ every_case_tac \\ fs [] \\ rw [] \\ fs []
\\ first_x_assum (qspec_then `k` mp_tac)
\\ fs [FLOOKUP_DEF] \\ rw [] \\ res_tac
\\ match_mp_tac bv_ok_SUBSET_IMP
\\ asm_exists_tac \\ fs [] \\ fs [SUBSET_DEF])
THEN1
(rename1 `_ () = Ref`
\\ full_simp_tac(srw_ss())[LET_DEF,state_ok_def]
\\ SRW_TAC [] [bv_ok_def,FLOOKUP_DEF,EVERY_MEM]
\\ BasicProvers.EVERY_CASE_TAC
\\ full_simp_tac(srw_ss())[EVERY_MEM] \\ RES_TAC \\ full_simp_tac(srw_ss())[]
\\ REPEAT STRIP_TAC \\ RES_TAC
THEN1 (bv_ok_SUBSET_IMP |> Q.ISPEC_THEN `r.refs`MATCH_MP_TAC
\\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[SUBSET_DEF,FLOOKUP_DEF])
THEN1 (bv_ok_SUBSET_IMP |> Q.ISPEC_THEN `r.refs`MATCH_MP_TAC
\\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[SUBSET_DEF,FLOOKUP_DEF])
THEN1
(`bv_ok r.refs e` by (rw [] \\ fs [])
\\ qpat_x_assum `_::_ = _` kall_tac
\\ match_mp_tac bv_ok_SUBSET_IMP \\ asm_exists_tac \\ fs [SUBSET_DEF])
\\ Q.PAT_X_ASSUM `xx = ValueArray l` MP_TAC
\\ SRW_TAC [] [FAPPLY_FUPDATE_THM] \\ RES_TAC
THEN1 (bv_ok_SUBSET_IMP |> Q.ISPEC_THEN `r.refs`MATCH_MP_TAC
Expand All @@ -204,12 +225,14 @@ val do_app_ok_lemma = Q.prove(
THEN1 (bv_ok_SUBSET_IMP |> Q.ISPEC_THEN `r.refs`MATCH_MP_TAC
\\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[SUBSET_DEF,FLOOKUP_DEF]))
THEN1
(full_simp_tac(srw_ss())[state_ok_def]
(rename1 `_ () = Deref`
\\ full_simp_tac(srw_ss())[state_ok_def]
\\ Q.PAT_X_ASSUM `!k:num. bbb` (MP_TAC o Q.SPEC `n`) \\ full_simp_tac(srw_ss())[]
\\ full_simp_tac(srw_ss())[EVERY_EL] \\ REPEAT STRIP_TAC \\ RES_TAC
\\ SRW_TAC [] [] \\ Cases_on `i` \\ full_simp_tac(srw_ss())[])
THEN1
(full_simp_tac(srw_ss())[state_ok_def] \\ SRW_TAC [] [] THEN1
(rename1 `_ () = Update`
\\ full_simp_tac(srw_ss())[state_ok_def] \\ SRW_TAC [] [] THEN1
(full_simp_tac(srw_ss())[EVERY_MEM] \\ REPEAT STRIP_TAC
\\ BasicProvers.EVERY_CASE_TAC
\\ RES_TAC \\ full_simp_tac(srw_ss())[]
Expand Down Expand Up @@ -601,6 +624,8 @@ val do_app_adjust = Q.prove(
?t3. (do_app op (MAP (adjust_bv b2) (REVERSE a)) t2 =
Rval (adjust_bv b2 q,t3)) /\
state_rel b2 r t3`,
cheat);
(*
SIMP_TAC std_ss [Once bEvalOp_def,iEvalOp_def,do_app_aux_def]
\\ Cases_on `op` \\ full_simp_tac(srw_ss())[]
THEN1 (* Cons *)
Expand Down Expand Up @@ -801,6 +826,7 @@ val do_app_adjust = Q.prove(
\\ full_simp_tac(srw_ss())[bEvalOp_def,adjust_bv_def,bvl_to_bvi_id]
\\ every_case_tac >> full_simp_tac(srw_ss())[bvl_to_bvi_id] >> srw_tac[][]
\\ EVAL_TAC )) |> INST_TYPE[alpha|->``:'ffi``];
*)

val eval_ind_alt = Q.store_thm("eval_ind_alt",
`∀P.
Expand Down Expand Up @@ -892,6 +918,8 @@ val compile_exps_correct = Q.prove(
state_rel b2 s2 t2 /\
(MAP (adjust_bv b1) env = MAP (adjust_bv b2) env) /\
(!a. a IN FDOM s1.refs ==> (b1 a = b2 a))`,
cheat);
(*
SIMP_TAC std_ss []
\\ recInduct eval_ind_alt \\ REPEAT STRIP_TAC
\\ full_simp_tac(srw_ss())[bEval_def,compile_exps_def,iEval_def,bEvery_def,handle_ok_def]
Expand Down Expand Up @@ -1856,6 +1884,7 @@ val compile_exps_correct = Q.prove(
\\ IMP_RES_TAC evaluate_refs_SUBSET \\ full_simp_tac(srw_ss())[SUBSET_DEF]
\\ Cases_on `res` \\ full_simp_tac(srw_ss())[]
\\ Cases_on`e` \\ full_simp_tac(srw_ss())[]));
*)

val _ = save_thm("compile_exps_correct",compile_exps_correct);

Expand Down
6 changes: 3 additions & 3 deletions compiler/backend/proofs/clos_knownProofScript.sml
View file
Expand Up @@ -1245,9 +1245,9 @@ val kvrel_do_eq0 = Q.prove(
fs[] >> simp[do_eq_def] >> rw[] >> fs[LIST_REL_EL_EQN] >> metis_tac[])
>- simp[]
>- (simp[PULL_EXISTS] >> rpt gen_tac >> strip_tac >>
ONCE_REWRITE_TAC [do_eq_def] >> rename1 `do_eq uu1 vv1` >>
Cases_on `do_eq uu1 vv1` >> fs[] >> simp[bool_case_eq] >> dsimp[] >>
rename1 `do_eq uu1 vv1 = Eq_val b` >> Cases_on `b` >> simp[] >>
ONCE_REWRITE_TAC [do_eq_def] >>
Cases_on `do_eq u1 v1` >> fs[] >> simp[bool_case_eq] >> dsimp[] >>
rename1 `do_eq u1 v1 = Eq_val b` >> Cases_on `b` >> simp[] >>
rpt strip_tac >> nailIHx strip_assume_tac >> simp[] >> metis_tac[])
>- (simp[PULL_EXISTS] >> ONCE_REWRITE_TAC[do_eq_def] >> simp[])
>- (simp[PULL_EXISTS] >> ONCE_REWRITE_TAC[do_eq_def] >> simp[]));
Expand Down

0 comments on commit 8bb786c

Please sign in to comment.