source: LTS/Vm.ma @ 3463

include "costs.ma".
include "basics/lists/list.ma".
include "../src/utilities/option.ma".
include "basics/jmeq.ma".

lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
∀f : A → option B.∀y : B.
! x ← m; f x = return y → 
∃ x.(m = return x) ∧ (f x = return y).
#A #B * [| #a] #f #y normalize #EQ [destruct]
%{a} %{(refl …)} //
qed.

record assembler_params : Type[1] ≝ 
{ seq_instr : Type[0]
; jump_condition : Type[0] 
; io_instr : Type[0] 
; entry_of_function : FunctionName → ℕ
; call_label_fun : list (ℕ × CallCostLabel)
; return_label_fun : list (ℕ × ReturnPostCostLabel)
}.

inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
| Ijmp: ℕ → AssemblerInstr p
| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
| Icall: FunctionName → AssemblerInstr p
| Iret: AssemblerInstr p.

record AssemblerProgram (p : assembler_params) : Type[0] ≝ 
{ instructions : list (AssemblerInstr p)
; endmain : ℕ
; endmain_ok : endmain ≤ |instructions|
}.

definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
 λp,l,n. nth_opt ? n (instructions … l).

definition stackT: Type[0] ≝ list (nat).

record sem_params (p : assembler_params) : Type[1] ≝ 
{ m : monoid
; asm_store_type : Type[0]
; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
; eval_asm_cond : jump_condition p → asm_store_type → option bool
; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
; cost_of_io : io_instr p → asm_store_type → m
; cost_of : AssemblerInstr p → asm_store_type →  m
}.

record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ 
{ pc : ℕ
; asm_stack : stackT
; asm_store : asm_store_type … p'
; asm_is_io : bool
; cost : m … p'
}.

definition label_of_pc ≝ λL.λl.λpc.find … 
   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
   
definition option_pop ≝ 
  λA.λl:list A. match l with
  [ nil ⇒ None ?
  | cons a tl ⇒ Some ? (〈a,tl〉) ].


inductive vmstep (p : assembler_params) (p' : sem_params p) 
   (prog : AssemblerProgram p)  : 
      ActionLabel → relation (vm_state p p') ≝ 
| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
           fetch … prog (pc … st1) = return (Seq p i l) → 
           asm_is_io … st1 = false → 
           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 →  
           asm_stack … st1 = asm_stack … st2 → 
           asm_is_io … st1 = asm_is_io … st2 → 
           S (pc … st1) = pc … st2 → 
           op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 → 
           vmstep … (cost_act l) st1 st2
| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. 
           fetch … prog (pc … st1) = return (Ijmp p new_pc) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           asm_stack … st1 = asm_stack … st2 → 
           asm_is_io … st1 = asm_is_io … st2 → 
           new_pc = pc … st2 → 
           op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 → 
           vmstep … (cost_act (None ?)) st1 st2
| vm_cjump_true : 
           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
           eval_asm_cond p p' cond (asm_store … st1) = return true→ 
           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           asm_stack … st1 = asm_stack … st2 → 
           asm_is_io … st1 = asm_is_io … st2 → 
           pc … st2 = new_pc → 
           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 
           vmstep … (cost_act (Some ? ltrue)) st1 st2
| vm_cjump_false : 
           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
           eval_asm_cond p p' cond (asm_store … st1) = return false→ 
           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           asm_stack … st1 = asm_stack … st2 → 
           asm_is_io … st1 = asm_is_io … st2 → 
           S (pc … st1) = pc … st2 → 
           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 
           vmstep … (cost_act (Some ? lfalse)) st1 st2
| vm_io_in :  
           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
           fetch … prog (pc … st1) = return (Iio p lin io lout) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           asm_stack … st1 = asm_stack … st2 → 
           true = asm_is_io … st2 → 
           pc … st1 = pc … st2 → 
           cost … st1 = cost … st2 → 
           vmstep … (cost_act (Some ? lin)) st1 st2
| vm_io_out : 
           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
           fetch … prog (pc … st1) = return (Iio p lin io lout) → 
           asm_is_io … st1 = true → 
           eval_asm_io … io (asm_store … st1) = return asm_store … st2 → 
           asm_stack … st1 = asm_stack … st2 → 
           false = asm_is_io … st2 → 
           S (pc … st1) = pc … st2 → 
           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 → 
           vmstep … (cost_act (Some ? lout)) st1 st2
| vm_call : 
           ∀st1,st2 : vm_state p p'.∀f,lbl.
           fetch … prog (pc … st1) = return (Icall p f) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 → 
           asm_is_io … st1 = asm_is_io … st2 → 
           entry_of_function p  f = pc … st2 → 
           op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → 
           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl → 
           vmstep … (call_act f lbl) st1 st2
| vm_ret :
          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
           fetch … prog (pc … st1) = return (Iret p) → 
           asm_is_io … st1 = false → 
           asm_store … st1 = asm_store … st2 → 
           asm_stack … st1 = newpc ::  asm_stack … st2  → 
           asm_is_io … st1 = asm_is_io … st2 → 
           newpc = pc … st2 → 
           label_of_pc ? (return_label_fun p) newpc = return lbl → 
           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → 
           vmstep … (ret_act (Some ? lbl)) st1 st2.

definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 
AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ 
λp,p',prog,st.
! i ← fetch … prog (pc … st);
match i with
[ Seq x opt_l ⇒ 
   if asm_is_io … st then
     None ?
   else 
     ! new_store ← eval_asm_seq p p' x (asm_store … st);
     return 〈cost_act opt_l,
             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
                (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
| Ijmp newpc ⇒ 
   if asm_is_io … st then
     None ?
   else
     return 〈cost_act (None ?),
             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
                (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
| CJump cond newpc ltrue lfalse ⇒ 
   if asm_is_io … st then
     None ?
   else
     ! b ← eval_asm_cond p p' cond (asm_store … st);
     if b then
       return 〈cost_act (Some ? ltrue),
               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
     else
       return 〈cost_act (Some ? lfalse),
               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
| Iio lin io lout ⇒ 
              if asm_is_io … st then 
                 ! new_store ← eval_asm_io … io (asm_store … st);
                 return 〈cost_act (Some ? lout),
                         mk_vm_state ?? (S (pc … st)) (asm_stack … st) 
                         new_store false
                         (op … (cost … st) 
                               (cost_of_io p p' io (asm_store … st)))〉    
              else 
                return 〈cost_act (Some ? lin),
                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
                                    true (cost … st)〉
| Icall f ⇒ 
    if asm_is_io … st then
      None ?
    else
      ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
      return 〈call_act f lbl,
              mk_vm_state ?? (entry_of_function p f) 
                             ((S (pc … st)) :: (asm_stack … st))
                             (asm_store … st) false
                             (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
| Iret ⇒ if asm_is_io … st then
            None ?
         else
            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
            ! lbl ← label_of_pc ? (return_label_fun p) newpc;
            return 〈ret_act (Some ? lbl),
                    mk_vm_state ?? newpc tl (asm_store … st) false   
                     (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
].

lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
#p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
#H cases(bind_inversion ????? H) -H * normalize nodelta
[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
  @vm_seq //
| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
  @vm_ijump //
| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
  whd in ⊢ (??%% → ?); #EQ destruct
  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
]
qed.

 
lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → 
eval_vmstate p p' prog st1 = return 〈l,st2〉.
#p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
* #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
  >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
  >EQstore >EQstack <EQcost >EQstore %
|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
  #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind 
  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
   #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
   normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
   >EQstore >m_return_bind <EQpc <EQio2 %
| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
  #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
  normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
  <EQstack >EQstore %
| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
  #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
  >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
]
qed.

coercion vm_step_to_eval.

include "../src/utilities/hide.ma".

discriminator option.

definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝ 
λp,p',prog.mk_abstract_status 
                (vm_state p p') 
                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧ 
                               vmstep p p' prog l st1 st2) 
                (λ_.λ_.True)
                (λs.match fetch … prog (pc … s) with
                    [ Some i ⇒ match i with 
                               [ Seq _ _ ⇒ cl_other
                               | Ijmp _ ⇒ cl_other
                               | CJump _ _ _ _ ⇒ cl_jump
                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
                               | Icall _ ⇒ cl_other 
                               | Iret ⇒ cl_other
                               ]
                    | None ⇒ cl_other
                    ]
                ) 
                (λ_.true) 
                (λs.eqb (pc ?? s) O)
                (λs.eqb (pc … s) (endmain … prog))
                ???.
@hide_prf
[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
  [ #_ #EQ destruct] * normalize nodelta
  [ #seq #lbl #_
  | #n #_
  | #cond #newpc #ltrue #lfalse #EQfetch
  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
  | #f #_
  | #_
  ]
  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
  normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??)
  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
  * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
| #s1 #s2 #l inversion(fetch ???) normalize nodelta
  [ #_ #EQ destruct] * normalize nodelta
  [ #seq #lbl #_
  | #n #_
  | #cond #newpc #ltrue #lfalse #_
  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
  | #f #_
  | #_
  ]
  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
  normalize nodelta #H cases(bind_inversion ????? H) -H *
  [ #seq1 #lbl1 
  | #n1
  | #cond1 #newpc1 #ltrue1 #lfalse1
  | #lin1 #io1 #lout1
  | #f 
  |
  ]
  normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta
  [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct
  |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ 
    [2: cases x normalize nodelta
    |5: #H cases(bind_inversion ????? H) -H #y * #_ 
    ]
  ] 
  whd in ⊢ (??%% → ?); #EQ destruct destruct % //
|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
  [ #_ #EQ destruct] * normalize nodelta
  [ #seq #lbl #_
  | #n #_
  | #cond #newpc #ltrue #lfalse #_
  | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio
  | #f #_
  | #_
  ]
  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
  normalize nodelta  >EQfetch >m_return_bind normalize nodelta >EQio
  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ 
  whd in ⊢ (??%% → ?); #EQ destruct % //
qed.

definition asm_concrete_trans_sys ≝ 
λp,p',prog.mk_concrete_transition_sys … 
             (asm_operational_semantics p p' prog) (m … p') (cost …).

definition emits_labels ≝ 
λp.λinstr : AssemblerInstr p.match instr with
        [ Seq _ opt_l ⇒ match opt_l with 
                        [ None ⇒ Some ? (λpc.S pc) 
                        | Some _ ⇒ None ?
                        ] 
        | Ijmp newpc ⇒ Some ? (λ_.newpc)
        | _ ⇒ None ?
        ]. 

definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝ 
λp,p',prog,st.fetch … prog (pc … st).

definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t 
 … (fetch_state p p' prog) instr_m.

definition non_empty_list : ∀A.list A → bool ≝ 
λA,l.match l with [ nil ⇒ false | _ ⇒  true ].

let rec block_cost (p : assembler_params) 
 (prog: AssemblerProgram p) (abs_t : monoid) 
 (instr_m : AssemblerInstr p → abs_t)
 (program_counter: ℕ) 
    (program_size: ℕ) 
        on program_size: option abs_t ≝
match program_size with
  [ O ⇒ None ?
  | S program_size' ⇒ 
    if eqb program_counter (endmain … prog) then
       return e … abs_t
    else
    ! instr ← fetch … prog program_counter;
    ! n ← (match emits_labels … instr with
          [ Some f ⇒ block_cost … prog abs_t instr_m (f program_counter) program_size'
          | None ⇒ return e …
          ]);
    return (op … abs_t (instr_m … instr) n) 
  ].
 
inductive InitCostLabel : Type[0] ≝ 
  costlab : CostLabel → InitCostLabel
| initial_act : InitCostLabel.

definition eq_init_costlabel ≝ (λi1,i2.match i1 with
 [ initial_act ⇒ match i2 with [initial_act ⇒ true | _ ⇒ false ]
 | costlab c ⇒ match i2 with [costlab c1 ⇒ c == c1 | _ ⇒ false ]
 ]).

definition DEQInitCostLabel ≝ mk_DeqSet InitCostLabel eq_init_costlabel ?.
* [#c] * [1,3: #c1] whd in match eq_init_costlabel; normalize nodelta 
[4: /2/ | 2,3: % #EQ destruct] % [ #H >(\P H) % | #EQ destruct >(\b (refl …)) %]
qed.

coercion costlab.

definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝ 
map … costlab.

coercion list_cost_to_list_initcost.
  
record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ 
{ map_type :> Type[0]
; empty_map : map_type
; get_map : map_type → dom → option codom
; set_map : map_type → dom → codom → map_type
; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
}.

definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝ 
λp,i,program_counter.
match i with
  [ Seq _ opt_l ⇒ match opt_l with 
                  [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
                  | None ⇒ [ ]
                  ]
  | Ijmp _ ⇒ [ ]
  | CJump _ newpc ltrue lfalse ⇒ [〈costlab (a_non_functional_label ltrue),newpc〉;
                                  〈costlab (a_non_functional_label lfalse),S program_counter〉]
  | Iio lin _ lout ⇒ [〈costlab (a_non_functional_label lin),program_counter〉;
                      〈costlab (a_non_functional_label lout),S program_counter〉]
  | Icall f ⇒ [ ]
  | Iret ⇒ [ ]
  ].

let rec labels_pc (p : assembler_params)
(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝ 
match prog with
[ nil ⇒ [〈initial_act,O〉] @ 
        map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_call z),y〉) (call_label_fun … p) @
        map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_return_post z),y〉) (return_label_fun … p)
| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
].

lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m.
fetch p prog pc = return i →
mem ? lbl (labels_pc_of_instr … i (m+pc)) → 
mem ? lbl (labels_pc p (instructions … prog) m).
#p * #instrs #end_main #Hend_main #i #lbl #pc 
whd in match fetch; normalize nodelta lapply pc -pc
-end_main elim instrs
[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
#x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
  /2 by mem_append_l1/
| #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) //
]
qed.

lemma labels_pc_return: ∀p,prog,x1,x2.
 label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
 ∀m.
   mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
  elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
  normalize nodelta
  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
  | #NEQ #H2 %2 @IH // ] 
| #hd #tl #IH #m @mem_append_l2 @IH ]
qed.

lemma labels_pc_call: ∀p,prog,x1,x2.
 label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
 ∀m.
   mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m).
 #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
  elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
  normalize nodelta
  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
  | #NEQ #H2 %2 @IH // ] 
| #hd #tl #IH #m @mem_append_l2 @IH ]
qed.

unification hint  0 ≔ ; 
    X ≟ DEQInitCostLabel
(* ---------------------------------------- *) ⊢ 
    InitCostLabel ≡ carr X.


unification hint  0 ≔ p1,p2; 
    X ≟ DEQInitCostLabel
(* ---------------------------------------- *) ⊢ 
    eq_init_costlabel p1 p2 ≡ eqb X p1 p2.
    

let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ 
match l with
[ nil ⇒ return y
| cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z
].

definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → 
∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
λp,abs_t,instr_m,mT,prog.
let prog_size ≝ S (|instructions … prog|) in
m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size;  
                               return set_map … m z k) (labels_pc … (instructions … prog) O) 
      (empty_map ?? mT).
      

include "basics/lists/listb.ma".

(*doppione da mettere a posto*)
let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 
match l with
[ nil ⇒ True 
| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
].

definition asm_no_duplicates ≝ 
λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).

(*falso: necessita di no_duplicates*)

definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ 
λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y.

definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet.
mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?.
@hide_prf
* #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta
% [2: #EQ destruct @andb_Prop >(\b (refl …)) %]
inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct
>(\P EQ1) >(\P EQ2) %
qed.
(*
unification hint  0 ≔ D1,D2 ; 
    X ≟ DeqProd D1 D2
(* ---------------------------------------- *) ⊢ 
    D1 × D2 ≡ carr X.


unification hint  0 ≔ D1,D2,p1,p2; 
    X ≟ DeqProd D1 D2
(* ---------------------------------------- *) ⊢ 
    eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2.
    
definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ 
λD1,D2,x.x.

coercion deq_prod_to_prod.
*)

lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) 
∧ b = f a.
#A #B #f #l elim l [ #a *] #x #xs #IH #a *
[ #EQ destruct %{(f x)} % // % // | #H cases(IH … H)
  #b * #H1 #EQ destruct %{(f a)} % // %2 //
]
qed.

lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
asm_no_duplicates p prog → 
static_analisys p abs_t instr_m mT prog = return map → 
mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 
get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)).
#p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???)
#l #endmain #Hendmain elim l [ #x #y #z #w #h * ]
* #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H 
cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H 
cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
destruct *
[ #EQ destruct >get_set_hit >EQelem %
| #H >get_set_miss [ @IH //] inversion (? == ?) [2: #_ %]
  #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
  cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
]
qed.

include "Simulation.ma".

record terminated_trace (S : abstract_status) (R_s2 : S) : Type[0] ≝ 
{  R_post_step : option (ActionLabel × S)
 ; R_fin_ok : match R_post_step with
               [ None ⇒ bool_to_Prop (as_final … R_s2)
               | Some x ⇒ let 〈l,R_post_state〉≝ x in
                          (is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ 
                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
                          as_execute … l R_s2 R_post_state
               ]
 }.

definition big_op: ∀M: monoid. list M → M ≝
 λM. foldl … (op … M) (e … M).

lemma big_op_associative:
 ∀M:monoid. ∀l1,l2.
  big_op M (l1@l2) = op M (big_op … l1) (big_op … l2).
 #M #l1 whd in match big_op; normalize nodelta
 generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1
 [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c)
   generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M) 
   elim l2 normalize
   [ #c #c1 #c2 #EQ @sym_eq //
   | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |]
   ]
 | #x #xs #IH #c #l2 @IH
 ]
qed.

lemma act_big_op : ∀M,B. ∀act : monoid_action M B.
 ∀l1,l2,x.
   act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x).
 #M #B #act #l1 elim l1
 [ #l2 #x >act_neutral //
 | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2)); 
   >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl);
   >big_op_associative >act_op in ⊢ (???%); %
 ]
qed.

lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
block_cost p prog abs_t instr_m pc size = return k → 
∀size'.size ≤ size' → 
block_cost p prog abs_t instr_m pc size' = return k.
#p #prog #abs_t #instr_m #pc #size lapply pc elim size
[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
  #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H %
| #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i
  * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?);
  #EQ destruct #size' *
  [ whd in ⊢ (??%?); @eqb_elim
    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
    #_ normalize nodelta >EQi >m_return_bind >EQelem %
  | #m #Hm whd in ⊢ (??%?); @eqb_elim
    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
    #_ normalize nodelta >EQi >m_return_bind
    cases (emits_labels ??) in EQelem; normalize nodelta
    [ whd in ⊢ (??%%→ ??%%); #EQ destruct %]
    #f #EQelem >(IH … EQelem) [2: /2/ ] %
  ]
]
qed.

lemma step_emit : ∀p,p',prog,st1,st2,l,i.
fetch p prog (pc … st1) = return i →
eval_vmstate p p' … prog st1 = return 〈l,st2〉 →  
emits_labels … i = None ? → ∃x.
match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
[call_act f c ⇒ [a_call c]
|ret_act x ⇒ 
   match x with [None⇒[]|Some c⇒[a_return_post c]]
|cost_act x ⇒
   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
|init_act⇒[ ]
] = [x] ∧ 
 (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)).
#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
[ #seq * [|#lab]
| #newpc
| #cond #newpc #ltrue #lfalse
| #lin #io #lout
| #f
|
]
#EQi cases(asm_is_io ???) normalize nodelta
[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
  ]
]
whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:]
[1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ]
/2 by labels_pc_return, labels_pc_call/
qed.

lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f.
fetch p prog (pc … st1) = return i →
eval_vmstate p p' … prog st1 = return 〈l,st2〉 →  
emits_labels … i = Some ? f → 
match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
[call_act f c ⇒ [a_call c]
|ret_act x ⇒ 
   match x with [None⇒[]|Some c⇒[a_return_post c]]
|cost_act x ⇒
   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
|init_act⇒[ ]
] = [ ] ∧ pc … st2 = f (pc … st1).
#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
[ #seq * [|#lab]
| #newpc
| #cond #newpc #ltrue #lfalse
| #lin #io #lout
| #f
|
]
#EQi cases(asm_is_io ???) normalize nodelta
[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
  ]
]
whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
normalize nodelta #EQ destruct /2 by refl, conj/
qed.


lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog →
∀abs_t : abstract_transition_sys (m … p').∀instr_m.
∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
static_analisys p ? instr_m mT prog = return map1 →
∀st1,st2 : vm_state p p'.
∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
∀k.
pre_measurable_trace … t → 
block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k → 
∀a1.rel_galois … good st1 a1 → 
let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
∀costs.
costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace …  t) →
rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
[2: @hide_prf cases daemon]
#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
lapply ter -ter elim t
[ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ] 
  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 
  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
    #H cases(bind_inversion ????? H) -H *
    [ #seq * [|#lbl1]
    | #newpc
    | #cond #newpc #ltrue #lfalse
    | #lin #io #lout
    | #f
    |
    ] 
    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
    normalize nodelta >EQfetch >m_return_bind normalize nodelta
    cases(asm_is_io ??) normalize nodelta 
    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
      [3: cases x normalize nodelta
      |6: #H cases(bind_inversion ????? H) -H #y * #_
      ]
    ]
    whd in ⊢ (??%% → ?); #EQ destruct 
    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r
    >act_neutral
    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
  ]
| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
  whd #costs whd in match list_cost_to_list_initcost; normalize nodelta 
  <map_append <map_append 
  change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);  
  #EQ destruct whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
  cases(bind_inversion ????? H) -H #i * #EQi
  inversion(emits_labels ??)
  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
  | #f #EQemits normalize nodelta #H
    cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
    #EQ destruct(EQ) >act_op whd in match (append ???); @IH
  ]
  [1,5: inversion H in ⊢ ?; 
    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
      #EQ1 #EQ2 #EQ3 #EQ4 destruct
    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
      #EQ1 #EQ2 #EQ3 #EQ4 destruct
    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    ] //
  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >EQx
    whd in match (map ????); whd in match (map ????); whd in match (big_op ??);
    >neutral_l @opt_safe_elim #elem #EQget <(static_analisys_ok  … x … (pc … st2) … EQmap)
    assumption
  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
  | %
  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    >(monotonicity_of_block_cost … EQk') //
  | @(instr_map_ok … good … EQi … good_a1) /2/
  | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) %
  ]
]
qed.