Changeset 2595

Timestamp:

Jan 30, 2013, 7:25:39 PM (7 years ago)

Author:

tranquil

Message:

• dropped locals and exit from definition of joint_if_function
• new definition of blocks to accomodate ERTLptr pass
• stated properties of translation as axioms

Location:

src/joint

Files:

• Joint.ma (modified) (7 diffs)
• TranslateUtils.ma (modified) (12 diffs)
• blocks.ma (modified) (9 diffs)
• semantics.ma (modified) (4 diffs)
• semantics_blocks.ma (modified) (4 diffs)

src/joint/Joint.ma

@@ -88 +88 @@
  (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
  ; paramsT : Type[0]
- ; localsT: Type[0]
  }.
 
@@ -409 +408 @@
   joint_if_result   : call_dest p;
   joint_if_params   : paramsT p;
-  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
 (*CSC: XXXXX stacksize unused for LTL-...*)
   joint_if_stacksize: nat;
   joint_if_code     : codeT p globals ;
-  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;
-  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt)
+  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
+  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
 }.
 
@@ -431 +429 @@
   λgraph: codeT pars globals.
   λentry.
-  λexit.
+  (*λexit.*)
     mk_joint_internal_function pars globals
       (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
-      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
-      graph entry exit.
+      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
+      graph entry (*exit*).
 
 definition set_joint_if_graph ≝
@@ -442 +440 @@
   λp:joint_internal_function pars globals.
   λentry_prf.
-  λexit_prf.
+  (*λexit_prf.*)
     set_joint_code globals pars p 
       graph
       (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
-      (mk_Sig … (joint_if_exit ?? p) exit_prf).
+      (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
 
 definition set_luniverse ≝
@@ -454 +452 @@
    mk_joint_internal_function globals pars
     luniverse (joint_if_runiverse … p) (joint_if_result … p)
-    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
-    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
+    (joint_if_params … p) (joint_if_stacksize … p)
+    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
 
 definition set_runiverse ≝
@@ -463 +461 @@
    mk_joint_internal_function globals pars
     (joint_if_luniverse … p) runiverse (joint_if_result … p)
-    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
-    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
+    (joint_if_params … p) (joint_if_stacksize … p)
+    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
     
 (* Specialized for graph_params *)
@@ -473 +471 @@
     mk_joint_internal_function …
      (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
-     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
+     (joint_if_params … p) (joint_if_stacksize … p)
      code
      (pi1 … (joint_if_entry … p))
-     (pi1 … (joint_if_exit … p)).
+     (*(pi1 … (joint_if_exit … p))*).
 >graph_code_has_point whd in match code; >mem_set_add
-@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
+@orb_Prop_r elim (joint_if_entry ???)
 #x #H <graph_code_has_point @H
 qed. 
 
-definition set_locals ≝
-  λpars,globals.
-  λp : joint_internal_function pars globals.
-  λlocals.
-   mk_joint_internal_function pars globals
-    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
-    (joint_if_params … p) locals (joint_if_stacksize … p)
-    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
-
 definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
 

src/joint/TranslateUtils.ma

@@ -4 +4 @@
 include "utilities/deqsets.ma".
 
-(* general type of functions generating fresh things *)
-definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
-
-include alias "basics/lists/list.ma".
+(*include alias "basics/lists/list.ma".
 let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
   on n :
@@ -17 +14 @@
     ! reg ← fresh ;
     return «reg::regs',?»
-  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
+  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*)
 
 definition fresh_label:
- ∀g_pars,globals.freshT globals g_pars label ≝
+ ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝
   λg_pars,globals,def.
     let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
      〈set_luniverse … def luniverse, r〉.
+
+definition fresh_register:
+ ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝
+  λg_pars,globals,def.
+    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
+     〈set_runiverse … def runiverse, r〉.
 
 (* insert into a graph a block of instructions *)
@@ -29 +32 @@
   (g_pars: graph_params)
   (globals: list ident)
-  (insts: list (joint_seq g_pars globals))
-  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
-  match insts with
-  [ nil ⇒ return src
+  (insts: list (joint_step g_pars globals))
+  (src : label) (dst : label) on insts : joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
+  λdef.match insts with
+  [ nil ⇒ add_graph … src (sequential … (NOOP …) dst) def
   | cons instr others ⇒
-    ! mid ← fresh_label … ;
-    ! def ← state_get … ;
-    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
-    adds_graph_list g_pars globals others mid
-  ].
-
-definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
-  [ inl _ ⇒ true
-  | inr _ ⇒ false
-  ].
-definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
-  [ inl _ ⇒ true
-  | inr _ ⇒ false
+    match others with
+    [ nil ⇒ add_graph … src (sequential … instr dst) def
+    | _ ⇒
+      let 〈def', mid〉 ≝ fresh_label … def in
+      let def'' ≝ add_graph … src (sequential … instr mid) def' in
+      adds_graph_list … others mid dst def''
+    ]
   ].
 
@@ -52 +49 @@
   ∀g_pars : graph_params.
   ∀globals: list ident.
-  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
-       seq_block g_pars globals (joint_fin_step g_pars).
-  label → if is_inl … b then label else unit →
+  ∀b : step_block g_pars globals.
+  label → label →
   joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
-  λg_pars,globals,insts,src.
-  match insts return λx.if is_inl … x then ? else ? → ? → ? with
-  [ inl b ⇒ λdst,def.
-    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
-    add_graph … mid (sequential … (\snd b) dst) def
-  | inr b ⇒ λdst,def.
-    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
-    add_graph … mid (final … (\snd b)) def
+  λg_pars,globals,insts,src,dst,def.
+  let 〈pref, last〉 ≝ split_on_last_ne … insts in
+  match pref with
+  [ nil ⇒ add_graph … src (sequential … (last src) dst) def
+  | _ ⇒
+    let 〈def', lbl〉 ≝ fresh_label … def in
+    let def'' ≝ adds_graph_list … (map_eval … pref lbl) src lbl def' in
+    add_graph … lbl (sequential … (last lbl) dst) def''
+  ].
+
+definition fin_adds_graph :
+  ∀g_pars : graph_params.
+  ∀globals: list ident.
+  ∀b : fin_block g_pars globals.
+  label →
+  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
+  λg_pars,globals,insts,src,def.
+  let 〈pref, last〉 ≝ insts in
+  match pref with
+  [ nil ⇒ add_graph … src (final … last) def
+  | _ ⇒
+    let 〈def', lbl〉 ≝ fresh_label … def in
+    let def'' ≝ adds_graph_list … pref src lbl def' in
+    add_graph … lbl (final … last) def''
   ].
 
@@ -70 +82 @@
 definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
 λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
-
-lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
-#tag #A * #l * #m whd in ⊢ (%→?%);
-elim (lookup tag ???)
-[ * #ABS elim (ABS ?) %
-| #a #_ %
-] qed.
-
-lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
-#tag #A * #l * #m whd in ⊢ (?%→%);
-elim (lookup tag ???)
-[ * | #a * % #ABS destruct(ABS) ] qed.
 
 (*
@@ -114 +114 @@
 qed.
 
+lemma fresh_not_in_univ : ∀tag,id,u,u'.
+〈id, u'〉 = fresh tag u →
+¬fresh_for_univ tag id u.
+#tag * #id * #u * #u' normalize #EQ destruct //
+qed.
+
+lemma adds_graph_list_fresh_preserve :
+  ∀g_pars,globals,b,src,dst,def.
+  let def' ≝ adds_graph_list g_pars globals b src dst def in
+  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
+       fresh_for_univ … lbl (joint_if_luniverse … def').
+#g_pars #globals #l elim l -l
+[ #src #dst #def whd #lbl #H @H ]
+#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
+whd in match (adds_graph_list ??????);
+whd in match fresh_label; normalize nodelta
+inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
+normalize nodelta 
+@IH whd in match (joint_if_luniverse ???);
+@(fresh_remains_fresh … EQfresh) @H
+qed.
+
+lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
+#X * [2: #hd #tl ] #last % qed.
+
+lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
+(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
+P (split_on_last_ne X l).
+#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
+>split_on_last_ne_def @H % qed.
+
 (* use Russell? *)
-axiom adds_graph_list_ok :
-  ∀g_pars,globals,b,src,def.
+lemma adds_graph_list_ok :
+  ∀g_pars,globals,b,src,dst,def.
   fresh_for_univ … src (joint_if_luniverse … def) →
   luniverse_ok ?? def →
-  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
+  let def' ≝ adds_graph_list g_pars globals b src dst def in
   luniverse_ok ?? def' ∧
+  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
+                      stmt_at … (joint_if_code … def') lbl =
+                      stmt_at … (joint_if_code … def) lbl) ∧
+  let B ≝ ensure_step_block … b in
   ∃l.bool_to_Prop (uniqueb … l) ∧
-     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
-                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
-     src ~❨b,l❩~> dst in joint_if_code … def'.
-(*
-#p #g #l elim l -l
-[ #src #def #_ #Hdef whd
-  %{Hdef} %{[ ]} %%% ]
-#hd #tl #IH #src #def #src_fresh #Hdef
-whd in match (adds_graph_list ?????);
+    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+    src ~❨B,l❩~> dst in joint_if_code … def'.
+#p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
+#src #dst #def #Hsrc #Hdef
+[1,3: %
+  [1,3: %
+    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
+      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
+      >(lookup_add_miss ?????? H) @Hdef
+    |*: #lbl #H #G @lookup_add_miss @H
+    ]
+  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
+  ]
+]
+whd in match (adds_graph_list ??????);
 whd in match (fresh_label ???);
-@(pair_elim … (fresh ??)) normalize nodelta
-#mid #luniverse' #EQfresh
-whd in ⊢ (match % with [ _ ⇒ ?]);
-letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
-cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
-  [ % ] #EQ_aux
-  lapply (IH mid def' ??)
-  [ #l whd in match def'; #Hpres
-    lapply (present_to_memb … Hpres) -Hpres
-    >mem_set_add @eq_identifier_elim
-    [ #EQ destruct(EQ) *
-    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
-      #l_in
+inversion (fresh ??) normalize nodelta
+#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
+letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
+lapply (IH mid dst def' ??)
+[ #lbl @(eq_identifier_elim … lbl src) #H destruct
+  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
+    >(lookup_add_miss ?????? H) ]
+  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
+| whd in match def';
+  @(fresh_is_fresh … EQfresh)
+]
+whd in match (joint_if_luniverse ???);
+whd in match (joint_if_code ???);
+** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2 
+whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
+%
+[ %{Hdef''} #lbl #NEQ
+  @(eq_identifier_elim ?? lbl mid)
+  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
+  | #NEQ' #H >(stmt_preserved … NEQ')
+    [ whd in match (joint_if_code ???);
+      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
+    | @(fresh_remains_fresh … EQfresh) @H
     ]
-    @(fresh_remains_fresh … (sym_eq … EQfresh))
-    [2: @Hdef @memb_to_present ] assumption
-  | whd in match def';
-    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
-    whd in match (set_luniverse ????);
-    @(fresh_is_fresh … (sym_eq … EQfresh))
   ]
-  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
-  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
-  % [ % ]
-  [ whd in ⊢ (?%);
-    cut (Not (bool_to_Prop (mid∈l)))
-    [ % #H elim (All_memb … Hl2 H)
-      whd in match (joint_if_luniverse ???);
-      #G #_ @(absurd ?? G)
-      @ (fresh_is_fresh … (sym_eq … EQfresh))
-    | #H >H assumption
-    ]
-  | %
-    [ %
-      [ 
-      normalize #H10 #H11
-      
-    >(All_fresh_not_memb … (sym_eq … EQfresh))
-    [ assumption ]
-    @(All_mp … Hl2) #lbl *
-    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
-    normalize #EQfresh #H #lbl_not_mid
-    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
-    
-    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
-    [ normalize
-*)
+]
+%{(mid::l)}
+% [ % ]
+[ whd in ⊢ (?%);
+  cut (Not (bool_to_Prop (mid∈l)))
+  [ % #H elim (All_memb … Hl2 H)
+    whd in match (joint_if_luniverse ???);
+    #G #_ @(absurd ?? G)
+    @ (fresh_is_fresh … EQfresh)
+  | #H >H assumption
+  ]
+| %
+  [ %{(fresh_not_in_univ … EQfresh)}
+    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
+  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
+    @(fresh_remains_fresh … EQfresh) assumption
+  ]
+| whd in match (ensure_step_block ???) in EQ ⊢ %;
+  whd in match (map ??? (hd2 :: ?)); >EQ whd
+  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
+  %{mid'} % [2: @Hl4 ]
+  %{Hl3} %{mid} >stmt_preserved
+  [ % [2: % ] @lookup_add_hit
+  | @(fresh_remains_fresh … EQfresh) assumption
+  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
+  ]
+]
+qed.
+
+axiom adds_graph_ok :
+  ∀g_pars,globals,B,src,dst,def.
+  fresh_for_univ … src (joint_if_luniverse … def) →
+  luniverse_ok ?? def →
+  let def' ≝ adds_graph g_pars globals B src dst def in
+  luniverse_ok ?? def' ∧
+  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
+                      stmt_at … (joint_if_code … def') lbl =
+                      stmt_at … (joint_if_code … def) lbl) ∧
+  ∃l.bool_to_Prop (uniqueb … l) ∧
+    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+    src ~❨B,l❩~> dst in joint_if_code … def'.
+ 
+axiom fin_adds_graph_ok :
+  ∀g_pars,globals,B,src,def.
+  fresh_for_univ … src (joint_if_luniverse … def) →
+  luniverse_ok ?? def →
+  let def' ≝ fin_adds_graph g_pars globals B src def in
+  luniverse_ok ?? def' ∧
+  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
+                      stmt_at … (joint_if_code … def') lbl =
+                      stmt_at … (joint_if_code … def) lbl) ∧
+  ∃l.bool_to_Prop (uniqueb … l) ∧
+    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+    src ~❨B,l❩~> it in joint_if_code … def'.
 
 (* preserves first statement if a cost label (should be an invariant) *)
@@ -189 +265 @@
   with
   [ Some s ⇒ λ_.
+    let default_add ≝ λ_ : unit.
+      let 〈def', lbl〉 ≝ fresh_label … def in
+      let def'' ≝ add_graph … lbl s def' in
+      adds_graph … insts entry lbl def'' in
     match s with
     [ sequential s' next ⇒
@@ -195 +275 @@
         match s'' with
         [ COST_LABEL _ ⇒
-          adds_graph ?? (inl … (s'' :: insts)) entry next def
+          adds_graph ?? (s'' :: insts) entry next def
         | _ ⇒
-          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
-          add_graph … tmp s def'
+          default_add it
         ]
       | _ ⇒
-        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
-        add_graph … tmp s def'
+        default_add it
       ]
     | _ ⇒
-      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
-      add_graph … tmp s def'
+      default_add it
     ]
   | None ⇒ Ⓧ
   ] (pi2 … entry).
 
+(*
 definition insert_epilogue ≝
   λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
@@ -226 +304 @@
 whd in match def''; >graph_code_has_point //
 qed.
+*)
 
 definition b_adds_graph :
   ∀g_pars: graph_params.
   ∀globals: list ident.
-  (* fresh register creation *)
-  freshT g_pars globals (localsT … g_pars) →
-  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
-       bind_seq_block g_pars globals (joint_fin_step g_pars).
-  label → if is_inl … b then label else unit →
+  ∀b : bind_step_block g_pars globals.
+  label → label →
   joint_internal_function g_pars globals→
   joint_internal_function g_pars globals ≝
-  λg_pars,globals,fresh_r,insts,src.
-  match insts return λx.if is_inl … x then ? else ? → ? → ? with
-  [ inl b ⇒ λdst,def.
-    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
-    adds_graph … (inl … stmts) src dst def
-  | inr b ⇒ λdst,def.
-    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
-    adds_graph … (inr … stmts) src dst def
-  ].
-
-  
+  λg_pars,globals,insts,src,dst,def.
+  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
+  adds_graph … stmts src dst def.
+
+axiom b_adds_graph_ok :
+  ∀g_pars,globals,B,src,dst,def.
+  fresh_for_univ … src (joint_if_luniverse … def) →
+  luniverse_ok ?? def →
+  let def' ≝ b_adds_graph g_pars globals B src dst def in
+  luniverse_ok ?? def' ∧
+  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
+                      stmt_at … (joint_if_code … def') lbl =
+                      stmt_at … (joint_if_code … def) lbl) ∧
+  ∃l,r.
+    bool_to_Prop (uniqueb … l) ∧
+    bool_to_Prop (uniqueb … r) ∧
+    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
+                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
+    src ~❨B,l,r❩~> dst in joint_if_code … def'.
+ 
+definition b_fin_adds_graph :
+  ∀g_pars: graph_params.
+  ∀globals: list ident.
+  ∀b : bind_fin_block g_pars globals.
+  label →
+  joint_internal_function g_pars globals→
+  joint_internal_function g_pars globals ≝
+  λg_pars,globals,insts,src,def.
+  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
+  fin_adds_graph … stmts src def.
+
+axiom b_fin_adds_graph_ok :
+  ∀g_pars,globals,B,src,def.
+  fresh_for_univ … src (joint_if_luniverse … def) →
+  luniverse_ok ?? def →
+  let def' ≝ b_fin_adds_graph g_pars globals B src def in
+  luniverse_ok ?? def' ∧
+  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
+                      stmt_at … (joint_if_code … def') lbl =
+                      stmt_at … (joint_if_code … def) lbl) ∧
+  ∃l,r.
+    bool_to_Prop (uniqueb … l) ∧
+    bool_to_Prop (uniqueb … r) ∧
+    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
+                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
+    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
+                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
+    src ~❨B,l,r❩~> it in joint_if_code … def'.
 
 (* translation with inline fresh register allocation *)
@@ -253 +368 @@
   ∀src_g_pars,dst_g_pars : graph_params.
   ∀globals: list ident.
-  (* fresh register creation *)
-  freshT dst_g_pars globals (localsT dst_g_pars) →
   (* initialized function definition with empty graph *)
   joint_internal_function dst_g_pars globals →
   (* functions dictating the translation *)
-  (label → joint_step src_g_pars globals →
-    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
-  (label → joint_fin_step src_g_pars →
-    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
+  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
+  (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
   (* source function *)
   joint_internal_function src_g_pars globals →
   (* destination function *)
   joint_internal_function dst_g_pars globals ≝
-  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
+  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
   let f : label → joint_statement (src_g_pars : params) globals →
     joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
@@ -272 +383 @@
     match stmt with
     [ sequential inst next ⇒
-      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
+      b_adds_graph … (trans_step lbl inst) lbl next def
     | final inst ⇒
-      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
+      b_fin_adds_graph … (trans_fin_step lbl inst) lbl def
     | FCOND abs _ _ _ ⇒ Ⓧabs
     ] in
   foldi … f (joint_if_code … def) empty.
 
-(* translation without register allocation *)
+definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
+λX,Y,f.
+(∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧
+(∀x1,x2.
+  opt_All … 
+    (λys1.
+      opt_All …
+      (λys2.
+        ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)
+      (f x2))
+    (f x1)).
+
+lemma opt_All_intro : ∀X,P,o.
+(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
+ 
+(*
+definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
+λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).
+
+unification hint 0 ≔ p, g, def;
+points ≟ code_point p,
+code ≟ joint_if_code p g def,
+P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
+⊢
+points_of p g def ≡ Sig points P.
+
+definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
+  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
+@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
+*)
+
+axiom b_graph_translate_ok :
+  ∀src_g_pars,dst_g_pars : graph_params.
+  ∀globals: list ident.∀empty.∀f_step,f_fin,def_in.
+  luniverse_ok ?? def_in →
+  let def_out ≝
+    b_graph_translate src_g_pars dst_g_pars globals empty f_step f_fin def_in in
+  luniverse_ok … def_out ∧
+  joint_if_result … def_out = joint_if_result … empty ∧
+  joint_if_params … def_out = joint_if_params … empty ∧
+  joint_if_stacksize … def_out = joint_if_stacksize … empty ∧
+  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
+  ∃f_lbls : label → option (list label).
+  ∃f_regs : label → option (list register).
+  partial_partition … f_lbls ∧
+  partial_partition … f_regs ∧
+  (∀l.opt_All … (All …
+    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
+           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧
+  (∀l.opt_All … (All …
+    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
+           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧
+  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
+  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
+  match s with
+  [ sequential s' nxt ⇒
+    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
+  | final s' ⇒
+    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
+  | FCOND abs _ _ _ ⇒ Ⓧabs
+  ].
+
+definition added_registers :
+  ∀p : graph_params.∀g.
+  joint_internal_function p g → (label → option (list register)) → list register ≝
+  λp,g,def,f_regs.
+  let f ≝ λlbl : label.λ_.λacc.
+    match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
+  foldi … f (joint_if_code p g def) [ ].
+
+axiom added_registers_ok :
+  ∀p,g,def,f_regs.
+  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
+  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
+
+(* translation without register allocation (more or less an alias) *)
 definition graph_translate :
   ∀src_g_pars,dst_g_pars : graph_params.
@@ -286 +472 @@
   joint_internal_function dst_g_pars globals →
   (* functions dictating the translation *)
-  (label → joint_step src_g_pars globals →
-    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
-  (label → joint_fin_step src_g_pars →
-    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
+  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
+  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
   (* source function *)
   joint_internal_function src_g_pars globals →
   (* destination function *)
   joint_internal_function dst_g_pars globals ≝ 
-  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
-  let f : label → joint_statement (src_g_pars : params) globals →
-    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
-    λlbl,stmt,def.
-    match stmt with
-    [ sequential inst next ⇒
-      adds_graph … (inl … (trans_step lbl inst)) lbl next def
-    | final inst ⇒
-      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
-    | FCOND abs _ _ _ ⇒ Ⓧabs
-    ] in
-  foldi … f (joint_if_code … def) empty.
-
+  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step.
+  b_graph_translate … empty
+    (λl,s.return trans_step l s)
+    (λl,s.return trans_fin_step l s).
+
+(* helper for initializing a valid init graph (with a valid entry) *)
 definition init_graph_if ≝ 
   λg_pars : graph_params.λglobals.
-  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
-  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
-  let graph ≝ add ? ? graph exit (RETURN …) in
+  λluniverse,runiverse,ret,params,stack_size,entry.
+  let graph ≝ add ?? (empty_map ? (joint_statement ??)) entry (RETURN …) in
   mk_joint_internal_function g_pars globals
-    luniverse runiverse ret params locals stack_size
-    graph entry exit.
->graph_code_has_point @map_mem_prop
-[@graph_add_lookup] @graph_add
+    luniverse runiverse ret params stack_size
+    graph entry.
+@hide_prf >graph_code_has_point @map_mem_prop @graph_add
 qed.
 

src/joint/blocks.ma

@@ -42 +42 @@
   (list (block_step p globals)) × A.*)
 
-definition seq_block ≝ λp : stmt_params.λglobals,A.
-  (list (joint_seq p globals)) × A.
+(* move *)
+let rec bind_new_P R X (P : X → Prop) (b : bind_new R X) on b : Prop ≝
+match b with
+[ bret x ⇒ P x
+| bnew f ⇒ ∀x.bind_new_P … P (f x)
+].
+
+definition BindNewP : ∀R.MonadPred (BindNew R) ≝
+λR.mk_MonadPred (BindNew R) (bind_new_P R) ???.
+[ #X #P #x #K @K
+| #X #Y #Pin #Pout #m elim m -m
+  [ #x #H #f #G @G @H
+  | #g #IH #H #f #G #x @IH [ @H | @G ]
+  ]
+| #X #P #Q #H #m elim m -m
+  [ #x #Px @H @Px
+  | #g #IH #Pg #x @IH @Pg
+  ]
+]
+qed.
+
+definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ].
+
+definition head_ne : ∀X.(Σl.not_empty X l) → X ≝
+λX,l.
+match l return λl.not_empty ? l → ? with
+[ nil ⇒ Ⓧ
+| cons hd _ ⇒ λ_.hd
+] (pi2 … l).
+
+
+let rec split_on_last_ne_aux X l on l : not_empty X l → (list X) × X ≝
+match l return λx.not_empty ? x → ? with
+[ nil ⇒ Ⓧ
+| cons hd tl ⇒ λ_.
+  match tl return λtl.(not_empty X tl → ?) → ? with
+  [ nil ⇒ λ_.〈[ ], hd〉
+  | cons hd' tl' ⇒ λrec_call.let 〈pre, last〉 ≝ rec_call I in 〈hd :: pre, last〉
+  ] (split_on_last_ne_aux ? tl)
+].
+
+definition split_on_last_ne : ∀X.(Σl.not_empty X l) → (list X)×X ≝
+λX,l.split_on_last_ne_aux … (pi2 … l).
+
+definition last_ne : ∀X.(Σl.not_empty X l) → X ≝ λX,l.\snd (split_on_last_ne … l).
+definition chop_last_ne : ∀X.(Σl.not_empty X l) → list X ≝ λX,l.\fst (split_on_last_ne … l).
+
+lemma split_on_last_ne_def : ∀X,pre,last,prf.split_on_last_ne X «pre@[last], prf» = 〈pre, last〉.
+whd in match split_on_last_ne; normalize nodelta
+#X #pre elim pre -pre [ #last #prf % ]
+#hd * [2: #hd' #tl'] #IH #last *
+[ whd in ⊢ (??%?); >IH % | % ]
+qed.
+
+lemma split_on_last_ne_inv : ∀X,l.
+pi1 ?? l = (let 〈pre, last〉 ≝ split_on_last_ne X l in pre @ [last]).
+whd in match split_on_last_ne; normalize nodelta
+#X * #l elim l -l [ * ]
+#hd * [2: #hd' #tl'] #IH * [2: % ]
+whd in match (split_on_last_ne_aux ???);
+lapply (IH I) @pair_elim #pre #last #_ #EQ >EQ %
+qed.
+
+(* the label input is to accomodate ERTptr pass *)
+definition step_block ≝ λp,globals.Σl : list (code_point p → joint_step p globals).not_empty ? l.
+unification hint 0 ≔ p : params, g;
+S ≟ code_point p → joint_step p g,
+L ≟ list S,
+P ≟ not_empty S
+(*---------------------------------------*)⊢
+step_block p g ≡ Sig L P.
+
+definition fin_block ≝ λp,globals.(list (joint_step p globals))×(joint_fin_step p).
 
 (*definition seq_to_skip_block :
@@ -53 +124 @@
   seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
 
-definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
-  bind_new (localsT p) (seq_block p globals A).
-unification hint 0 ≔ p : stmt_params, g, X;
-R ≟ localsT p,
-P ≟ seq_block p g X
+definition bind_step_block ≝ λp.λglobals.
+  bind_new register (step_block p globals).
+
+unification hint 0 ≔ p, g;
+P ≟ step_block p g
 (*---------------------------------------*)⊢
-bind_seq_block p g X ≡ bind_new R P.
-
-definition bind_seq_list ≝ λp : stmt_params.λglobals.
-  bind_new (localsT p) (list (joint_seq p globals)).
+bind_step_block p g ≡ bind_new register P.
+
+definition bind_fin_block ≝ λp : stmt_params.λglobals.
+  bind_new register (fin_block p globals).
+
 unification hint 0 ≔ p : stmt_params, g;
-R ≟ localsT p,
-S ≟ joint_seq p g,
+P ≟ fin_block p g
+(*---------------------------------------*)⊢
+bind_fin_block p g ≡ bind_new register P.
+
+definition bind_step_list ≝ λp : stmt_params.λglobals.
+  bind_new register (list (joint_step p globals)).
+unification hint 0 ≔ p : stmt_params, g;
+S ≟ joint_step p g,
 L ≟ list S
 (*---------------------------------------*)⊢
-bind_seq_list p g ≡ bind_new R L.
+bind_step_list p g ≡ bind_new register L.
+
+definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x).
+
+definition ensure_step_block : ∀p : params.∀globals.
+list (joint_step p globals) → step_block p globals ≝
+λp,g,l.match add_dummy_variance … l return λ_.Σl.not_empty ? l with
+[ nil ⇒ «[λ_.NOOP ??], I»
+| cons hd tl ⇒ «hd :: tl, I»
+].
+
+definition ensure_step_list : ∀p,globals.
+list (joint_seq p globals) → list (joint_step p globals) ≝
+λp,g.map … (step_seq …).
+
+definition ensure_step_block_from_seq : ∀p : params.∀globals.
+list (joint_seq p globals) → step_block p globals ≝
+λp,g.ensure_step_block ?? ∘ ensure_step_list ??.
+
+coercion step_block_from_list nocomposites : ∀p : params.∀g.∀l : list (joint_step p g).step_block p g ≝
+ensure_step_block on _l : list (joint_step ??) to step_block ??.
+
+coercion step_list_from_seq nocomposites : ∀p,g.∀l : list (joint_seq p g).list (joint_step p g) ≝
+ensure_step_list on _l : list (joint_seq ??) to list (joint_step ??).
+
+coercion step_block_from_seq nocomposites : ∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
+ensure_step_block_from_seq on _l : list (joint_seq ??) to step_block ??.
+
 
 (*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
@@ -90 +195 @@
   seq_or_fin_step_classifier ?? (\snd b).
 *)
-
-let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
-match l with
-[ nil ⇒ 〈[ ], dflt〉
-| cons hd tl ⇒
-  match tl with
-  [ nil ⇒ 〈[ ], hd〉
-  | _ ⇒
-    let 〈pref, post〉 ≝ split_on_last A dflt tl in
-    〈hd :: pref, post〉
-  ]
-].
-
-lemma split_on_last_ok :
-  ∀A,dflt,l.
-  match l with
-  [ nil ⇒ True
-  | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post])
-  ].
-#A #dflt #l elim l normalize nodelta
-[ %
-| #hd * [ #_ %]
-  #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?);
-  elim (split_on_last ???) #a #b %
-]
-qed.
-
-definition seq_block_from_seq_list :
+(*definition seq_block_from_seq_list :
 ∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
 λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
@@ -176 +254 @@
   ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
   bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
+*)
 
 notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
@@ -183 +262 @@
   @{'block_in_code $c $x $B $l $y}.
 
+notation > "x ~❨ B , l, r ❩~> y 'in' c" with precedence 56 for
+  @{'bind_block_in_code $c $x $B $l $r $y}.
+  
+notation < "hvbox(x ~❨ B , l, r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
+  @{'bind_block_in_code $c $x $B $l $r $y}.
+
 definition step_in_code ≝
   λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
@@ -193 +278 @@
   stmt_at … c src = Some ? (final … s).
 
-let rec seq_list_in_code p globals (c : codeT p globals)
-  (src : code_point p) (B : list (joint_seq p globals))
+let rec step_list_in_code p globals (c : codeT p globals)
+  (src : code_point p) (B : list (joint_step p globals))
   (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
   match B with
@@ -206 +291 @@
     [ nil ⇒ False
     | cons mid rest ⇒
-      step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
+      step_in_code …  c src hd mid ∧ step_list_in_code … c mid tl rest dst
     ]
   ].
 
-interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
-
-lemma seq_list_in_code_append :
+interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
+
+lemma step_list_in_code_append :
   ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
   src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
@@ -224 +309 @@
 qed.
 
-lemma seq_list_in_code_append_inv :
+lemma step_list_in_code_append_inv :
   ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
   src ~❨B1@B2,l❩~> dst in c →
   ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
-#p #globals #c #src #B1 lapply src -src elim B1
+#p #globals #c #src #B1 lapply src -src elim B1 -B1
 [ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
 | #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
@@ -237 +322 @@
 qed.
 
-definition seq_block_step_in_code ≝
-  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
-  ∃hd,tl.l = hd @ [tl] ∧
-  src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
-
-definition seq_block_fin_step_in_code ≝
-  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
+lemma append_not_empty_r : ∀X,l1,l2.not_empty X l2 → not_empty ? (l1 @ l2).
+#X #l1 cases l1 -l1 [ #l2 #K @K | #hd #tl #l2 #_ % ] qed.
+
+definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l.
+
+definition step_block_in_code ≝
+  λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst.
+  let 〈pref, last〉 ≝ split_on_last_ne … b in
+  ∃mid.src ~❨map_eval … pref mid, l❩~> mid in c ∧ step_in_code ?? c mid (last mid) dst.
+
+lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l.
+#X #Y #Z #f #g #l elim l -l normalize // qed.
+
+lemma map_ext_eq : ∀X,Y,f,g.∀l : list X.(∀x.f x = g x) → map X Y f l = map X Y g l.
+#X #Y #f #g #l #H elim l -l normalize // qed.
+
+lemma map_id : ∀X.∀l : list X.map X X (λx.x) l = l.
+#X #l elim l -l normalize // qed.
+
+lemma coerced_step_list_in_code :
+∀p : params.∀g,c,src.∀b : list (joint_step p g).∀l,dst.
+step_block_in_code p g c src b l dst →
+match b with
+[ nil ⇒ step_in_code … c src (NOOP …) dst
+| _ ⇒ step_list_in_code … c src b (l@[dst]) dst
+].
+#p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst
+[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K @K ]
+cases pref -pref [2: #hd #tl ]
+whd in ⊢ (%→?);
+[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K %{K} % ]
+whd in match (ensure_step_block ???);
+<map_append
+change with ((? :: ?) @ ?) in match (? :: ? @ ?);
+>split_on_last_ne_def normalize nodelta * #mid *
+whd in match (map_eval ????);
+>map_compose >map_id #H1 #H2
+@(step_list_in_code_append … H1) %{H2} %
+qed.
+
+definition fin_block_in_code ≝
+  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
   ∃hd,tl.l = hd @ [tl] ∧
   src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
+
+interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
+interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
+
+let rec bind_new_instantiates B X
+  (x : X) (b : bind_new B X) (l : list B) on b : Prop ≝
+  match b with
+  [ bret B ⇒
+    match l with
+    [ nil ⇒ x = B
+    | _ ⇒ False
+    ]
+  | bnew f ⇒
+    match l with
+    [ nil ⇒ False
+    | cons r l' ⇒
+      bind_new_instantiates B X x (f r) l'
+    ]
+  ].
+
+definition bind_step_block_in_code ≝
+  λp,g.λc:codeT p g.λsrc.λB : bind_step_block p g.λlbls,regs.λdst.
+  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
+
+definition bind_fin_block_in_code ≝
+  λp,g.λc:codeT p g.λsrc.λB : bind_fin_block p g.λlbls,regs.λdst.
+  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
+
+interpretation "bound step block in code" 'bind_block_in_code c x B l r y = (bind_step_block_in_code ?? c x B l r y).
+interpretation "bound fin block in code" 'bind_block_in_code c x B l r y = (bind_fin_block_in_code ?? c x B l r y).
 
 (* generates ambiguity even if it shouldn't

src/joint/semantics.ma

@@ -197 +197 @@
   
   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
-  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
+  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
   ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    (*CSC: setup_call returns a res only because we can call a function with the wrong number and
@@ -218 +218 @@
   }.
 
+(*
 definition allocate_locals :
   ∀p,F.∀sup : sem_unserialized_params p F.
@@ -223 +224 @@
   λp,F,sup,l,st.
   let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
-  set_regs … r st. 
+  set_regs … r st. *)
 
 definition helper_def_retrieve : 
@@ -526 +527 @@
 
 definition eval_internal_call ≝
-λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
+λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
+λst : state p.
 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
-! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
-return allocate_locals … p (joint_if_locals … fn) st'.
+setup_call … stack_size (joint_if_params … globals fn) args st.
 
 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].

src/joint/semantics_blocks.ma

@@ -2 +2 @@
 include "joint/Traces.ma".
 include "joint/semanticsUtils.ma".
+
+include "common/StatusSimulation.ma". (* for trace_any_any_free *)
 
 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
@@ -13 +15 @@
   m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
 
-definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
+definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
+  as_execute S s1 s2 →
+  as_classifier … s1 cl_other →
+  ∀taaf : trace_any_any_free S s2 s3.
+  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
+  trace_any_any_free S s1 s3 ≝
+λS,s1,s2,s3,H,I,tl.
+match tl return λs2,s3,tl.
+  as_execute … s1 s2 →
+  if taaf_non_empty … tl then ¬as_costed … s2 else True →
+  trace_any_any_free S s1 s3 
+with
+[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
+| taaf_step s2 s3 s4 taa H' I' ⇒
+  λH,J.taaf_step … (taa_step … H I J taa) H' I'
+| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
+  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
+] H.
 
-let rec produce_trace_any_any
+lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
+bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
+#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
+[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
+qed.
+
+let rec produce_trace_any_any_free_aux
   (p : evaluation_params)
   (st : state_pc p)
@@ -26 +51 @@
     return 〈curr_id, curr_fn〉 →
   let src ≝ point_of_pc p (pc … st) in
-  if list_not_empty ? b then
-    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
-  else
-    True →
+  (* disambiguation: select 3rd (step list in code) *)
   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
-  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
+  All ? (no_cost_label …) b →
   repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
-  trace_any_any (joint_abstract_status p) st
-    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
-  return λb.∀l,dst.?→?→?→?→?→?→?
+  Σtaaf : trace_any_any_free (joint_abstract_status p) st
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
+  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
+  match b
+  return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
   with
   [ nil ⇒
-    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
-    (taa_base (joint_abstract_status p) st)
-    ⌈trace_any_any ??? ↦ ?⌉
+    λl,dst,st',fd_prf,in_code,all_other,EQ1.
+    «taaf_base (joint_abstract_status p) st
+    ⌈trace_any_any_free ??? ↦ ?⌉,?»
   | cons hd tl ⇒
     λl.
-    match l return λx.∀dst,st'.?→?→?→?→?→? with
-    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
+    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
+    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
     | cons mid rest ⇒
-      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
+      λdst,st',fd_prf,in_code,all_other,EQ1.
       let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
       match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
       return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
-      trace_any_any (joint_abstract_status p) st
-        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
-      [ Value st_mid ⇒ λEQ2.
-        let tr_tl ≝ produce_trace_any_any ?
-            (mk_state_pc ? st_mid mid_pc)
-            curr_id curr_fn tl rest dst ?????? in
-        taa_step … tr_tl
+      Σtaaf : trace_any_any_free (joint_abstract_status p) st
+        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
+        (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
+      [ OK st_mid ⇒ λEQ2.
+        let tr_tl ≝ produce_trace_any_any_free_aux ?
+            (mk_state_pc ? st_mid mid_pc (last_pop … st))
+            curr_id curr_fn tl rest dst ????? in
+        «taaf_cons … tr_tl ?,?»
       | _ ⇒ λEQ2.⊥
       ] (refl …)
     ]
-  ].
-[ whd in EQ1 : (??%%);
-  cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
-  >pc_of_point_of_pc cases st //
+  ]. @hide_prf
+[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
+  whd in EQ1 : (??%%);
+  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
+  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
 | @in_code
-|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
+|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
+|4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
+  [ #_ #_ * #_ cases (taaf_non_empty ????)
+    [ #ABS cases (ABS I) | #_ % ]
+  | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
+    * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
+    #_ * #H #_ >(H I) % whd in ⊢ (%→?);
+    whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
+    >fetch_statement_eq [2: whd in match point_of_pc;
+    normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
+    normalize nodelta
+    >(no_label_uncosted … hd_other') * #ABS @ABS %
+  ]
+|7: % [2: #_ %] * @taaf_cons_non_empty
 ]
 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
 >EQ2 in EQ1; >m_return_bind
 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
-cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
+cases all_other -all_other #hd_no_cost #tl_other
 #EQ1
 try assumption
-[ whd whd in match eval_state; normalize nodelta
+[2: whd whd in match eval_state; normalize nodelta
   >(fetch_statement_eq … fd_prf EQ_stmt_at)
   >m_return_bind
@@ -79 +118 @@
   >EQ2 >m_return_bind
   whd in match eval_statement_advance; normalize nodelta
-  >(no_call_advance … hd_no_call)
   whd in match next; normalize nodelta 
   whd in match succ_pc; normalize nodelta
   >EQ_mid %
-| whd whd in ⊢ (??%?);
-  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
-  @(no_call_other … hd_no_call)
-| whd in ⊢ (?%);
-  whd in match as_label; normalize nodelta
-  %* #H @H -H whd in ⊢ (??%?);
-  whd in match (as_pc_of ??);
-  inversion (fetch_statement ????) normalize nodelta
-  [2: // ]
-  ** #i' #f' #stmt' #EQ
-  elim (fetch_statement_inv … EQ)
-  >fd_prf
-  whd in ⊢ (??%?→?); #EQ destruct(EQ)
-  whd in ⊢ (%→?);
-  whd in match (point_of_pc ??); >point_of_offset_of_point
-  #EQ'
-  cases tl in tl_other rest_in_code;
-  [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
-    >EQ' in dst_prf; >m_return_bind #H @H
-  | #hd' #tl' ** #_ #hd_no_cost' #_
-    cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
-    >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
-    @(no_label_uncosted … hd_no_cost')
-  ]
-| >dst_prf cases (list_not_empty ??) %
-| normalize nodelta >point_of_pc_of_point assumption
+|1: whd whd in ⊢ (??%?);
+  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
+|3: normalize nodelta >point_of_pc_of_point assumption
 ]
 qed.
+
+definition produce_trace_any_any_free :
+  ∀p : evaluation_params.
+  ∀st : state_pc p.
+  ∀curr_id,curr_fn.
+  ∀b : list (joint_seq p (globals p)).
+  ∀l : list (code_point p).
+  ∀dst : code_point p.
+  ∀st' : state p.
+  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
+    return 〈curr_id, curr_fn〉 →
+  let src ≝ point_of_pc p (pc … st) in
+  (* disambiguation: select 3rd (step list in code) *)
+  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
+  All ? (no_cost_label …) b →
+  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
+  trace_any_any_free (joint_abstract_status p) st
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
+  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
+  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.