Module FlatAsmProgram

Require Import String Coqlib Maps.
Require Import AST Integers Floats Values Memory Events Smallstep.
Require Import Locations Stacklayout Conventions EraseArgs.
Require Import Segment FlatAsmGlobenv FlatAsmBuiltin.
Require Import Asm RawAsm.
Require Import Num.
Require Globalenvs.

Ltac destr_if :=
  match goal with
  | [ |- context [if ?b then _ else _] ] =>
    let eq := fresh "EQ" in
    (destruct b eqn:eq)
  end.

Ltac destr_match :=
  match goal with
  | [ |- context [match ?b with _ => _ end] ] =>
    let eq := fresh "EQ" in
    (destruct b eqn:eq)
  end.

Ltac destr_match_in H :=
  match type of H with
  | context [match ?b with _ => _ end] =>
    let eq := fresh "EQ" in
    (destruct b eqn:eq)
  end.


Definition undef_segid: segid_type := 1%positive.
Definition data_segid: segid_type := 3%positive.
Definition code_segid: segid_type := 4%positive.

Definition num_segments: nat := 3.


Section FLATPROG.

Context {I: Type}.

Definition instr_with_info:Type := I * segblock * ident.

Definition code := list instr_with_info.
Record function : Type := mkfunction { fn_sig: signature; fn_code: code; fn_range:segblock; fn_stacksize: Z; fn_pubrange: Z * Z}.
Definition fundef := AST.fundef function.
Definition gdef := globdef fundef unit.

Definition GID_MAP_TYPE := ident -> option seglabel.
Definition LABEL_MAP_TYPE := ident -> ident -> option seglabel.

Record program : Type := {
  prog_defs: list (ident * option gdef * segblock);
  prog_public: list ident;
  prog_main: ident;
  data_seg: segment;
  code_seg: segment;
  glob_map: GID_MAP_TYPE;
  lbl_map: LABEL_MAP_TYPE;
  prog_senv : Globalenvs.Senv.t;
}.

Definition genv := Genv.t fundef unit instr_with_info.

Definition add_global (ge:genv) (idg: ident * option gdef * segblock) : genv :=
  let '(gid,gdef,blk) := idg in
  let gsymbs :=
      match gdef with
      | None
      | Some (Gfun (External _)) =>
        fun id => if ident_eq id gid then Some (Genv.genv_next ge, Ptrofs.zero) else (Genv.genv_symb ge) id
      | _ => Genv.genv_symb ge
      end
  in
  let gdefs :=
      match gdef with
      | None
      | Some (Gfun (External _)) =>
        (fun (b:block) (ofs:ptrofs) =>
          if (eq_block b (Genv.genv_next ge)) && (Ptrofs.eq ofs Ptrofs.zero)
          then gdef else Genv.genv_defs ge b ofs)
      | _ => Genv.genv_defs ge
      end
  in
  Genv.mkgenv
    (Genv.genv_public ge)
    gsymbs
    gdefs
    (Genv.genv_instrs ge)
    (Genv.genv_internal_codeblock ge)
    (Genv.genv_lbl ge)
    (Pos.succ (Genv.genv_next ge))
    (Genv.genv_senv ge).
  
                     
Fixpoint add_globals (ge:genv) (gl: list (ident * option gdef * segblock)) : genv :=
  match gl with
  | nil => ge
  | (idg::gl') =>
    let ge' := add_global ge idg in
    add_globals ge' gl'
  end.

Lemma add_global_pres_genv_instrs: forall def ge ge',
  ge' = add_global ge def ->
  forall b ofs, Genv.genv_instrs ge b ofs = Genv.genv_instrs ge' b ofs.

Lemma add_globals_pres_genv_instrs: forall defs ge ge',
  ge' = add_globals ge defs ->
  forall b ofs, Genv.genv_instrs ge b ofs = Genv.genv_instrs ge' b ofs.



Definition get_instr_ptr (smap:segid_type ->block) (i:instr_with_info): val :=
  let '(_,bi,_) := i in Genv.label_to_ptr smap (segblock_to_label bi).

Definition acc_instr_map (smap:segid_type -> block) (i:instr_with_info) map :
  block -> ptrofs -> option instr_with_info :=
  let ptr := get_instr_ptr smap i in
  fun b ofs => if Val.eq (Vptr b ofs) ptr then Some i else (map b ofs).

Fixpoint acc_instrs_map (smap:segid_type -> block) (c:code) map
  : block -> ptrofs -> option instr_with_info :=
  match c with
  | nil => map
  | i'::c' =>
    let map' := acc_instrs_map smap c' map in
    acc_instr_map smap i' map'
  end.

Definition code_labels (c:code) : list seglabel :=
  List.map (fun '(_,blk,_) => segblock_to_label blk) c.

Lemma incode_labels : forall i (c:code),
  In i c -> In (segblock_to_label (snd (fst i))) (code_labels c).

Definition code_labels_are_distinct (c: code) : Prop :=
  let labels := (map (fun '(_,blk,_) => segblock_to_label blk) c) in
  list_norepet labels.

Fixpoint pos_advance_N (p:positive) (n:nat) : positive :=
  match n with
  | O => p
  | Datatypes.S n' => pos_advance_N (Psucc p) n'
  end.

Lemma psucc_advance_Nsucc_eq : forall n p,
  pos_advance_N (Pos.succ p) n = Pos.succ (pos_advance_N p n).

Lemma pos_advance_N_ple : forall p n,
  Ple p (pos_advance_N p n).


Section WITHSEGSLENGTH.

Variable init_block : block.
Variable segs_length : nat.


Definition segblock_is_valid (b:block) : Prop :=
  Ple init_block b /\ Plt b (pos_advance_N init_block segs_length).

Lemma init_segblock_is_valid :
  (segs_length <> 0)%nat -> segblock_is_valid init_block.

Definition injective_on_valid_segs (sbmap: segid_type -> block) : Prop :=
  forall s1 s2, sbmap s1 = sbmap s2 -> segblock_is_valid (sbmap s1) -> s1 = s2.

Definition code_labels_are_valid (sbmap: segid_type -> block) (c:code) : Prop :=
  forall i sblk fid, In (i,sblk,fid) c -> segblock_is_valid (sbmap (segblock_id sblk)).

Lemma code_labels_are_valid_cons_inv : forall sbmap a l,
    code_labels_are_valid sbmap (a :: l) ->
    segblock_is_valid (sbmap (segblock_id (snd (fst a))))
    /\ code_labels_are_valid sbmap l.

Lemma code_labels_are_valid_cons : forall sbmap a l,
    segblock_is_valid (sbmap (segblock_id (snd (fst a)))) ->
    code_labels_are_valid sbmap l ->
    code_labels_are_valid sbmap (a :: l).
  
Lemma code_labels_are_valid_app : forall sbmap l1 l2,
    code_labels_are_valid sbmap l1 ->
    code_labels_are_valid sbmap l2 ->
    code_labels_are_valid sbmap (l1 ++ l2).

Lemma code_labels_are_valid_eq_map : forall sbmap sbmap' l,
    (forall id, sbmap id = sbmap' id) ->
    code_labels_are_valid sbmap l ->
    code_labels_are_valid sbmap' l.

End WITHSEGSLENGTH.

   
Lemma acc_instrs_map_self : forall init_block slen i c map map' sbmap,
  injective_on_valid_segs init_block slen sbmap ->
  In i c ->
  code_labels_are_distinct c ->
  code_labels_are_valid init_block slen sbmap c ->
  map' = acc_instrs_map sbmap c map ->
  map' (sbmap (segblock_id (snd (fst i)))) (segblock_start (snd (fst i))) = Some i.

Definition get_def_code (def: (ident * option gdef * segblock)) : code :=
  let '(_,def,_) := def in
  match def with
  | Some (Gfun (Internal f)) => fn_code f
  | _ => nil
  end.

Fixpoint get_defs_code (defs: list (ident * option gdef * segblock)) : code :=
  match defs with
  | nil => nil
  | def :: defs' =>
    (get_def_code def) ++ (get_defs_code defs')
  end.

Definition get_program_code (p:program) : code :=
  get_defs_code (prog_defs p).

Definition gen_instrs_map (smap:segid_type -> block) (p:program)
  : block -> ptrofs -> option instr_with_info :=
  acc_instrs_map smap (get_program_code p) (fun b ofs => None).
  
Definition gen_internal_codeblock (smap:segid_type -> block) (p:program) : block -> bool:=
  let code_seg_id := segid p.(code_seg) in
  fun b => eq_block b (smap code_seg_id).

Fixpoint acc_segblocks (nextblock: block) (ids: list segid_type) (map: segid_type -> block)
  : (segid_type -> block) :=
  match ids with
  | nil => map
  | id::ids' =>
    let map' := acc_segblocks (Psucc nextblock) ids' map in
    (fun x => if ident_eq x id then nextblock else map' x)
  end.

Definition list_of_segments (p:program) : list segment :=
  (p.(data_seg) :: (p.(code_seg)) :: nil).

Definition undef_seg_block := 1%positive.
Definition data_block := 2%positive.
Definition code_block := 3%positive.
Definition init_block := data_block.

Definition gen_segblocks (p:program) : (segid_type -> block) :=
  let initmap := fun id => undef_seg_block in
  let ids := List.map segid (list_of_segments p) in
  acc_segblocks init_block ids initmap.

Lemma acc_segblocks_upper_bound : forall l i f,
  (forall id, Plt (f id) i) ->
  (forall id, Plt (acc_segblocks i l f id) (pos_advance_N i (length l))).

Lemma gen_segblocks_upper_bound : forall p id,
  Plt (gen_segblocks p id) (pos_advance_N init_block (length (list_of_segments p))).

Lemma acc_segblocks_in_valid: forall ids id sbmap initb initmap,
  In id ids ->
  sbmap = acc_segblocks initb ids initmap ->
  segblock_is_valid initb (length ids) (sbmap id).
    
Lemma gen_segblocks_in_valid : forall p id sbmap,
  In id (map segid (list_of_segments p)) ->
  sbmap = gen_segblocks p ->
  segblock_is_valid init_block (length (list_of_segments p)) (sbmap id).

Lemma acc_segblocks_range: forall ids b initb initmap s,
  b = (acc_segblocks initb ids initmap s) ->
  b = (initmap s) \/ segblock_is_valid initb (length ids) b.

Lemma acc_segblocks_absurd : forall ids b initb initmap s,
  (forall s, Plt (initmap s) b) -> Plt b initb ->
  b = (acc_segblocks initb ids initmap s) -> False.

Lemma acc_segblocks_injective : forall ids init_block0 initmap sbmap,
    (forall s, Plt (initmap s) init_block0) ->
    sbmap = acc_segblocks init_block0 ids initmap ->
    injective_on_valid_segs init_block0 (length ids) sbmap.

Lemma gen_segblocks_injective : forall p,
    injective_on_valid_segs init_block (length (list_of_segments p)) (gen_segblocks p).


Definition empty_genv (p:program): genv :=
  Genv.mkgenv (prog_public p) (fun id => None) (fun b ofs => None) (fun b ofs => None) (fun b => false)
              (fun fid lbl => None) 1%positive (prog_senv p).

Definition gidmap_to_symbmap (smap: segid_type -> block) (gmap:GID_MAP_TYPE) :=
  fun id =>
    match gmap id with
    | None => None
    | Some (sid,ofs) => Some (smap sid, ofs)
    end.

Definition lblmap_to_symbmap (smap: segid_type -> block) (lmap:LABEL_MAP_TYPE) :=
  fun fid lbl =>
    match lmap fid lbl with
    | None => None
    | Some (sid,ofs) => Some (smap sid, ofs)
    end.

Definition globalenv (p: program) : genv :=
  let smap := gen_segblocks p in
  let symbmap := gidmap_to_symbmap smap (glob_map p) in
  let lblmap := lblmap_to_symbmap smap (lbl_map p) in
  let imap := gen_instrs_map smap p in
  let nextblock := Pos.of_succ_nat num_segments in
  let cbmap := gen_internal_codeblock smap p in
  let genv := Genv.mkgenv (prog_public p) symbmap (fun b ofs => None) imap cbmap lblmap nextblock (prog_senv p) in
  add_globals genv p.(prog_defs).
  


Section WITHEXTERNALCALLS.
Context `{external_calls_prf: ExternalCalls}.

Section WITHGE.

Variable ge:genv.

Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
  match id with
  | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
  | Init_int16 n => Mem.store Mint16unsigned m b p (Vint n)
  | Init_int32 n => Mem.store Mint32 m b p (Vint n)
  | Init_int64 n => Mem.store Mint64 m b p (Vlong n)
  | Init_float32 n => Mem.store Mfloat32 m b p (Vsingle n)
  | Init_float64 n => Mem.store Mfloat64 m b p (Vfloat n)
  | Init_addrof gloc ofs => Mem.store Mptr m b p (Genv.symbol_address ge gloc ofs)
  | Init_space n => Some m
  end.

Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
                              {struct idl}: option mem :=
  match idl with
  | nil => Some m
  | id :: idl' =>
      match store_init_data m b p id with
      | None => None
      | Some m' => store_init_data_list m' b (p + init_data_size id) idl'
      end
  end.

Definition alloc_global (m: mem) (idg: ident * option gdef * segblock): option mem :=
  let '(id, gdef, sb) := idg in
  match gdef with
  | None =>
    let (m1, b) := Mem.alloc m 0 0 in
    Some m1
  | Some (Gfun f) =>
    let (m1, b) := Mem.alloc m 0 1 in
    Some m1
  | Some (Gvar v) =>
    let (m1, b) := Mem.alloc m 0 0 in
    Some m1
  end.

Fixpoint alloc_globals (m: mem) (gl: list (ident * option gdef * segblock))
                       {struct gl} : option mem :=
  match gl with
  | nil => Some m
  | g :: gl' =>
      match alloc_global m g with
      | None => None
      | Some m' => alloc_globals m' gl'
      end
  end.

Definition store_global n (smap:segid_type -> block) (m: mem) (idg: ident * option gdef * segblock): option mem :=
  let '(id, gdef, sb) := idg in
  let ofs := Ptrofs.unsigned (segblock_start sb) in
  let sz := Ptrofs.unsigned (segblock_size sb) in
  let b := smap (segblock_id sb) in
  match gdef with
  | None => Some m
  | Some (Gfun f) =>
    match f with
    | External _ =>
      Mem.drop_perm m (pos_advance_N (Pos.of_succ_nat num_segments) n) 0 1 Nonempty
    | Internal f =>
      Mem.drop_perm m b ofs (ofs + sz) Nonempty
    end
  | Some (Gvar v) =>
    let init := gvar_init v in
    let isz := init_data_list_size init in
    match Globalenvs.store_zeros m b ofs isz with
    | None => None
    | Some m1 =>
      match store_init_data_list m1 b ofs init with
      | None => None
      | Some m2 => Mem.drop_perm m2 b ofs (ofs+isz) (Globalenvs.Genv.perm_globvar v)
      end
    end
  end.

Fixpoint store_globals_iter n (smap:segid_type->block) (m: mem) (gl: list (ident * option gdef * segblock))
                       : option mem :=
  match gl with
  | nil => Some m
  | g :: gl' =>
      match store_global n smap m g with
      | None => None
      | Some m' => store_globals_iter (Datatypes.S n) smap m' gl'
      end
  end.

Definition store_globals (smap:segid_type->block) (m: mem) (gl: list (ident * option gdef * segblock))
                       : option mem :=
  store_globals_iter 0 smap m gl.

End WITHGE.

Fixpoint alloc_segments m (segs: list segment) :=
  match segs with
  | nil => m
  | s :: segs' =>
    match Mem.alloc m 0 (Ptrofs.unsigned (segsize s)) with
    | (m',_) => alloc_segments m' segs'
    end
  end.

Definition alloc_segment m seg := Mem.alloc m 0 (Ptrofs.unsigned (segsize seg)).

Definition init_mem (p: program) :=
  let ge := globalenv p in
  let (initm,_) := Mem.alloc Mem.empty 0 0 in
  let m := alloc_segments initm (list_of_segments p) in
  match alloc_globals m (prog_defs p) with
  | None => None
  | Some m3 =>
    store_globals ge (gen_segblocks p) m3 (prog_defs p)
  end.


Lemma store_init_data_perm : forall (ge:genv) m m' b b' p i q k prm,
  store_init_data ge m b p i = Some m' -> Mem.perm m' b' q k prm <-> Mem.perm m b' q k prm.

Lemma store_init_data_list_perm : forall idl (ge:genv) m m' b p b' q k prm,
  store_init_data_list ge m b p idl = Some m' -> Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm.

Lemma store_init_data_stack : forall v (ge:genv) (m m' : mem) (b : block) (ofs : Z),
       store_init_data ge m b ofs v = Some m' -> Mem.stack m' = Mem.stack m.

Lemma store_init_data_list_stack : forall l (ge:genv) (m m' : mem) (b : block) (ofs : Z),
       store_init_data_list ge m b ofs l = Some m' -> Mem.stack m' = Mem.stack m.

Existing Instance inject_perm_all.

Lemma store_global_stack : forall (ge:genv) n smap m def m',
    store_global ge n smap m def = Some m' ->
    Mem.stack m' = Mem.stack m.

Lemma store_globals_iter_stack : forall l (ge:genv) n smap m m',
    store_globals_iter ge n smap m l = Some m' ->
    Mem.stack m' = Mem.stack m.

Lemma store_globals_stack : forall l (ge:genv) smap m m',
    store_globals ge smap m l = Some m' ->
    Mem.stack m' = Mem.stack m.

Lemma alloc_segments_perm_ofs : forall segs m1 m2
                                  (ALLOCSEGS : alloc_segments m1 segs = m2)
                                  (PERMOFS : forall b ofs k p, Mem.perm m1 b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned),
    (forall b ofs k p, Mem.perm m2 b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned).

Lemma one_le_ptrofs_max_unsigned : 1 <= Ptrofs.max_unsigned.

Lemma alloc_globals_perm_ofs : forall defs m1 m2
                                  (ALLOC : alloc_globals m1 defs = Some m2)
                                  (PERMOFS : forall b ofs k p, Mem.perm m1 b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned),
    (forall b ofs k p, Mem.perm m2 b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned).


Lemma alloc_segments_stack: forall l m m',
    m' = alloc_segments m l -> Mem.stack m' = Mem.stack m.

Lemma alloc_segments_nextblock : forall l m m',
  m' = alloc_segments m l -> Mem.nextblock m' = pos_advance_N (Mem.nextblock m) (length l).

Lemma alloc_segment_stack: forall s m m' b,
    alloc_segment m s = (m',b) -> Mem.stack m' = Mem.stack m.

Definition DEF : Type := ident * option gdef * segblock.


Lemma alloc_global_stack: forall (def: DEF) m m',
    alloc_global m def = Some m' -> Mem.stack m = Mem.stack m'.
    
Lemma alloc_globals_stack: forall (defs: list DEF) m m',
    alloc_globals m defs = Some m' -> Mem.stack m = Mem.stack m'.
    

Lemma init_mem_stack:
  forall p m,
    init_mem p = Some m ->
    Mem.stack m = nil.

Lemma store_init_data_nextblock : forall v (ge:genv) m b ofs m',
  store_init_data ge m b ofs v = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.
    
Lemma store_init_data_list_nextblock : forall l (ge:genv) m b ofs m',
  store_init_data_list ge m b ofs l = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.

Remark store_global_nextblock:
  forall v (ge: genv) n smap m m',
  store_global ge n smap m v = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.

Remark store_globals_iter_nextblock:
  forall gl (ge: genv) n smap m m',
  store_globals_iter ge n smap m gl = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.

Remark store_globals_nextblock:
  forall gl (ge: genv) smap m m',
  store_globals ge smap m gl = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.

Lemma alloc_global_nextblock : forall (def:DEF) m m',
  alloc_global m def = Some m' ->
  Mem.nextblock m' = Pos.succ (Mem.nextblock m).

Lemma alloc_globals_nextblock : forall (defs: list DEF) m m',
  alloc_globals m defs = Some m' ->
  Mem.nextblock m' = pos_advance_N (Mem.nextblock m) (List.length defs).
    
Lemma alloc_segment_nextblock : forall m s m' b,
    alloc_segment m s = (m', b) -> Mem.nextblock m' = Pos.succ (Mem.nextblock m).



Lemma add_global_next_block: forall (ge:genv) def,
    Genv.genv_next (add_global ge def) = Pos.succ (Genv.genv_next ge).

Lemma add_globals_next_block: forall (defs: list DEF) ge,
  Genv.genv_next (add_globals ge defs) = pos_advance_N (Genv.genv_next ge) (List.length defs).

Lemma alloc_segments_nextblock' : forall (l : list segment) (m: mem),
  Mem.nextblock (alloc_segments m l) = pos_advance_N (Mem.nextblock m) (length l).

Lemma alloc_global_pres_perm :
  forall def m b ofs k p m'
  (PERM: Mem.perm m b ofs k p)
  (ALLOC: alloc_global m def = Some m'),
    Mem.perm m' b ofs k p.

Lemma alloc_globals_pres_perm :
  forall defs m b ofs k p m'
  (PERM: Mem.perm m b ofs k p)
  (ALLOC: alloc_globals m defs = Some m'),
    Mem.perm m' b ofs k p.

Lemma init_mem_genv_next: forall (p: program) m,
  init_mem p = Some m ->
  Genv.genv_next (globalenv p) = Mem.nextblock m.

Lemma add_global_pres_instrs : forall ge def,
    Genv.genv_instrs (add_global ge def) = Genv.genv_instrs ge.

Lemma add_globals_pres_instrs : forall defs ge,
    Genv.genv_instrs (add_globals ge defs) = Genv.genv_instrs ge.

Definition def_is_var_or_internal_fun (def: (ident * option gdef * segblock)) :=
  let '(_,d,_) := def in
  (exists v, d = Some (Gvar v)) \/ (exists f, d = (Some (Gfun (Internal f)))).

Definition defs_is_var_or_internal_fun (i:ident) (defs: list (ident * option gdef * segblock)) :=
  forall def sb, In (i, def, sb) defs -> def_is_var_or_internal_fun (i, def, sb).
                                                    
Lemma add_global_pres_find_symbol : forall def ge i,
  def_is_var_or_internal_fun def ->
  Genv.find_symbol (add_global ge def) i = Genv.find_symbol ge i.

Lemma add_globals_pres_find_symbol : forall defs ge i,
  defs_is_var_or_internal_fun i defs ->
  Genv.find_symbol (add_globals ge defs) i = Genv.find_symbol ge i.

Lemma add_global_pres_internal_block : forall def ge b,
  Genv.genv_internal_codeblock (add_global ge def) b = Genv.genv_internal_codeblock ge b.

Lemma add_globals_pres_internal_block : forall defs ge ge' b,
  add_globals ge defs = ge' ->
  Genv.genv_internal_codeblock ge' b = Genv.genv_internal_codeblock ge b.

Lemma add_global_pres_find_symbol_neq : forall ge i o s i1,
  i <> i1 ->
  Genv.find_symbol (add_global ge (i, o, s)) i1 = Genv.find_symbol ge i1.

Lemma add_globals_pres_find_symbol_not_in :
  forall defs i ge
    (NIN: ~In i (map (fun '(i,_,_) => i) defs)),
    Genv.find_symbol (add_globals ge defs) i = Genv.find_symbol ge i.

Definition def_is_none_or_external_fun (def: (ident * option gdef * segblock)) :=
  let '(_,d,_) := def in
  d = None \/ (exists f, d = (Some (Gfun (External f)))).


Lemma add_global_find_symbol_eq:
  forall (ge : genv) (i : ident) (o : option gdef) (s : segblock) (i1 : ident)
  (NE: def_is_none_or_external_fun (i, o, s)),
  Genv.find_symbol (add_global ge (i, o, s)) i = Some (Genv.genv_next ge, Ptrofs.zero).

Inductive Nth {A :Type} : nat -> list A -> A -> Prop :=
| Nth_base: forall x l, Nth O (x::l) x
| Nth_cons: forall n x y l, Nth n l x -> Nth (Coq.Init.Datatypes.S n) (y::l) x.

Lemma add_globals_find_symbol_ne : forall defs x def sb n ge
    (NE: def_is_none_or_external_fun (x, def, sb))
    (NTH: Nth n defs (x,def,sb))
    (NPT: list_norepet (map (fun '(i,_,_) => i) defs)),
    Genv.find_symbol (add_globals ge defs) x = Some (pos_advance_N (Genv.genv_next ge) n, Ptrofs.zero).
      

Lemma In_Nth: forall (A : Type) (l : list A) (x : A),
    In x l -> exists n : nat, (n < length l)%nat /\ Nth n l x.

Lemma add_global_pres_lbl:
  forall (def : ident * option gdef * segblock) (ge : genv) (b : block),
    Genv.genv_lbl (add_global ge def) b = Genv.genv_lbl ge b.
    
Lemma add_globals_pres_lbl:
  forall (defs : list (ident * option gdef * segblock)) (ge : genv) (b : block),
    Genv.genv_lbl (add_globals ge defs) b = Genv.genv_lbl ge b.

Lemma genv_internal_codeblock_add_global:
  forall g def,
    Genv.genv_internal_codeblock (add_global g def) = Genv.genv_internal_codeblock g.

Lemma genv_internal_codeblock_add_globals:
  forall l g,
    Genv.genv_internal_codeblock (add_globals g l) = Genv.genv_internal_codeblock g.

Lemma add_global_pres_find_def_blt : forall b ge def ofs,
  Pos.lt b (Genv.genv_next ge) ->
  Genv.find_def (add_global ge def) b ofs = Genv.find_def ge b ofs.

Lemma add_globals_pres_find_def: forall defs ge b ofs,
    Pos.lt b (Genv.genv_next ge) ->
    Genv.find_def (add_globals ge defs) b ofs = Genv.find_def ge b ofs.

Lemma unique_def_is_internal_fun : forall defs i f sb
  (NPT: list_norepet (map (fun '(i,_,_) => i) defs))
  (IN: In (i, Some (Gfun (Internal f)), sb) defs),
  defs_is_var_or_internal_fun i defs.

Lemma unique_def_is_var : forall defs i v sb
  (NPT: list_norepet (map (fun '(i,_,_) => i) defs))
  (IN: In (i, Some (Gvar v), sb) defs),
  defs_is_var_or_internal_fun i defs.


End WITHEXTERNALCALLS.

End FLATPROG.