Merge pull request #804 from CakeML/currheap

Improved use of CurrHeap

compiler/backend/backendComputeLib.sml

@@ -631,6 +631,7 @@ val add_backend_compset = computeLib.extend_compset
       (* ---- wordLang inst_select and inst flattening ---- *)
     ,word_instTheory.three_to_two_reg_def
     ,word_instTheory.pull_exp_def
+    ,word_instTheory.is_Lookup_CurrHeap_def
     ,word_instTheory.inst_select_def
     ,word_instTheory.inst_select_exp_def
     ,word_instTheory.flatten_exp_def

compiler/backend/data_to_wordScript.sml

@@ -110,13 +110,13 @@ val ptr_bits_def = Define `
 val real_addr_def = Define `
   (real_addr (conf:data_to_word$config) r): 'a wordLang$exp =
     let k = shift (:'a) in
-      if k <= conf.pad_bits + 1 then
-        Op Add [Lookup CurrHeap;
-                Shift Lsr (Var r) (shift_length conf - k)]
+    let l = shift_length conf in
+      if k = l ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0 then
+        Op Add [Lookup CurrHeap; Op Sub [Var r; Const 1w]]
+      else if k <= conf.pad_bits + 1 then
+        Op Add [Lookup CurrHeap; Shift Lsr (Var r) (l - k)]
       else
-        Op Add [Lookup CurrHeap;
-                Shift Lsl (Shift Lsr (Var r)
-                  (shift_length conf)) k]`
+        Op Add [Lookup CurrHeap; Shift Lsl (Shift Lsr (Var r) l) k]`
 
 val real_offset_def = Define `
   (real_offset (conf:data_to_word$config) r): 'a wordLang$exp =

compiler/backend/presLangScript.sml

@@ -631,6 +631,8 @@ val stack_prog_to_display_def = Define`
         store_name_to_display sn]
     | Set sn n => Item NONE «Set» [store_name_to_display sn;
         num_to_display n]
+    | OpCurrHeap b n1 n2 => Item NONE «OpCurrHeap»
+        [asm_binop_to_display b; num_to_display n1; num_to_display n2]
     | Call rh tgt eh => Item NONE «Call»
         [(case rh of
             | NONE => empty_item «Tail»
@@ -762,6 +764,8 @@ val word_prog_to_display_def = tDefine "word_prog_to_display" `
     [word_prog_to_display_ret a; option_to_display num_to_display b;
         list_to_display num_to_display c;
         word_prog_to_display_handler d]) /\
+  (word_prog_to_display (OpCurrHeap b n1 n2) = Item NONE «OpCurrHeap»
+    [asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\
   (word_prog_to_display (Seq prog1 prog2) = Item NONE (strlit "Seq")
     [word_prog_to_display prog1; word_prog_to_display prog2]) /\
   (word_prog_to_display (If cmp n reg p1 p2) = Item NONE (strlit "If")

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -8474,7 +8474,7 @@ Theorem word_exp_insert:
       word_exp t (real_addr c m)))
 Proof
   fs [wordSemTheory.word_exp_def,real_addr_def]
-  \\ IF_CASES_TAC \\ fs []
+  \\ rpt (IF_CASES_TAC \\ fs [])
   \\ fs [wordSemTheory.word_exp_def,real_addr_def] \\ fs [lookup_insert]
 QED
 

compiler/backend/proofs/data_to_word_memoryProofScript.sml

@@ -4609,16 +4609,28 @@ val get_real_addr_def = Define `
     let k = shift (:α) in
       case FLOOKUP st CurrHeap of
       | SOME (Word curr) =>
-          if k <= conf.pad_bits + 1
-          then SOME (curr + (w >>> (shift_length conf - k)))
-          else SOME (curr + (w >>> (shift_length conf) << k))
+          if k = shift_length conf ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0
+          then SOME (curr + w - 1w)
+          else
+            if k <= conf.pad_bits + 1
+            then SOME (curr + (w >>> (shift_length conf - k)))
+            else SOME (curr + (w >>> (shift_length conf) << k))
       | _ => NONE`
 
 val get_real_offset_def = Define `
   get_real_offset (w:'a word) =
     if dimindex (:'a) = 32
     then SOME (w + bytes_in_word) else SOME (w << 1 + bytes_in_word)`
 
+Triviality or_1:
+  ∀w. (0 -- 0) w ‖ 1w = 1w :'a word
+Proof
+  fs [fcpTheory.CART_EQ,word_or_def,fcpTheory.FCP_BETA,word_lsl_def,
+      word_0,word_bits_def]
+  \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
+  \\ rw [] \\ eq_tac \\ rw []
+QED
+
 Theorem get_real_addr_get_addr:
    heap_length heap <= dimword (:'a) DIV 2 ** shift_length c /\
     heap_lookup n heap = SOME anything /\
@@ -4635,6 +4647,23 @@ Proof
     \\ match_mp_tac LESS_LESS_EQ_TRANS
     \\ once_rewrite_tac [CONJ_COMM]
     \\ asm_exists_tac \\ fs [])
+  \\ IF_CASES_TAC
+  THEN1
+   (Cases_on ‘w’
+    \\ fs [get_lowerbits_def,small_shift_length_def,or_1]
+    \\ ‘0w = n2w n ≪ shift_length c && 1w’ by
+     (fs [fcpTheory.CART_EQ,word_and_def,fcpTheory.FCP_BETA,word_lsl_def,word_0]
+      \\ rewrite_tac [word_1comp_def]
+      \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
+      \\ gvs [good_dimindex_def,shift_def])
+    \\ drule (GSYM WORD_ADD_OR)
+    \\ pop_assum kall_tac
+    \\ fs []
+    \\ gvs [WORD_MUL_LSL,bytes_in_word_def,word_mul_n2w,good_dimindex_def,
+            dimword_def,shift_def]
+    \\ qpat_x_assum ‘_ = shift_length _’ (assume_tac o GSYM)
+    \\ fs [])
+  \\ pop_assum kall_tac
   \\ reverse IF_CASES_TAC THEN1
    (drule lsl_lsr \\ fs [get_lowerbits_LSL_shift_length]
     \\ fs [] \\ rw []

compiler/backend/proofs/stack_allocProofScript.sml

@@ -5215,6 +5215,19 @@ Proof
     \\ BasicProvers.TOP_CASE_TAC \\ fs[] \\ rw[]
     \\ imp_res_tac FLOOKUP_SUBMAP \\ fs[]
     \\ full_simp_tac(srw_ss())[state_component_equality] )
+  \\ conj_tac (* OpCurrHeap *) >- (
+    fs[Once comp_def,evaluate_def,get_var_def,word_exp_def]
+    \\ fs [AllCaseEqs(),set_var_def]
+    \\ full_simp_tac(srw_ss())[state_component_equality]
+    \\ rw [] \\ fs [PULL_EXISTS]
+    \\ gs [optionTheory.IS_SOME_EXISTS,AllCaseEqs()]
+    \\ qpat_x_assum`_ = t.regs`(assume_tac o SYM) \\ fs[]
+    \\ rename [‘FLOOKUP s.regs src = SOME (Word x7)’]
+    \\ ‘FLOOKUP regs src = SOME (Word x7)’ by fs [FLOOKUP_DEF,SUBMAP_DEF]
+    \\ fs []
+    \\ match_mp_tac SUBMAP_mono_FUPDATE
+    \\ rw[GSYM SUBMAP_DOMSUB_gen]
+    \\ metis_tac[SUBMAP_TRANS,SUBMAP_DOMSUB] )
   \\ conj_tac (* Tick *) >- (
     rpt strip_tac
     \\ qexists_tac `0` \\ full_simp_tac(srw_ss())[Once comp_def,evaluate_def,dec_clock_def]

compiler/backend/proofs/stack_namesProofScript.sml

@@ -208,7 +208,6 @@ val comp_correct = Q.prove(
      s.compile = (λcfg. c cfg o (stack_names$compile f))
      ==>
      evaluate (comp f p, rename_state c f s) = (r, rename_state c f t)`,
-
   recInduct evaluate_ind \\ rpt strip_tac
   THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac)
   THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac \\ CASE_TAC \\ fs []
@@ -219,6 +218,7 @@ val comp_correct = Q.prove(
     imp_res_tac inst_rename >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
+  THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] \\ rw []
          \\ fs [] \\ rw [] \\ fs [empty_env_def,dec_clock_def])
   THEN1

compiler/backend/proofs/stack_rawcallProofScript.sml

@@ -158,6 +158,8 @@ Proof
    (rename [`Get`] \\ simple_case)
   THEN1
    (rename [`Set`] \\ simple_case)
+  THEN1
+   (rename [`OpCurrHeap`] \\ simple_case)
   THEN1
    (rename [`Tick`] \\ simple_case)
   THEN1
@@ -941,26 +943,4 @@ Proof
   \\ simp [stack_get_handler_labels_def]
 QED
 
-(*
-Theorem get_code_labels_comp:
-  !i p.
-    get_code_labels (comp i p) = get_code_labels p /\
-    get_code_labels (comp_top i p) = get_code_labels p
-Proof
-  recInduct comp_ind \\ rpt gen_tac \\ strip_tac
-  \\ Cases_on `p` \\ fs [] \\ simp [comp_top_def]
-  \\ simp [Once comp_def]
-  \\ TRY (fs [get_code_labels_def] \\ NO_TAC)
-  THEN1 (every_case_tac \\ fs [get_code_labels_def])
-  \\ reverse conj_asm2_tac THEN1 fs [get_code_labels_def]
-  \\ rename [`comp_seq p1 p2`]
-  \\ Cases_on `comp_seq p1 p2 i (Seq (comp i p1) (comp i p2)) =
-               Seq (comp i p1) (comp i p2)` \\ simp []
-  \\ drule comp_seq_neq_IMP \\ strip_tac \\ rveq \\ fs []
-  \\ fs [comp_seq_def,dest_case_def,CaseEq"option",CaseEq"bool"]
-  \\ Cases_on `lookup dest i` \\ fs []  \\ rw []
-  \\ simp [get_code_labels_def]
-QED
-*)
-
 val _ = export_theory();

compiler/backend/proofs/stack_removeProofScript.sml

@@ -9,7 +9,7 @@ open preamble
      set_sepTheory
      semanticsPropsTheory
      helperLib
-local open dep_rewrite blastLib in end
+local open dep_rewrite blastLib labPropsTheory in end
 
 val _ = new_theory"stack_removeProof";
 
@@ -597,6 +597,7 @@ Theorem state_rel_word_exp:
    word_exp t e = SOME w
 Proof
   ho_match_mp_tac word_exp_ind
+  \\ rpt conj_tac
   \\ simp[word_exp_def]
   \\ rw[]
   \\ imp_res_tac state_rel_mem_load_imp
@@ -990,7 +991,7 @@ val name_cases = prove(
 (* Significantly faster than SEP_R_TAC *)
 val mem_load_lemma = Q.prove(`
   MEM name store_list ∧
-  FLOOKUP (s:('a,'c,'b)state).store name = SOME x ∧
+  FLOOKUP (s:('a,'c,'b)stackSem$state).store name = SOME x ∧
   (memory s.memory s.mdomain *
         word_list
           (the_SOME_Word (FLOOKUP s.store BitmapBase) ≪ word_shift (:α))
@@ -1001,7 +1002,7 @@ val mem_load_lemma = Q.prove(`
            bytes_in_word *
            n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
           s.data_buffer.space_left * word_store c s.store *
-        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
+        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
   mem_load (c+store_offset name) t1 = SOME x`,
   strip_tac >>
   drule fun2set_STAR_IMP>>
@@ -1041,7 +1042,7 @@ val mem_load_lemma2 = Q.prove(`
            bytes_in_word *
            n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
           s.data_buffer.space_left * word_store c s.store *
-        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
+        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
   c+store_offset name ∈ t1.mdomain`,
   strip_tac >>
   drule fun2set_STAR_IMP>>
@@ -1142,28 +1143,31 @@ Proof
   srw_tac[][FUN_EQ_THM,prog_comp_def,FORALL_PROD,LAMBDA_PROD]
 QED
 
-val comp_correct = Q.prove(
-  `!p s1 r s2 t1 k off jump.
+Theorem comp_correct[local]:
+  !p s1 r s2 t1 k off jump.
      evaluate (p,s1) = (r,s2) /\ r <> SOME Error /\
      state_rel jump off k s1 t1 /\ reg_bound p k ==>
      ?ck t2. evaluate (comp jump off k p,t1 with clock := ck + t1.clock) = (r,t2) /\
              (case r of
-               | SOME (Halt _) => t2.ffi = s2.ffi
-               | SOME TimeOut => t2.ffi = s2.ffi
-               | SOME (FinalFFI _) => t2.ffi = s2.ffi
-               | _ =>  (state_rel jump off k s2 t2))`,
+              | SOME (Halt _) => t2.ffi = s2.ffi
+              | SOME TimeOut => t2.ffi = s2.ffi
+              | SOME (FinalFFI _) => t2.ffi = s2.ffi
+              | _ =>  (state_rel jump off k s2 t2))
+Proof
   recInduct evaluate_ind \\ rpt strip_tac
-  THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
-  THEN1
+  THEN1 (* Skip *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
+  THEN1 (* Halt *)
    (full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
     \\ imp_res_tac state_rel_get_var \\ full_simp_tac(srw_ss())[]
     \\ qexists_tac`0`
     \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
     \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
     \\ full_simp_tac(srw_ss())[state_rel_def])
-  THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
-  THEN1 (
-    full_simp_tac(srw_ss())[comp_def,evaluate_def]
+  THEN1 (* Alloc *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
+  THEN1 (* Inst *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def]
     \\ last_x_assum mp_tac
     \\ BasicProvers.TOP_CASE_TAC \\ full_simp_tac(srw_ss())[]
     \\ strip_tac \\ rveq
@@ -1224,6 +1228,19 @@ val comp_correct = Q.prove(
     \\ Q.ABBREV_TAC `d = t1.mdomain`
     \\ drule name_cases
     \\ metis_tac[store_write_lemma])
+  THEN1 (* OpCurrHeap *)
+   (qexists_tac`0`
+    \\ `s.use_store` by full_simp_tac(srw_ss())[state_rel_def]
+    \\ full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
+    \\ gvs [AllCaseEqs(),word_exp_def]
+    \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
+    \\ fs [inst_def,assign_def,word_exp_def]
+    \\ gvs [AllCaseEqs(),word_exp_def,PULL_EXISTS]
+    \\ rename [‘FLOOKUP s.regs src = SOME (Word c1)’]
+    \\ rename [‘FLOOKUP s.store CurrHeap = SOME (Word c2)’]
+    \\ qsuff_tac ‘FLOOKUP t1.regs src = SOME (Word c1) ∧
+                  FLOOKUP t1.regs (k + 2) = SOME (Word c2)’ THEN1 fs []
+    \\ fs [state_rel_def])
   THEN1 (* Tick *)
    (full_simp_tac(srw_ss())[comp_def,evaluate_def]
     \\ `s.clock = t1.clock` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[]
@@ -1516,7 +1533,7 @@ val comp_correct = Q.prove(
     \\ disch_then(qspec_then`ck2`mp_tac)
     \\ simp[] \\ ntac 2 strip_tac
     \\ qexists_tac`ck' + ck2` \\  simp[] )
- THEN1 ( (* Install *)
+  THEN1 ( (* Install *)
     rw[comp_def]
     \\ fs[evaluate_def]
     \\ fs[reg_bound_def]
@@ -1968,7 +1985,8 @@ val comp_correct = Q.prove(
       \\ full_simp_tac(srw_ss())[mem_load_def]  \\ SEP_R_TAC \\ full_simp_tac(srw_ss())[])
     \\ `good_dimindex(:'a)` by full_simp_tac(srw_ss())[state_rel_def]
     \\ full_simp_tac(srw_ss())[labPropsTheory.good_dimindex_def,word_shift_def,FLOOKUP_UPDATE]
-    \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def]));
+    \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def])
+QED
 
 Theorem compile_semantics:
    state_rel jump off k s1 s2 /\ semantics start s1 <> Fail ==>
@@ -3442,8 +3460,8 @@ Proof
 QED
 
 Theorem stack_remove_lab_pres:
-    ∀jump off k p.
-  extract_labels p = extract_labels (comp jump off k p)
+  ∀jump off k p.
+    extract_labels p = extract_labels (comp jump off k p)
 Proof
   ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
   once_rewrite_tac [comp_def]>>fs[extract_labels_def]>>
@@ -3474,25 +3492,26 @@ Proof
 QED
 
 Theorem stack_remove_comp_stack_asm_name:
-    ∀jump off k p.
-  stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
-  addr_offset_ok c 0w ∧
-  good_dimindex (:'a) ∧
-  (∀n. n ≤ max_stack_alloc ⇒
-  c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
-  c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
-  (* Needed to implement the global store *)
-  (∀s. addr_offset_ok c (store_offset s)) ∧
-  reg_name (k+2) c ∧
-  reg_name (k+1) c ∧
-  reg_name k c ∧
-  off = c.addr_offset ⇒
-  stack_asm_name c (comp jump off k p)
+  ∀jump off k p.
+    stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
+    addr_offset_ok c 0w ∧
+    good_dimindex (:'a) ∧
+    (∀n. n ≤ max_stack_alloc ⇒
+    c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
+    c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
+    (* Needed to implement the global store *)
+    (∀s. addr_offset_ok c (store_offset s)) ∧
+    reg_name (k+2) c ∧
+    reg_name (k+1) c ∧
+    reg_name k c ∧
+    off = c.addr_offset ⇒
+    stack_asm_name c (comp jump off k p)
 Proof
   ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
   simp[Once comp_def]>>
   rw[]>>
-  fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
+  fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,
+     arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
   >-
     (every_case_tac>>fs[])
   >-

compiler/backend/proofs/stack_to_labProofScript.sml

@@ -1167,6 +1167,10 @@ Proof
     rename [`Set`] >>
     srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
     full_simp_tac(srw_ss())[state_rel_def] ) >>
+  conj_tac >- (
+    rename [`OpCurrHeap`] >>
+    srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
+    full_simp_tac(srw_ss())[state_rel_def] ) >>
   conj_tac >- (
     rename [`Tick`] >>
     simp[stackSemTheory.evaluate_def,flatten_def] >>