Produce smaller cutsets in data_live

Progress on #1042
CakeML · Aug 10, 2024 · 63b46f5 · 63b46f5
1 parent 21c979f
commit 63b46f5
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 27 deletions.
diff --git a/compiler/backend/data_liveScript.sml b/compiler/backend/data_liveScript.sml
@@ -108,8 +108,8 @@ Definition compile_def:
        let l1 = list_insert vs (delete v live) in
          (Assign v op vs NONE,l1)) /\
   (compile (Assign v op vs (SOME names)) live =
-     let l1 = inter names (list_insert vs (delete v live)) in
-       (Assign v op vs (SOME l1),l1)) /\
+     let l1 = inter names (delete v live) in
+       (Assign v op vs (SOME l1),list_insert vs l1)) /\
   (compile (If n c2 c3) live =
      let (d3,l3) = compile c3 live in
      let (d2,l2) = compile c2 live in

diff --git a/compiler/backend/proofs/data_liveProofScript.sml b/compiler/backend/proofs/data_liveProofScript.sml
@@ -144,16 +144,17 @@ val is_pure_do_app_Rval_IMP = Q.prove(
                 ,data_spaceTheory.op_space_req_def,allowed_op_def
                 ,do_stack_def]);
 
-val evaluate_compile = Q.prove(
-  `!c s1 res s2 l2 t1 l1 d.
-      (evaluate (c,s1) = (res,s2)) /\ state_rel s1 t1 l1 /\
-      (compile c l2 = (d,l1)) /\ (res <> SOME (Rerr (Rabort Rtype_error))) /\
-      (!s3. (jump_exc s1 = SOME s3) ==>
-            ?t3. (jump_exc t1 = SOME t3) /\ state_rel s3 t3 LN /\
-                 (t3.handler = s3.handler) /\
-                 (LENGTH t3.stack = LENGTH s3.stack)) ==>
-      ?t2. (evaluate (d,t1) = (res,t2)) /\
-           state_rel s2 t2 (case res of NONE => l2 | _ => LN)`,
+Theorem evaluate_compile[local]:
+  ∀c s1 res s2 l2 t1 l1 d.
+    (evaluate (c,s1) = (res,s2)) /\ state_rel s1 t1 l1 /\
+    (compile c l2 = (d,l1)) /\ (res <> SOME (Rerr (Rabort Rtype_error))) /\
+    (∀s3. (jump_exc s1 = SOME s3) ==>
+          ∃t3. (jump_exc t1 = SOME t3) /\ state_rel s3 t3 LN /\
+               (t3.handler = s3.handler) /\
+               (LENGTH t3.stack = LENGTH s3.stack)) ==>
+    ∃t2. (evaluate (d,t1) = (res,t2)) /\
+         state_rel s2 t2 (case res of NONE => l2 | _ => LN)
+Proof
   ONCE_REWRITE_TAC [EQ_SYM_EQ]
   \\ recInduct evaluate_ind \\ REPEAT STRIP_TAC
   THEN1 (* Skip *)
@@ -164,16 +165,18 @@ val evaluate_compile = Q.prove(
      \\ fs [set_var_def,lookup_insert])
   THEN1 (* Assign *)
     (Cases_on `names_opt` THEN1
-      (fs [compile_def]
-       \\ Cases_on `lookup dest l2 = NONE ∧ is_pure op` \\ fs []
+      (qpat_x_assum ‘(d,l1) = _’ mp_tac
+       \\ fs [compile_def]
+       \\ IF_CASES_TAC
        THEN1
-        (rpt var_eq_tac \\ fs [evaluate_def,cut_state_opt_def]
+        (strip_tac \\ fs []
+         \\ rpt var_eq_tac \\ fs [evaluate_def,cut_state_opt_def]
          \\ every_case_tac \\ fs [] \\ rpt var_eq_tac
          \\ imp_res_tac is_pure_do_app_Rerr_IMP \\ fs []
          \\ imp_res_tac is_pure_do_app_Rval_IMP \\ fs [] \\ rpt var_eq_tac
          \\ fs [state_rel_def,set_var_def,lookup_insert,domain_lookup] \\ rw [])
-       \\ fs [] \\ pop_assum kall_tac \\ rpt var_eq_tac
-       \\ fs [evaluate_def,get_var_def,LET_DEF]
+       \\ pop_assum kall_tac \\ fs [] \\ strip_tac \\ rpt var_eq_tac
+       \\ fs [evaluate_def,get_var_def,LET_DEF,cut_state_opt_def]
        \\ every_case_tac >> fs[] \\ SRW_TAC [] []
        \\ fs [compile_def,LET_DEF,evaluate_def,cut_state_opt_def] \\ rw[]
        \\ qmatch_assum_rename_tac`get_vars args _ = SOME xx`
@@ -187,17 +190,17 @@ val evaluate_compile = Q.prove(
      \\ every_case_tac >> fs[] \\ SRW_TAC [] []
      \\ fs [compile_def,LET_DEF,evaluate_def,cut_state_opt_def]
      \\ Q.MATCH_ASSUM_RENAME_TAC `do_app op vs t = _`
-     \\ Cases_on `domain x SUBSET domain s.locals` \\ fs []
+     \\ Cases_on `domain (list_insert args x) SUBSET domain s.locals` \\ fs []
      \\ fs [cut_state_def,cut_env_def]
-     \\ (`domain (inter x (list_insert args (delete dest l2))) SUBSET
-         domain t1.locals` by
+     \\ Cases_on ‘domain x ⊆ domain r.locals’ \\ gvs []
+     \\ (`domain (list_insert args (inter x (delete dest l2))) ⊆
+                 domain t1.locals` by
       (fs [domain_inter,domain_list_insert,SUBSET_DEF,state_rel_def]
        \\ RES_TAC \\ fs [domain_lookup]
        \\ fs [PULL_EXISTS,oneTheory.one] \\ RES_TAC \\ METIS_TAC []))
      \\ fs [] \\ SRW_TAC [] []
-     \\ Q.ABBREV_TAC `t4 = mk_wf (inter t1.locals
-                (inter x (list_insert args (delete dest l2))))`
-     \\ `state_rel (s with locals := mk_wf (inter s.locals x))
+     \\ Q.ABBREV_TAC `t4 = (inter t1.locals (list_insert args (inter x (delete dest l2))))`
+     \\ `state_rel (s with locals := mk_wf (inter s.locals (list_insert args x)))
         (t1 with locals := t4) LN` by (fs [state_rel_def] \\ NO_TAC)
      \\ `get_vars args t4 = SOME vs` by
       (UNABBREV_ALL_TAC
@@ -209,12 +212,13 @@ val evaluate_compile = Q.prove(
        \\ fs [domain_inter,domain_list_insert] \\ NO_TAC)
      \\ fs [] \\ IMP_RES_TAC state_rel_IMP_do_app
      \\ fs [] \\ IMP_RES_TAC state_rel_IMP_do_app_err
-     \\ fs [state_rel_def,set_var_def,lookup_insert]
+     \\ ‘domain x ∩ (domain l2 DELETE dest) ⊆ domain t4’ by
+       (gvs [Abbr‘t4’,SUBSET_DEF,sptreeTheory.domain_list_insert])
+     \\ fs [] \\ fs [state_rel_def,set_var_def,lookup_insert]
      \\ REPEAT STRIP_TAC \\ SRW_TAC [] [call_env_def,flush_state_def]
      \\ fs [domain_inter,domain_list_insert,domain_delete]
      \\ UNABBREV_ALL_TAC
-     \\ IMP_RES_TAC do_app_const
-     \\ fs []
+     \\ IMP_RES_TAC do_app_const \\ fs []
      \\ fs [lookup_inter_alt,domain_inter,domain_list_insert,domain_delete])
   THEN1 (* Tick *)
     (fs [evaluate_def,compile_def,state_rel_def] \\ SRW_TAC [] []
@@ -652,7 +656,8 @@ val evaluate_compile = Q.prove(
   \\ SRW_TAC [] [] \\ fs []
   \\ Cases_on `LASTN (t1.handler + 1) t1.stack` \\ fs []
   \\ Cases_on `h` \\ fs []
-  \\ SRW_TAC [] [] \\ fs []);
+  \\ SRW_TAC [] [] \\ fs []
+QED
 
 Theorem compile_correct:
    !c s. FST (evaluate (c,s)) <> SOME (Rerr(Rabort Rtype_error)) /\