Changeset 2683 for src/joint/semanticsUtils.ma

Timestamp:

Feb 20, 2013, 6:41:46 PM (7 years ago)

Author:

tranquil

Message:

proof of properties of b_graph_program_transform (with an open axiom)

File:

• src/joint/semanticsUtils.ma (modified) (3 diffs)

src/joint/semanticsUtils.ma

@@ -4 +4 @@
 include "ASM/BitVectorTrie.ma".
 include "joint/TranslateUtils.ma".
+include "common/ExtraMonads.ma".
+include "common/extraGlobalenvs.ma".
 
 record hw_register_env : Type[0] ≝
@@ -164 +166 @@
 qed.
 
-axiom b_graph_transform_program_props :
+lemma symbols_match :
+    ∀M:matching.∀initV,initW.
+     (∀v,w. match_var_entry M v w →
+      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
+    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
+    ∀MATCH:match_program … M p p'.
+    symbols … (globalenv … initW p') = symbols … (globalenv … initV p).
+* #A #B #V #W #match_fn #match_var #initV #initW #H
+#p #p' * #Mvars #Mfn #Mmain
+whd in match globalenv in ⊢ (???%); normalize nodelta
+whd in match (globalenv_allocmem ????);
+change with (add_globals ?????) in match (foldl ?????);
+>(proj1 … (add_globals_match … initW … Mvars))
+[ % |*:]
+[ * #idr #v * #idr' #w #MVE %
+  [ inversion MVE
+    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
+  | @(H … MVE)
+  ]
+| @(matching_fns_get_same_blocks … Mfn) 
+  #f #g @match_funct_entry_id
+]
+qed.
+
+lemma symbols_transf:
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
+#A #B #V #iV #p #tf whd
+@(symbols_match … (transform_program_match … tf ?))
+#v0 #w0 * //
+qed.
+
+definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
+λA,B,P,mA,mB.
+∀p.
+match lookup_opt … p mA with
+[ Some a ⇒
+  match lookup_opt … p mB with
+  [ Some b ⇒ P a b
+  | _ ⇒ False
+  ]
+| _ ⇒ match lookup_opt … p mB with
+  [ Some _ ⇒ False
+  | _ ⇒ True
+  ]
+].
+
+definition match_funct_map :
+  ∀M : matching.
+  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
+  λM,vars.pm_P … (match_fundef M ?).
+
+axiom functions_match:
+    ∀M:matching.∀initV,initW.
+    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
+    ∀MATCH:match_program … M p p'.
+    match_funct_map M ?
+      (functions ? (globalenv ?? initV p))
+      (functions ? (globalenv ?? initW p') ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
+@sym_eq @(matching_vars … (mp_vars … MATCH)) qed.
+
+lemma functions_transf:
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
+ option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
+#A #B #V #iV #p #tf #n
+lapply(functions_match … (transform_program_match … tf p) n) try @iV
+cases (lookup_opt … n ?) [2: #f] normalize nodelta
+generalize in ⊢ (match (???match % with [ _ ⇒ ?]) with [ _ ⇒ ? | _ ⇒ ? ] → ?);
+#e >(K ?? e) normalize nodelta
+cases (lookup_opt ???) [2,4: #f'] normalize nodelta
+[2,3,4: * % ]
+#EQ destruct %
+qed.
+
+lemma symbol_for_block_transf :
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ ∀bl.
+ symbol_for_block … (globalenv … init prog_out) bl =
+ symbol_for_block … (globalenv … init prog_in) bl.
+#A #B #V #iV #p #tf whd
+#bl 
+whd in match symbol_for_block; normalize nodelta
+>(symbols_match … (transform_program_match … tf ?))
+[ % |*:]
+#v #w * //
+qed.
+
+include alias "common/Pointers.ma".
+
+lemma fetch_function_transf :
+ ∀A,B,V,init.∀prog_in : program A V.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in trans in
+ ∀bl.
+ fetch_function … (globalenv … init prog_out) bl =
+ ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
+ return 〈i, trans … f〉.
+#A #B #V #init #prog_in #trans #bl
+whd in match fetch_function; normalize nodelta
+>(symbol_for_block_transf A B V init prog_in trans)
+cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
+whd in match find_funct_ptr; normalize nodelta
+whd in match (block_region (pi1 ?? bl));
+cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
+>(functions_transf A B V init prog_in trans p)
+cases (lookup_opt ???) //
+qed.
+
+lemma fetch_internal_function_transf :
+ ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
+ ∀trans : ∀vars.A vars → B vars.
+ let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
+ ∀bl.
+ fetch_internal_function … (globalenv_noinit … prog_out) bl =
+ ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
+ return 〈i, trans … f〉.
+#A #B #prog #trans #bl
+ whd in match fetch_internal_function; normalize nodelta
+>(fetch_function_transf … prog)
+cases (fetch_function ???)
+[ * #id * #f % | #e % ]
+qed.
+
+include alias "utilities/binary/positive.ma".
+
+lemma pm_map_cases : ∀A.∀P : positive_map A → Prop.∀m : positive_map A.
+((∀p.lookup_opt … p m = None ?) → P m) →
+(∀p,v.lookup_opt … p m = Some ? v → P m) →
+P m.
+#A #P #m lapply P -P elim m -m
+[ #P #H1 #_ @H1 #p % ]
+* [2: #x ] #l #r #IHl #IHr #P #H1 #H2 [ @(H2 one x) % ]
+@IHl [2: #p #v #EQ @(H2 (p0 p) v EQ) ]
+#l_empty
+@IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ]
+#r_empty
+@H1 * normalize //
+qed.
+
+lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
+(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
+(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
+∀m.P m.
+#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
+[ #P #H1 #_ @H1 #p % ]
+#o #l #r #IHl #IHr #P #H1 #H2
+@IHl #l'
+[ #empty_l' @IHr #r'
+  [ #empty_r' cases o [ @H1 * try #p normalize // ]
+    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
+    @H2 [ @H1 * try #p normalize // | % ]
+  ]
+]
+#p #v #H #G
+[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
+| change with (P (insert ? (p0 p) v (pm_node ? ???)))
+] @H2 assumption
+qed.
+
+include alias "basics/logic.ma".
+include alias "common/PositiveMap.ma".
+
+lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
+#A #B #impl * #Bf % #At @Bf @impl @At qed-.
+
+lemma b_graph_transform_program_find_funct_ptr :
  ∀src,dst:sem_graph_params.
  ∀data : ∀globals.joint_closed_internal_function src globals →
@@ -172 +346 @@
  let src_genv ≝ globalenv_noinit ? prog_in in
  let dst_genv ≝ globalenv_noinit ? prog_out in
- ∃init_regs : ident → list register.
- ∃f_lbls : ident → label → option (list label).
- ∃f_regs : ident → label → option (list register).
+ ∃init_regs : block → list register.
+ ∃f_lbls : block → label → option (list label).
+ ∃f_regs : block → label → option (list register).
+ ∀bl,def_in.
+ find_funct_ptr … src_genv bl = return (Internal ? def_in) →
+ ∃init_data,def_out.
+ find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
+ bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
+ b_graph_translate_props src dst ? init_data (init_regs bl)
+    def_in def_out (f_lbls bl) (f_regs bl).
+#src #dst #data #prog_in
+whd
+letin prog_out ≝ (b_graph_transform_program … data prog_in)
+letin src_genv ≝ (globalenv_noinit ? prog_in)
+letin dst_genv ≝ (globalenv_noinit ? prog_out)
+cut (∀p.lookup_opt ? p (functions ? dst_genv) =
+     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
+      (lookup_opt ? p (functions ? src_genv)))
+[ @functions_transf ]
+cases dst_genv #functs2 #nextf2 #symbols2 #H2
+cases src_genv #functs1 #nextf1 #symbols1 #H1
+lapply H2 lapply H1 lapply functs2
+@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
+[ #functs1_empty | #p #f #IH #p_not_in ]
+#functs2 #H1 #H2 #transf
+[ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)}
+  #bl #def_in #ABS @⊥ lapply ABS -ABS
+  whd in match find_funct_ptr;
+  normalize nodelta
+  whd in match (block_region bl);
+  cases (block_id bl) normalize nodelta
+  [2,3: #p [2: >functs1_empty ]]
+  normalize #ABS destruct
+]
+cases (IH (pm_set … p (None ?) functs2) ???)
+[2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
+  [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
+  #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
+|3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
+  [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
+  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
+|4: #b @(eqb_elim b p)
+  [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
+  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
+  >(lookup_opt_insert_miss ? f b p … NEQ) %
+]
+-IH cases f in H1 transf; -f #f #H1 #transf
+#init_regs * #f_lbls * #f_regs #props
+[ (* internal *)
+  letin upd ≝ (λA : Type[0].λf : block → A.
+    λid.λv,id'.
+    if eq_block id id' then v else f id')
+  cases (pi2 ?? (b_graph_translate … (data … f) f))
+  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
+  #inst_loc_data #loc_props
+  letin bl ≝ (mk_block (neg p))
+  %{(upd … init_regs bl loc_init_regs)}
+  %{(upd … f_lbls bl loc_f_lbls)}
+  %{(upd … f_regs bl loc_f_regs)}
+| (* external, nothing changes *)
+  %{init_regs}
+  %{f_lbls}
+  %{f_regs}
+]
+* #p' #def_in
+whd in match find_funct_ptr; normalize nodelta
+whd in match (block_region (mk_block p'));
+cases p' -p' [2,3,5,6: #p' ] normalize nodelta
+[1,3,5,6: #ABS normalize in ABS; destruct]
+@(eqb_elim p' p) #pp' destruct
+[1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
+  %{loc_data} %
+  [2: % [ % ]
+    [ >transf >lookup_opt_insert_hit %
+    |*: >eq_block_b_b assumption
+    ]
+  |]
+|*: >(lookup_opt_insert_miss ???? functs1 … pp')
+  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
+  #EQ lapply (props (mk_block (neg p')) def_in EQ)
+  whd in match find_funct_ptr; normalize nodelta
+  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
+]
+qed.
+
+lemma b_graph_transform_program_fetch_internal_function :
+ ∀src,dst:sem_graph_params.
+ ∀data : ∀globals.joint_closed_internal_function src globals →
+  bind_new register (b_graph_translate_data src dst globals).
+ ∀prog_in : joint_program src.
+ let prog_out ≝ b_graph_transform_program … data prog_in in
+ let src_genv ≝ globalenv_noinit ? prog_in in
+ let dst_genv ≝ globalenv_noinit ? prog_out in
+ let code_block ≝ (Σbl.block_region bl = Code) in
+ ∃init_regs : code_block → list register.
+ ∃f_lbls : code_block → label → option (list label).
+ ∃f_regs : code_block → label → option (list register).
  ∀bl,id,def_in.
- fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
+ fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
  ∃init_data,def_out.
- fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
- bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
- b_graph_translate_props src dst ? init_data (init_regs id)
-    def_in def_out (f_lbls id) (f_regs id).
+ fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
+ bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
+ b_graph_translate_props src dst ? init_data (init_regs bl)
+    def_in def_out (f_lbls bl) (f_regs bl).
+#src #dst #data #prog_in
+cases (b_graph_transform_program_find_funct_ptr src dst data prog_in)
+#init_regs * #f_lbls * #f_regs #props
+%{(λb.init_regs b)}
+%{(λb.f_lbls b)}
+%{(λb.f_regs b)}
+#bl #id #def_in
+#H @('bind_inversion H) * #id' * #def_in' -H
+normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
+@('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
+#H @('bind_inversion H) -H #def_in' #H
+whd in ⊢ (??%%→?); #EQ destruct
+cases (props … H)
+#loc_data * #def_out ** #H1 #H2 #H3
+%{loc_data} %{def_out}
+%{H3} %{H2}
+whd in match fetch_internal_function;
+whd in match fetch_function; normalize nodelta
+>symbol_for_block_transf >EQ1 >m_return_bind
+>H1 %
+qed.
+
+lemma b_graph_transform_program_fetch_statement :
+ ∀src,dst:sem_graph_params.
+ ∀data : ∀globals.joint_closed_internal_function src globals →
+  bind_new register (b_graph_translate_data src dst globals).
+ ∀prog_in : joint_program src.
+ let prog_out ≝ b_graph_transform_program … data prog_in in
+ let src_genv ≝ globalenv_noinit ? prog_in in
+ let dst_genv ≝ globalenv_noinit ? prog_out in
+ let code_block ≝ (Σbl.block_region bl = Code) in
+ ∃init_regs : code_block → list register.
+ ∃f_lbls : code_block → label → option (list label).
+ ∃f_regs : code_block → label → option (list register).
+ ∀pc,id,def_in,s.
+ fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
+ ∃init_data,def_out.
+ let bl ≝ pc_block pc in
+ fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
+ bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
+ b_graph_translate_props src dst ? init_data (init_regs bl)
+    def_in def_out (f_lbls bl) (f_regs bl) ∧
+ let l ≝ point_of_pc dst pc in
+ ∃lbls,regs.
+ f_lbls bl l = Some ? lbls ∧
+ f_regs bl l = Some ? regs ∧
+  match s with
+  [ sequential s' nxt ⇒
+    let block ≝
+      if eq_identifier … (joint_if_entry … def_in) l then
+        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
+      else
+        f_step … init_data l s' in
+    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
+  | final s' ⇒
+    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
+  | FCOND abs _ _ _ ⇒ Ⓧabs
+  ].
+#src #dst #data #prog_in
+cases (b_graph_transform_program_fetch_internal_function src dst data prog_in)
+#init_regs * #f_lbls * #f_regs #props
+%{init_regs}
+%{f_lbls}
+%{f_regs}
+#pc #id #def_in #s
+#H @('bind_inversion H) * #id' #def_in' -H
+#EQfif
+#H @('bind_inversion H) -H #s
+#H lapply (opt_eq_from_res ???? H) -H
+#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
+cases (props … EQfif)
+#a * #b #H %{a} %{b} %{H}
+cases H -H #_ #props'
+@(multi_fetch_ok … props' … EQstmt_at)
+qed.