include "Common.ma".

inductive classification: Type[0] ≝
   sequential: classification
 | conditional: nat → classification
 | call: ident → classification
 | ret: classification.

record object_code_def: Type[1] ≝
 { status: Type[0]
 ; trans: status → status
 ; max: nat
 ; pc: status → nat
 ; succ: nat → nat
 ; labelled: nat → nat → bool
 ; classify: nat → classification
 ; classification_ok1:
    ∀s. classify (pc s) = sequential → pc (trans s) = succ (pc s)
 ; code_closed:
    ∀pc. pc < max → classify pc = sequential → succ pc < max
   (* serve per jmp e call??? *)
 }.

record abelian_monoid: Type[1] ≝
 { carrier :> Type[0]
 ; op: carrier → carrier → carrier
 ; e: carrier
 ; neutral: ∀x. op … x e = x
 ; associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
 ; commutative: ∀x,y. op … x y = op … y x
 }.

instr_cost: nat → M

k: n:nat → pc:nat → M ≝
 match n with
 [ O ⇒ whatever
 | S n' ⇒
    match classify pc with
    [ seq ⇒
       if labelelled pc (succ pc) then
        instr_cost pc
       else
        instr_cost pc + k n' (succ pc)
    | call ⇒
       if postlabelled pc then
        instr_cost pc
       else
        instr_cost pc + k n' (succ pc)
    | _ ⇒ instr_cost pc
    ]]

theorem strong:
 ∀τ: so -pm→ sn. τ finisce con label o return →
  Σ_(pc → pc' ∈ τ) instr_cost pc =
  k max (pc s0) + Σ_(pc -L→ pc' ∈ τ senza l'ultima) K max pc'.

definition x ≤ y ≝ ∃z. op x z = y.

theorem weak:
 ∀τ: so -pm→ sn. τ estendibile fino a trovare una label o una ret.
  Σ_(pc → pc' ∈ τ) instr_cost pc ≤
  k max (pc s0) + Σ_(pc -L→ pc' ∈ τ senza l'ultima se finisce con label o return labelled) K max pc'.

theorem superweak:
 come strong o weak, ma
   1. tutte le call sono postlabelled
   2. il monoide non e' abeliano

===================================================

record cost_monoid ≝ λ nat → 

let rec cost_from (pc: nat): 

inductive instr: Type[0] :=
| Iconst: nat → instr
| Ivar: option ident → instr
| Isetvar: option ident → instr
| Iadd: instr
| Isub: instr
| Ijmp: nat → instr
| Ibne: nat → instr
| Ibge: nat → instr
| Ihalt: instr
| Iio: instr
| Icall: fname → instr
| Iret: fname → instr.

definition programT ≝ fname → list instr.

definition fetch: list instr → nat → option instr ≝ λl,n. nth_opt ? n l.

definition stackT: Type[0] ≝ list nat.

definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).

definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).

inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
| vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
   vmstep …
    〈c, pc,     stk,      s〉
    〈c, 1 + pc, n :: stk, s〉
| vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
   vmstep …
    〈c, pc,     stk,              s〉
    〈c, 1 + pc, get … s x :: stk, s〉
| vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
   vmstep …
    〈c, pc,     n :: stk, s〉
    〈c, 1 + pc, stk,      set … s x n〉
| vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
   vmstep …
    〈c, pc,     n2 :: n1 :: stk,  s〉
    〈c, 1 + pc, (n1 + n2) :: stk, s〉
| vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
   vmstep …
    〈c, pc,     n2 :: n1 :: stk,  s〉
    〈c, 1 + pc, (n1 - n2) :: stk, s〉
| vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) →
   let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
   vmstep …
    〈c, pc,  n2 :: n1 :: stk, s〉
    〈c, pc', stk,             s〉
| vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) →
   let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
   vmstep …
    〈c, pc,  n2 :: n1 :: stk, s〉
    〈c, pc', stk,             s〉
| vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) →
   let pc' ≝ 1 + pc + ofs in
   vmstep …
    〈c,           pc, stk, s〉
    〈c, 1 + pc + ofs, stk, s〉
| vmstep_io: ∀c,pc,stk,s. fetch c pc = Some … Iio →
   vmstep …
    〈c,     pc, stk, s〉
    〈c, 1 + pc, stk, s〉.

definition emitterT ≝ nat → nat → option label.

definition vmlstep: ∀p: programT. ∀S: storeT. ∀emit: emitterT.
 vmstate S → vmstate S → list label → Prop ≝
λp,S,emitter,s1,s2,ll. ∀l.
 vmstep p S s1 s2 ∧ ll = [l] ∧ emitter (pc … s1) (pc … s2) = Some … l.

(*
Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).

Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
        exists pc,
        code_at c pc = Some (Ihalt lbl) /\
        star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.

Definition term_vm (c: code_vm) (s_init s_fin: store):=
        exists pc,
        code_at c pc = Some (Ihalt False) /\
        star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.

Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
        exists pc,
        code_at c pc = Some (Ihalt label) /\
        star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
*)