Merge branch 'master' into Iced_cake

Author: HeikoBecker

compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml

@@ -3043,7 +3043,20 @@ Proof
     simp[Abbr`m'`]
     \\ IF_CASES_TAC
     >- (
-      DEP_REWRITE_TAC[get_mem_word_asm_write_bytearray_UNCHANGED_LT]
+      IF_CASES_TAC
+      >- (
+        DEP_REWRITE_TAC[get_mem_word_asm_write_bytearray_UNCHANGED_LT]
+        \\ conj_tac
+        >- (
+          EVAL_TAC \\ fs[]
+          \\ Cases_on`ms.R 3w` \\ fs[]
+          \\ fs[word_ls_n2w, word_lo_n2w]
+          \\ fs[EVAL``heap_start_offset``] )
+        \\ DEP_REWRITE_TAC[get_mem_word_UPDATE]
+        \\ conj_tac >- EVAL_TAC
+        \\ simp[])
+      \\ pop_assum kall_tac
+      \\ DEP_REWRITE_TAC[get_mem_word_asm_write_bytearray_UNCHANGED_LT]
       \\ conj_tac
       >- (
         EVAL_TAC \\ fs[]
@@ -3076,19 +3089,13 @@ Proof
   \\ simp[Q.ISPEC`λx. 1n`SUM_MAP_K |> SIMP_RULE(srw_ss())[]]
   \\ rw[]
   \\ simp[Abbr`m'`]
-  \\ rw[]
+  \\ reverse IF_CASES_TAC
   >- (
-    irule EQ_SYM
-    \\ irule asm_write_bytearray_unchanged_all_words
-    \\ conj_tac
+    simp[APPLY_UPDATE_THM]
+    \\ IF_CASES_TAC
     >- (
-      simp[IN_all_words, LENGTH_TAKE_EQ_MIN]
+      pop_assum mp_tac
       \\ EVAL_TAC
-      \\ simp[DISJ_EQ_IMP]
-      \\ qmatch_goalsub_abbrev_tac`LENGTH conf + (k + _)`
-      \\ `k ≤ 2048` by simp[Abbr`k`]
-      \\ reverse(Cases_on`LENGTH conf = 8` \\ fs[])
-      >- ( rveq \\ fs[LUPDATE_def] )
       \\ fs[EVAL``cline_size``] )
     \\ irule EQ_SYM
     \\ irule asm_write_bytearray_unchanged_all_words
@@ -3104,12 +3111,38 @@ Proof
     \\ rw[]
     \\ pop_assum mp_tac
     \\ EVAL_TAC
-    \\ fs[EVAL``cline_size``] )
-  \\ simp[APPLY_UPDATE_THM]
+    \\ fs[EVAL``cline_size``]
+    )
   \\ IF_CASES_TAC
   >- (
-    pop_assum mp_tac
+    irule EQ_SYM
+    \\ irule asm_write_bytearray_unchanged_all_words
+    \\ conj_tac
+    >- (
+      simp[IN_all_words, word_add_n2w, ADD1, DISJ_EQ_IMP]
+      \\ Cases_on`ms.R 3w` \\ fs[EVAL``heap_start_offset``, ADD1]
+      \\ simp[word_add_n2w, EVAL``startup_code_size``]
+      \\ rw[]
+      \\ fs[EVAL``cline_size``]
+      \\ fs[word_lo_n2w, word_ls_n2w] )
+    \\ simp[APPLY_UPDATE_THM]
+    \\ rw[]
+    \\ pop_assum mp_tac
+    \\ EVAL_TAC
+    \\ fs[EVAL``cline_size``]
+    )
+  \\ pop_assum kall_tac
+  \\ irule EQ_SYM
+  \\ irule asm_write_bytearray_unchanged_all_words
+  \\ conj_tac
+  >- (
+    simp[IN_all_words, LENGTH_TAKE_EQ_MIN]
     \\ EVAL_TAC
+    \\ simp[DISJ_EQ_IMP]
+    \\ qmatch_goalsub_abbrev_tac`LENGTH conf + (k + _)`
+    \\ `k ≤ 2048` by simp[Abbr`k`]
+    \\ reverse(Cases_on`LENGTH conf = 8` \\ fs[])
+    >- ( rveq \\ fs[LUPDATE_def] )
     \\ fs[EVAL``cline_size``] )
   \\ irule EQ_SYM
   \\ irule asm_write_bytearray_unchanged_all_words
@@ -4186,14 +4219,17 @@ Proof
     \\ simp[ag32_ffi_mem_domain_def]
     \\ EVAL_TAC
     \\ fs[word_ls_n2w, word_lo_n2w, word_add_n2w] )
+  \\ `LENGTH conf = 8` by (
+    fs[fsFFITheory.ffi_write_def]
+    \\ fs[OPTION_CHOICE_EQUALS_OPTION, LUPDATE_def] \\ rveq \\ fs[] )
+  \\ fs[]
   \\ irule asm_write_bytearray_unchanged
   \\ qpat_x_assum`_ = w2n (ms.R 4w)`(assume_tac o SYM)
   \\ Cases_on`ms.R 3w` \\ fs[memory_size_def]
   \\ qpat_x_assum`_ = w2n (ms.R 2w)`(assume_tac o SYM) \\ fs[]
   \\ fs[word_add_n2w]
   \\ fs[EVAL``output_offset``]
   \\ Cases_on`x` \\ fs[word_lo_n2w, word_ls_n2w]
-  \\ qmatch_goalsub_abbrev_tac`LENGTH conf + ll`
   \\ pop_assum mp_tac
   \\ simp[LENGTH_TAKE_EQ]
   \\ reverse IF_CASES_TAC
@@ -4204,11 +4240,7 @@ Proof
     \\ pairarg_tac \\ fs[fsFFITheory.write_def]
     \\ pairarg_tac \\ fs[] \\ rveq )
   \\ simp[EVAL``output_buffer_size``]
-  \\ `LENGTH conf = 8` by (
-    fs[fsFFITheory.ffi_write_def]
-    \\ fs[OPTION_CHOICE_EQUALS_OPTION, LUPDATE_def] \\ rveq \\ fs[] )
   \\ strip_tac
-  \\ simp[Abbr`ll`]
   \\ conj_tac >- simp[MIN_DEF]
   \\ conj_tac
   >- (
@@ -6138,7 +6170,7 @@ Theorem ag32_good_init_state:
    ∃io_regs cc_regs.
    good_init_state (ag32_machine_config ffi_names (LENGTH code) (LENGTH data))
      (FUNPOW Next startup_clock ms0)
-     (basis_ffi cl fs) code 0
+     code 0
      ((init_asm_state code data ffi_names (cl,inp)) with
        mem_domain := (ag32_machine_config ffi_names (LENGTH code) (LENGTH data)).prog_addresses)
      (λk. Word
@@ -6246,13 +6278,9 @@ Proof
     \\ fs[ag32_targetTheory.ag32_ok_def]
     \\ fs[ag32_targetTheory.ag32_config_def]
     >- (
-      fs[ffiTheory.call_FFI_def]
-      \\ rveq
-      \\ reverse conj_tac
-      >- (
-        rw[]
-        \\ rw[APPLY_UPDATE_THM, targetSemTheory.get_reg_value_def, EVAL``ALOOKUP ffi_exitpcs ""``] )
-      \\ rw[]
+      rw[]
+      \\ rw[APPLY_UPDATE_THM, targetSemTheory.get_reg_value_def,
+         EVAL``ALOOKUP ffi_exitpcs ""``]
       \\ irule EQ_SYM
       \\ irule asm_write_bytearray_id
       \\ gen_tac \\ strip_tac
@@ -6283,9 +6311,6 @@ Proof
       \\ fs[IS_SOME_EXISTS]
       \\ rpt(IF_CASES_TAC \\ simp[targetSemTheory.get_reg_value_def]))
     \\ rw[]
-    \\ rfs[ffiTheory.call_FFI_def]
-    \\ `st.oracle = (basis_ffi cl fs).oracle` by metis_tac[evaluatePropsTheory.RTC_call_FFI_rel_consts]
-    \\ fs[basis_ffiTheory.basis_ffi_def]
     \\ `EL index ffi_names ∈ set(MAP FST FFI_codes)` by (
       fs[SUBSET_DEF]
       \\ fs[FFI_codes_def, ffi_exitpcs_def]
@@ -6296,14 +6321,6 @@ Proof
     \\ qpat_x_assum`MEM nm _`mp_tac
     \\ simp[Once FFI_codes_def]
     \\ strip_tac \\ rveq \\ fs[]
-    \\ qmatch_asmsub_abbrev_tac`oracle_result_CASE r`
-    \\ pop_assum mp_tac
-    \\ simp[basis_ffiTheory.basis_ffi_oracle_def]
-    \\ strip_tac \\ fs[Abbr`r`]
-    \\ fs[CaseEq"option",CaseEq"bool",CaseEq"oracle_result"]
-    \\ pairarg_tac \\ fs[]
-    \\ fs[CaseEq"option",CaseEq"bool",CaseEq"oracle_result",CaseEq"ffi_result"]
-    \\ rveq \\ fs[]
     \\ simp[ag32_ffi_mem_update_def]
     \\ qmatch_goalsub_abbrev_tac`asm_write_bytearray p new_bytes m2`
     \\ `asm_write_bytearray p new_bytes m2 a = asm_write_bytearray p new_bytes t1.mem a`
@@ -6315,14 +6332,8 @@ Proof
       \\ simp[ag32_prog_addresses_def]
       \\ qpat_x_assum` _ < memory_size`mp_tac
       \\ EVAL_TAC \\ simp[])
-    \\ TRY (
-      CHANGED_TAC(fs[fsFFITheory.ffi_read_def])
-      \\ fs[CaseEq"list"] \\ rveq
-      \\ PURE_TOP_CASE_TAC \\ fs[]
-      \\ PURE_TOP_CASE_TAC \\ fs[]
-      \\ PURE_TOP_CASE_TAC \\ fs[]
-      \\ reverse IF_CASES_TAC >- rw[]
-      \\ rw[]
+    >- (
+      ntac 3 (PURE_TOP_CASE_TAC >> simp[]) >> IF_CASES_TAC >> rw[]
       \\ qmatch_goalsub_abbrev_tac`set_mem_word x y m a`
       \\ qpat_x_assum`m a = _`(SUBST1_TAC o SYM)
       \\ irule set_mem_word_neq
@@ -6333,7 +6344,7 @@ Proof
       \\ qpat_x_assum`_ < memory_size`mp_tac
       \\ EVAL_TAC
       \\ Cases_on`a` \\ fs[word_ls_n2w, word_lo_n2w, word_add_n2w]
-      \\ NO_TAC)
+      )
     \\ reverse IF_CASES_TAC
     >- (
       rw[APPLY_UPDATE_THM]
@@ -6345,23 +6356,10 @@ Proof
     \\ rw[]
     \\ fs[targetSemTheory.read_ffi_bytearrays_def]
     \\ fs[targetSemTheory.read_ffi_bytearray_def]
-    \\ fs[fsFFITheory.ffi_write_def]
-    \\ fs[CaseEq"list"] \\ rveq
-    \\ qhdtm_x_assum`OPTION_CHOICE`mp_tac
-    \\ rewrite_tac[OPTION_CHOICE_EQUALS_OPTION]
-    \\ reverse strip_tac
-    >- (
-      pop_assum mp_tac \\ simp[LUPDATE_def]
-      \\ strip_tac \\ rveq
-      \\ qpat_x_assum`_ = 0w`mp_tac
-      \\ simp[] )
-    \\ fs[]
-    \\ pairarg_tac \\ fs[] \\ rveq
-    \\ rw[]
-    \\ irule asm_write_bytearray_unchanged
+    \\ ntac 5 (PURE_TOP_CASE_TAC >> simp[])
+    \\ irule asm_write_bytearray_unchanged \\ simp[]
     \\ fs[EVAL``output_offset``, output_buffer_size_def]
     \\ fs[LENGTH_TAKE_EQ, fsFFITheory.write_def]
-    \\ pairarg_tac \\ fs[]
     \\ qpat_x_assum`_ ∈ _.mem_domain`mp_tac
     \\ qpat_x_assum`_ = _.mem_domain`(mp_tac o SYM)
     \\ simp[ag32_prog_addresses_def]
@@ -6370,7 +6368,8 @@ Proof
     \\ qpat_x_assum`_ < memory_size`mp_tac
     \\ CONV_TAC(LAND_CONV EVAL)
     \\ Cases_on`a` \\ fs[word_ls_n2w, word_lo_n2w, word_add_n2w]
-    \\ rw[MIN_DEF])
+    \\ rw[MIN_DEF]
+    )
   \\ conj_tac >- (
     rw[targetSemTheory.ccache_interfer_ok_def, ag32_machine_config_def,
        lab_to_targetTheory.ffi_offset_def, ag32_ccache_interfer_def,
@@ -6505,7 +6504,7 @@ Theorem ag32_installed:
      x ∉ ag32_startup_addresses ⇒
        ((FUNPOW Next startup_clock ms0).MEM x = ms0.MEM x))
    ⇒
-   installed code 0 data 0 (SOME ffi_names) (basis_ffi cl fs)
+   installed code 0 data 0 (SOME ffi_names)
      (heap_regs ag32_backend_config.stack_conf.reg_names)
      (ag32_machine_config ffi_names (LENGTH code) (LENGTH data))
      (FUNPOW Next startup_clock ms0)
@@ -6523,7 +6522,7 @@ Proof
   \\ disch_then drule
   \\ disch_then drule
   \\ strip_tac
-  \\ qmatch_asmsub_abbrev_tac`good_init_state _ _ _ _ _ t`
+  \\ qmatch_asmsub_abbrev_tac`good_init_state _ _ _ _ t`
   \\ qexists_tac`t` \\ simp[Abbr`t`]
   \\ asm_exists_tac \\ fs[]
   \\ qhdtm_x_assum`good_init_state` mp_tac

compiler/backend/ag32/proofs/ag32_machine_configScript.sml

@@ -39,17 +39,22 @@ val ag32_ffi_mem_update_def = Define`
   ag32_ffi_mem_update name conf bytes new_bytes mem =
     if (name = "write") then
       if (HD new_bytes = 0w) then
-        case bytes of (n1 :: n0 :: off1 :: off0 :: tll) =>
+        case bytes of
+        | (n1 :: n0 :: off1 :: off0 :: tll) =>
+          if LENGTH conf ≠ 8 then mem else
           let k = MIN (w22n [n1; n0]) output_buffer_size in
           let written = TAKE k (DROP (w22n [off1; off0]) tll) in
             asm_write_bytearray (n2w output_offset) (conf ++ [0w;0w;n1;n0] ++ written) mem
+        | _ => mem
       else ((n2w output_offset) =+ 1w) mem
     else if (name = "read") then
-      case new_bytes of (zz :: k1 :: k0 :: _) =>
+      case new_bytes of
+      | (zz :: k1 :: k0 :: _) =>
         if (zz = 0w) then
           set_mem_word (n2w stdin_offset)
             (get_mem_word mem (n2w stdin_offset) + n2w (w22n [k1; k0])) mem
         else mem
+      | _ => mem
     else mem`;
 
 val ag32_ffi_interfer_def = Define`

compiler/backend/arm8_asl/arm8_asl_configProofScript.sml

@@ -43,7 +43,7 @@ Theorem arm8_asl_compile_correct:
   compile arm8_backend_config prog = SOME (bytes, bitmaps, config') ⇒
     let (s,env) = THE (prim_sem_env ffi) in
     ¬semantics_prog s env prog Fail ∧
-    installed bytes cbspace bitmaps data_sp config'.lab_conf.ffi_names ffi (1,3) mc ms
+    installed bytes cbspace bitmaps data_sp config'.lab_conf.ffi_names (1,3) mc ms
     ⇒ machine_sem mc ffi ms ⊆
         extend_with_resource_limit (semantics_prog s env prog)
 Proof

compiler/backend/proofs/backendProofScript.sml

@@ -2966,7 +2966,7 @@ Theorem compile_correct':
    ¬semantics_prog s env prog Fail ∧
    backend_config_ok c ∧ lab_to_targetProof$mc_conf_ok mc ∧ mc_init_ok c mc ∧
    opt_eval_config_wf c' ev ∧
-   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names ffi (heap_regs c.stack_conf.reg_names) mc ms ⇒
+   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names (heap_regs c.stack_conf.reg_names) mc ms ⇒
      machine_sem (mc:(α,β,γ) machine_config) ffi ms ⊆
        extend_with_resource_limit'
          (is_safe_for_space ffi c prog (read_limits c mc ms))
@@ -3116,7 +3116,7 @@ Proof
   \\ disch_tac \\ fs []
   \\ fs [attach_bitmaps_def] \\ rveq \\ fs [] \\
   fs[targetSemTheory.installed_def] \\
-  qmatch_assum_abbrev_tac`good_init_state mc ms ffi bytes cbspace tar_st m dm io_regs cc_regs` \\
+  qmatch_assum_abbrev_tac`good_init_state mc ms bytes cbspace tar_st m dm io_regs cc_regs` \\
   qpat_x_assum`Abbrev(p7 = _)` mp_tac>>
   qmatch_goalsub_abbrev_tac`compile _ _ _ stk stoff`>>
   strip_tac \\
@@ -3337,11 +3337,12 @@ Proof
   `Fail ∉ y` by (fs [Abbr `y`] \\ fs [GSYM pure_co_def, simple_orac_eqs]) \\
   pop_assum mp_tac \\ simp[GSYM implements'_def] \\
   simp[Abbr`y`] \\
-  old_drule (GEN_ALL lab_to_targetProofTheory.semantics_compile) \\
+  old_drule $ GEN_ALL $
+    INST_TYPE [delta |-> ``:'ffi``] lab_to_targetProofTheory.semantics_compile \\
   disch_then(old_drule o CONV_RULE(STRIP_QUANT_CONV(LAND_CONV(move_conj_left(optionSyntax.is_some o rhs))))) \\
   simp[Abbr`c4`] \\
   disch_then(old_drule o CONV_RULE(STRIP_QUANT_CONV(LAND_CONV(move_conj_left(same_const``good_init_state`` o fst o strip_comb))))) \\
-  disch_then(qspec_then`lab_oracle`mp_tac)
+  disch_then(qspecl_then[`ffi`,`lab_oracle`]mp_tac)
   \\ old_drule (GEN_ALL bvi_tailrecProofTheory.compile_prog_next_mono)
   \\ strip_tac
   \\ pop_assum(assume_tac o Abbrev_intro)
@@ -3732,7 +3733,7 @@ Theorem compile_correct:
    let (s,env) = THE (prim_sem_env (ffi:'ffi ffi_state)) in
    ¬semantics_prog s env prog Fail ∧
    backend_config_ok c ∧ lab_to_targetProof$mc_conf_ok mc ∧ mc_init_ok c mc ∧
-   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names ffi
+   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names
         (heap_regs c.stack_conf.reg_names) mc ms ⇒
      machine_sem (mc:(α,β,γ) machine_config) ffi ms ⊆
        extend_with_resource_limit (semantics_prog s env prog)
@@ -3759,7 +3760,7 @@ Theorem compile_correct_is_safe_for_space:
   let (s,env) = THE (prim_sem_env (ffi:'ffi ffi_state)) in
   ¬semantics_prog s env prog Fail ∧
   backend_config_ok c ∧ lab_to_targetProof$mc_conf_ok mc ∧ mc_init_ok c mc ∧
-  installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names ffi
+  installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names
        (heap_regs c.stack_conf.reg_names) mc ms ⇒
   machine_sem (mc:(α,β,γ) machine_config) ffi ms =
   semantics_prog s env prog
@@ -3783,7 +3784,7 @@ Theorem compile_correct_eval:
    let (s0,env) = THE (prim_sem_env (ffi: 'ffi ffi_state)) in
    ¬semantics_prog (add_eval_state ev s0) env prog Fail ∧ backend_config_ok c ∧
    lab_to_targetProof$mc_conf_ok mc ∧ mc_init_ok c mc ∧ opt_eval_config_wf c' ev ∧
-   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names ffi
+   installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names
      (heap_regs c.stack_conf.reg_names) mc ms ⇒
    machine_sem mc ffi ms ⊆
      extend_with_resource_limit

compiler/backend/proofs/lab_to_targetProofScript.sml

@@ -6558,7 +6558,7 @@ val IMP_state_rel_make_init = Q.prove(
    list_subset (find_ffi_names code) mc_conf.ffi_names ∧
     remove_labels clock mc_conf.target.config 0 LN mc_conf.ffi_names code =
       SOME (code2,labs) /\
-    good_init_state mc_conf ms ffi (prog_to_bytes code2)
+    good_init_state mc_conf ms (prog_to_bytes code2)
       cbspace t m dm io_regs cc_regs
       ==>
     state_rel ((mc_conf: ('a,'state,'b) machine_config),code2,labs,
@@ -6584,8 +6584,9 @@ val IMP_state_rel_make_init = Q.prove(
         ccache_interfer_ok_def]
   \\ rfs[]
   \\ conj_tac >- (
-    rw[] \\ first_x_assum irule
-    \\ rw[] \\ asm_exists_tac \\ rw[] )
+    rw[] >> first_x_assum irule >> simp[] >>
+    gvs[call_FFI_def, AllCaseEqs()]
+    )
   \\ conj_tac >-
     (strip_tac >>
     pairarg_tac >> fs[]>>
@@ -6740,7 +6741,7 @@ val semantics_compile_lemma = Q.prove(
     lab_to_target$compile (c:'a lab_to_target$config) code = SOME (bytes,c') /\
     (* FFI is either given or computed *)
     c'.ffi_names = SOME mc_conf.ffi_names /\
-    good_init_state mc_conf ms ffi bytes cbspace t m dm io_regs cc_regs /\
+    good_init_state mc_conf ms bytes cbspace t m dm io_regs cc_regs /\
     semantics (make_init mc_conf ffi io_regs cc_regs t m dm ms code
       lab_to_target$compile (mc_conf.target.get_pc ms+n2w(LENGTH bytes)) cbspace
       coracle
@@ -6799,7 +6800,7 @@ Theorem semantics_compile:
    c.labels = LN ∧ c.pos = 0 ∧
    compile c code = SOME (bytes,c') ∧
    c'.ffi_names = SOME (mc_conf.ffi_names) /\
-   good_init_state mc_conf ms (ffi:'ffi ffi_state) bytes cbspace t m dm io_regs cc_regs ⇒
+   good_init_state mc_conf ms bytes cbspace t m dm io_regs cc_regs ⇒
    implements' T (machine_sem mc_conf ffi ms)
      {semantics
         (make_init mc_conf ffi io_regs cc_regs t m (dm ∩ byte_aligned) ms code