Library C_types
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext String_ext Lists_ext Max_ext.
Require Import machine_int nodup.
Import MachineInt.
Local Close Scope Z_scope.
Require Import Arith_ext String_ext Lists_ext Max_ext.
Require Import machine_int nodup.
Import MachineInt.
Local Close Scope Z_scope.
tags for C struct
Inductive stag := mkStag : string -> stag.
Definition eq_stag t1 t2 := match t1, t2 with mkStag s1, mkStag s2 => s1 == s2 end.
Lemma eq_stagP : Equality.axiom eq_stag.
Canonical Structure stag_eqMixin := EqMixin eq_stagP.
Canonical Structure stag_eqType := Eval hnf in EqType _ stag_eqMixin.
basic integral types
rtyp = "recursive type" = pointer to a structure of the corresponding tag
Inductive typ : Type :=
| btyp of ityp
| ptyp of typ
| rtyp of stag
| styp of stag & list (string * typ).
Section correct_typ_ind.
Variables (P : typ -> Prop) (Q : list (string * typ) -> Prop).
Hypotheses (H : forall s l, Q l -> P (styp s l))
(H0 : Q nil)
(H1 : forall i, P (btyp i))
(H2 : forall t, P t -> P (ptyp t))
(H3 : forall tag, P (rtyp tag))
(H4 : forall t, P t -> forall l, Q l -> forall s, Q ((s, t) :: l)).
Fixpoint typ_ind_gen t : P t :=
match t as x return P x with
| btyp i => H1 i
| ptyp t' => H2 t' (typ_ind_gen t')
| rtyp t => H3 t
| styp s l => H s l ((fix t_ind l' : Q l' :=
match l' as x return Q x with
| nil => H0
| cons (s1, t1) tl => H4 t1 (typ_ind_gen t1) tl (t_ind tl) s1
end) l)
end.
End correct_typ_ind.
Lemma typ_ind_new : forall P : typ -> Prop,
(forall i, P (btyp i)) ->
(forall t, P t -> P (ptyp t)) ->
(forall t, P (rtyp t)) ->
(forall s l, (forall x, In x (map (fun x => snd x) l) -> P x) -> P (styp s l)) ->
forall t, P t.
Fixpoint typ_max_depth t : nat :=
match t with
| btyp _ => O
| ptyp t' => S (typ_max_depth t')
| rtyp _ => O
| styp _ l => S (max_list (map (fun x => typ_max_depth (snd x)) l) O)
end.
| btyp of ityp
| ptyp of typ
| rtyp of stag
| styp of stag & list (string * typ).
Section correct_typ_ind.
Variables (P : typ -> Prop) (Q : list (string * typ) -> Prop).
Hypotheses (H : forall s l, Q l -> P (styp s l))
(H0 : Q nil)
(H1 : forall i, P (btyp i))
(H2 : forall t, P t -> P (ptyp t))
(H3 : forall tag, P (rtyp tag))
(H4 : forall t, P t -> forall l, Q l -> forall s, Q ((s, t) :: l)).
Fixpoint typ_ind_gen t : P t :=
match t as x return P x with
| btyp i => H1 i
| ptyp t' => H2 t' (typ_ind_gen t')
| rtyp t => H3 t
| styp s l => H s l ((fix t_ind l' : Q l' :=
match l' as x return Q x with
| nil => H0
| cons (s1, t1) tl => H4 t1 (typ_ind_gen t1) tl (t_ind tl) s1
end) l)
end.
End correct_typ_ind.
Lemma typ_ind_new : forall P : typ -> Prop,
(forall i, P (btyp i)) ->
(forall t, P t -> P (ptyp t)) ->
(forall t, P (rtyp t)) ->
(forall s l, (forall x, In x (map (fun x => snd x) l) -> P x) -> P (styp s l)) ->
forall t, P t.
Fixpoint typ_max_depth t : nat :=
match t with
| btyp _ => O
| ptyp t' => S (typ_max_depth t')
| rtyp _ => O
| styp _ l => S (max_list (map (fun x => typ_max_depth (snd x)) l) O)
end.
collect rtyp tags
Fixpoint rtags' n (t : typ) :=
match n with
| O =>
match t with
| btyp _ => nil
| ptyp _ => nil
| rtyp tg => tg :: nil
| styp _ l => nil
end
| S m =>
match t with
| btyp _ => nil
| ptyp t' => rtags' m t'
| rtyp tg => tg :: nil
| styp _ ss_ts => fold_left (fun a e => rtags' m e ++ a) (uzip2 ss_ts) nil
end
end.
Definition rtags t := rtags' (typ_max_depth t) t.
Lemma rtags'_upper : forall t n, typ_max_depth t <= n ->
rtags' (typ_max_depth t) t = rtags' n t .
Lemma incl_rtags_ptyp_inv : forall t l, incl (rtags (ptyp t)) l -> incl (rtags t) l.
Lemma In_fold_left_rtags2 : forall l tg f, In tg (rtags (snd f)) ->
In tg
(fold_left
(fun acc t =>
rtags'
(max_list
(map (fun f0 : string * _ => typ_max_depth (snd f0)) l)
(typ_max_depth (@snd string _ f)))
t ++
acc)
(uzip2 l)
(rtags (snd f))).
Lemma incl_rtags_styp_hd : forall l f tg, incl (rtags (snd f)) (rtags (styp tg (f :: l))).
Lemma incl_rtags_styp_tl : forall l f tg, incl (rtags (styp tg l)) (rtags (styp tg (f :: l))).
Lemma In_fold_left_rtags : forall l t, In t (uzip2 l) ->
forall a, In a (rtags t) ->
In a
(fold_left
(fun acc t' =>
rtags'
(max_list (map (fun x : string * _ => typ_max_depth (snd x)) l) 0)
t' ++
acc)
(uzip2 l)
nil).
Lemma incl_rtags_styp_inv : forall tg l tgs, incl (rtags (styp tg l)) tgs ->
forall y, In y (uzip2 l) -> incl (rtags y) tgs.
match n with
| O =>
match t with
| btyp _ => nil
| ptyp _ => nil
| rtyp tg => tg :: nil
| styp _ l => nil
end
| S m =>
match t with
| btyp _ => nil
| ptyp t' => rtags' m t'
| rtyp tg => tg :: nil
| styp _ ss_ts => fold_left (fun a e => rtags' m e ++ a) (uzip2 ss_ts) nil
end
end.
Definition rtags t := rtags' (typ_max_depth t) t.
Lemma rtags'_upper : forall t n, typ_max_depth t <= n ->
rtags' (typ_max_depth t) t = rtags' n t .
Lemma incl_rtags_ptyp_inv : forall t l, incl (rtags (ptyp t)) l -> incl (rtags t) l.
Lemma In_fold_left_rtags2 : forall l tg f, In tg (rtags (snd f)) ->
In tg
(fold_left
(fun acc t =>
rtags'
(max_list
(map (fun f0 : string * _ => typ_max_depth (snd f0)) l)
(typ_max_depth (@snd string _ f)))
t ++
acc)
(uzip2 l)
(rtags (snd f))).
Lemma incl_rtags_styp_hd : forall l f tg, incl (rtags (snd f)) (rtags (styp tg (f :: l))).
Lemma incl_rtags_styp_tl : forall l f tg, incl (rtags (styp tg l)) (rtags (styp tg (f :: l))).
Lemma In_fold_left_rtags : forall l t, In t (uzip2 l) ->
forall a, In a (rtags t) ->
In a
(fold_left
(fun acc t' =>
rtags'
(max_list (map (fun x : string * _ => typ_max_depth (snd x)) l) 0)
t' ++
acc)
(uzip2 l)
nil).
Lemma incl_rtags_styp_inv : forall tg l tgs, incl (rtags (styp tg l)) tgs ->
forall y, In y (uzip2 l) -> incl (rtags y) tgs.
collect styp tags
Fixpoint stags' n (t : typ) :=
match n with
| O =>
match t with
| btyp _ => nil
| ptyp _ => nil
| rtyp _ => nil
| styp _ l => nil
end
| S m =>
match t with
| btyp _ => nil
| ptyp t' => stags' m t'
| rtyp _ => nil
| styp tg ss_ts => (tg, ss_ts) ::
fold_left (fun a e => stags' m e ++ a) (uzip2 ss_ts) nil
end
end.
Definition stags t := stags' (typ_max_depth t) t.
Lemma stags'_upper : forall t n, typ_max_depth t <= n ->
stags' (typ_max_depth t) t = stags' n t .
Lemma incl_stags_ptyp_inv : forall t l, incl (stags (ptyp t)) l -> incl (stags t) l.
Lemma In_fold_left_stags : forall l t, In t (uzip2 l) ->
forall a, In a (stags t) ->
In a
(fold_left
(fun acc t' =>
stags'
(max_list (map (fun x : string * _ => typ_max_depth (snd x)) l) 0)
t' ++
acc)
(uzip2 l)
nil).
Lemma incl_stags_styp_inv : forall ta la l, incl (stags (styp ta la)) l ->
forall y, In y (uzip2 la) -> incl (stags y) l.
Lemma incl_stags_styp_inv2 : forall ta la l, incl (stags (styp ta la)) l ->
forall y, In y la -> incl (stags (snd y)) l.
Lemma incl_stags_styp_inv3 : forall ta la l, incl (stags (styp ta la)) l -> In (ta, la) l.
match n with
| O =>
match t with
| btyp _ => nil
| ptyp _ => nil
| rtyp _ => nil
| styp _ l => nil
end
| S m =>
match t with
| btyp _ => nil
| ptyp t' => stags' m t'
| rtyp _ => nil
| styp tg ss_ts => (tg, ss_ts) ::
fold_left (fun a e => stags' m e ++ a) (uzip2 ss_ts) nil
end
end.
Definition stags t := stags' (typ_max_depth t) t.
Lemma stags'_upper : forall t n, typ_max_depth t <= n ->
stags' (typ_max_depth t) t = stags' n t .
Lemma incl_stags_ptyp_inv : forall t l, incl (stags (ptyp t)) l -> incl (stags t) l.
Lemma In_fold_left_stags : forall l t, In t (uzip2 l) ->
forall a, In a (stags t) ->
In a
(fold_left
(fun acc t' =>
stags'
(max_list (map (fun x : string * _ => typ_max_depth (snd x)) l) 0)
t' ++
acc)
(uzip2 l)
nil).
Lemma incl_stags_styp_inv : forall ta la l, incl (stags (styp ta la)) l ->
forall y, In y (uzip2 la) -> incl (stags y) l.
Lemma incl_stags_styp_inv2 : forall ta la l, incl (stags (styp ta la)) l ->
forall y, In y la -> incl (stags (snd y)) l.
Lemma incl_stags_styp_inv3 : forall ta la l, incl (stags (styp ta la)) l -> In (ta, la) l.
a predicate to rule out:
- empty structures
- structures with duplicate fields
Fixpoint wft (t : typ) : bool :=
match t with
| btyp _ => true
| ptyp t' => wft t'
| rtyp _ => true
| styp _ nil => false
| styp _ l => fold_andb (map (fun x => wft (snd x)) l) && nodup (uzip1 l)
end.
Lemma wf_uchar : wft (btyp uchar).
Lemma wf_uint32 : wft (btyp uint32).
Lemma wft_styp_inv1 : forall s h t, wft (styp s (h :: t)) -> wft (snd h).
Lemma wft_styp_inv2 : forall s h t, t <> nil -> wft (styp s (h :: t)) -> wft (styp s t).
Lemma wft_styp_inv : forall tag l, wft (styp tag l) ->
forall x, In x l -> wft (snd x).
Lemma wft_styp_inv' : forall tag l, wft (styp tag l) ->
forall x, In x (uzip2 l) -> wft x.
Lemma wft_ptyp_inv : forall t, wft (ptyp t) -> wft t.
match t with
| btyp _ => true
| ptyp t' => wft t'
| rtyp _ => true
| styp _ nil => false
| styp _ l => fold_andb (map (fun x => wft (snd x)) l) && nodup (uzip1 l)
end.
Lemma wf_uchar : wft (btyp uchar).
Lemma wf_uint32 : wft (btyp uint32).
Lemma wft_styp_inv1 : forall s h t, wft (styp s (h :: t)) -> wft (snd h).
Lemma wft_styp_inv2 : forall s h t, t <> nil -> wft (styp s (h :: t)) -> wft (styp s t).
Lemma wft_styp_inv : forall tag l, wft (styp tag l) ->
forall x, In x l -> wft (snd x).
Lemma wft_styp_inv' : forall tag l, wft (styp tag l) ->
forall x, In x (uzip2 l) -> wft x.
Lemma wft_ptyp_inv : forall t, wft (ptyp t) -> wft t.
Pointer model
Parameter ptr_len : nat.
Parameter ptr_size : nat.
Parameter Hptr_size : ptr_len = ptr_size * 8.
Parameter ptr_size_neq0 : ptr_size <> O.
Parameter align_ptr : nat.
Parameter size_align_ptr : ptr_len = align_ptr.
Parameter ptr_len_32 : 32 <= ptr_len.
Lemma ptr_size_4 : (4 <= ptr_size)%nat.
Definition ptr_len' := ptr_len - 1.
Lemma Hptr_len' : ptr_len = S ptr_len'.
Definition intP (a b : int ptr_len) : bool :=
match dec_int a b with
| left _ => true
| right _ => false
end.
Lemma eqintP : Equality.axiom intP.
Canonical Structure int_eqMixin := EqMixin eqintP.
Canonical Structure int_eqType := Eval hnf in EqType _ int_eqMixin.
Require order.
Parameter ptr_size : nat.
Parameter Hptr_size : ptr_len = ptr_size * 8.
Parameter ptr_size_neq0 : ptr_size <> O.
Parameter align_ptr : nat.
Parameter size_align_ptr : ptr_len = align_ptr.
Parameter ptr_len_32 : 32 <= ptr_len.
Lemma ptr_size_4 : (4 <= ptr_size)%nat.
Definition ptr_len' := ptr_len - 1.
Lemma Hptr_len' : ptr_len = S ptr_len'.
Definition intP (a b : int ptr_len) : bool :=
match dec_int a b with
| left _ => true
| right _ => false
end.
Lemma eqintP : Equality.axiom intP.
Canonical Structure int_eqMixin := EqMixin eqintP.
Canonical Structure int_eqType := Eval hnf in EqType _ int_eqMixin.
Require order.
a relation between type that does not behave yet as an equality
(refl and sym only) (eqtm will behave as an equality )
Fixpoint eqt' n t1 t2 : bool :=
match n with
| O => match t1, t2 with
| btyp uint32, btyp uint32 => true
| btyp sint32, btyp sint32 => true
| btyp uchar , btyp uchar => true
| rtyp tg1 , rtyp tg2 => tg1 == tg2
| btyp uint32, btyp uchar => false
| btyp sint32, btyp uchar => false
| btyp uchar , btyp uint32 => false
| btyp uchar , btyp sint32 => false
| btyp uint32, btyp sint32 => false
| btyp sint32, btyp uint32 => false
| _ , ptyp _ => false
| ptyp _ , _ => false
| btyp _ , rtyp _ => false
| rtyp _ , btyp _ => false
| styp _ _ , _ => false
| _ , styp _ _ => false
end
| S m => match t1, t2 with
| btyp uint32, btyp uint32 => true
| btyp sint32, btyp sint32 => true
| btyp uchar , btyp uchar => true
| rtyp tg1 , rtyp tg2 => tg1 == tg2
| btyp uint32, btyp uchar => false
| btyp sint32, btyp uchar => false
| btyp uchar , btyp uint32 => false
| btyp uchar , btyp sint32 => false
| btyp uint32, btyp sint32 => false
| btyp sint32, btyp uint32 => false
| ptyp t1' , ptyp t2' => eqt' m t1' t2'
| styp tg1 l1 , styp tg2 l2 => (tg1 == tg2) &&
beq_nat (List.length l1) (List.length l2) &&
forallb (fun x => match x with
((s1, t1'), (s2, t2')) => (s1 == s2) && eqt' m t1' t2'
end) (combine l1 l2)
| rtyp tg1 , ptyp (styp tg2 _) => tg1 == tg2
| ptyp (styp tg2 _), rtyp tg1 => tg1 == tg2
| _, _ => false
end
end.
Definition eqt t1 t2 := eqt' (max (typ_max_depth t1) (typ_max_depth t2)) t1 t2.
Notation "t1 '=t=' t2" := (eqt t1 t2) (at level 75) : minC_types.
Local Open Scope minC_types.
Lemma eqt'_upper : forall t1 t2 n, max (typ_max_depth t1) (typ_max_depth t2) <= n ->
(t1 =t= t2) = eqt' n t1 t2.
Lemma eqt_refl : forall t, eqt t t.
Lemma eqt_ptyp_btyp_dis : forall a b, ~ ptyp a =t= btyp b.
Lemma eqt_ptyp_styp_dis : forall a tb lb, ~ ptyp a =t= styp tb lb.
Lemma eqt_btyp_styp_dis : forall a tb lb, ~ btyp a =t= styp tb lb.
Lemma eqt_rtyp_btyp_dis : forall a b, ~ rtyp a =t= btyp b.
Lemma eqt_styp_rtyp_dis : forall ta la b, ~ styp ta la =t= rtyp b.
Lemma eqt_ptyp : forall a b, a =t= b -> ptyp a =t= ptyp b.
Lemma eqt_ptyp_rtyp : forall a s l, a =t= styp s l -> ptyp a =t= rtyp s.
Lemma eqt_btyp_inj : forall a b, btyp a =t= btyp b -> a = b.
Lemma eqt_ptyp_inj : forall a b, ptyp a =t= ptyp b -> a =t= b.
Lemma eqt_rtyp_inj : forall a b, rtyp a =t= rtyp b -> a = b.
Lemma eqt_ptyp_styp_rtyp_inj : forall s l s', ptyp (styp s l) =t= rtyp s' -> s = s'.
Definition eqt_list l1 l2 :=
beq_nat (List.length l1) (List.length l2) &&
forallb (fun x =>
match x with
((s1, t1), (s2, t2)) => (s1 == s2 :> string) && (t1 =t= t2)
end) (combine l1 l2).
Lemma eqt_styp_inv : forall ta tb la lb, styp ta la =t= styp tb lb ->
(ta == tb) && eqt_list la lb.
Lemma eqt_list_styp_inj : forall la lb ta tb, styp ta la =t= styp tb lb ->
ta = tb /\ eqt_list la lb.
Lemma eqt_styp_inv_cons : forall la lb ha hb ta tb,
styp ta (ha :: la) =t= styp tb (hb :: lb) ->
fst ha == fst hb /\
snd ha =t= snd hb /\
styp ta la =t= styp tb lb.
Lemma eqt_styp : forall la lb ha hb ta tb,
fst ha == fst hb ->
snd ha =t= snd hb ->
styp ta la =t= styp tb lb ->
styp ta (ha :: la) =t= styp tb (hb :: lb).
Lemma eqt_sym : forall a b, a =t= b -> b =t= a.
Lemma eqt_list_sym : forall l l', eqt_list l l' -> eqt_list l' l.
match n with
| O => match t1, t2 with
| btyp uint32, btyp uint32 => true
| btyp sint32, btyp sint32 => true
| btyp uchar , btyp uchar => true
| rtyp tg1 , rtyp tg2 => tg1 == tg2
| btyp uint32, btyp uchar => false
| btyp sint32, btyp uchar => false
| btyp uchar , btyp uint32 => false
| btyp uchar , btyp sint32 => false
| btyp uint32, btyp sint32 => false
| btyp sint32, btyp uint32 => false
| _ , ptyp _ => false
| ptyp _ , _ => false
| btyp _ , rtyp _ => false
| rtyp _ , btyp _ => false
| styp _ _ , _ => false
| _ , styp _ _ => false
end
| S m => match t1, t2 with
| btyp uint32, btyp uint32 => true
| btyp sint32, btyp sint32 => true
| btyp uchar , btyp uchar => true
| rtyp tg1 , rtyp tg2 => tg1 == tg2
| btyp uint32, btyp uchar => false
| btyp sint32, btyp uchar => false
| btyp uchar , btyp uint32 => false
| btyp uchar , btyp sint32 => false
| btyp uint32, btyp sint32 => false
| btyp sint32, btyp uint32 => false
| ptyp t1' , ptyp t2' => eqt' m t1' t2'
| styp tg1 l1 , styp tg2 l2 => (tg1 == tg2) &&
beq_nat (List.length l1) (List.length l2) &&
forallb (fun x => match x with
((s1, t1'), (s2, t2')) => (s1 == s2) && eqt' m t1' t2'
end) (combine l1 l2)
| rtyp tg1 , ptyp (styp tg2 _) => tg1 == tg2
| ptyp (styp tg2 _), rtyp tg1 => tg1 == tg2
| _, _ => false
end
end.
Definition eqt t1 t2 := eqt' (max (typ_max_depth t1) (typ_max_depth t2)) t1 t2.
Notation "t1 '=t=' t2" := (eqt t1 t2) (at level 75) : minC_types.
Local Open Scope minC_types.
Lemma eqt'_upper : forall t1 t2 n, max (typ_max_depth t1) (typ_max_depth t2) <= n ->
(t1 =t= t2) = eqt' n t1 t2.
Lemma eqt_refl : forall t, eqt t t.
Lemma eqt_ptyp_btyp_dis : forall a b, ~ ptyp a =t= btyp b.
Lemma eqt_ptyp_styp_dis : forall a tb lb, ~ ptyp a =t= styp tb lb.
Lemma eqt_btyp_styp_dis : forall a tb lb, ~ btyp a =t= styp tb lb.
Lemma eqt_rtyp_btyp_dis : forall a b, ~ rtyp a =t= btyp b.
Lemma eqt_styp_rtyp_dis : forall ta la b, ~ styp ta la =t= rtyp b.
Lemma eqt_ptyp : forall a b, a =t= b -> ptyp a =t= ptyp b.
Lemma eqt_ptyp_rtyp : forall a s l, a =t= styp s l -> ptyp a =t= rtyp s.
Lemma eqt_btyp_inj : forall a b, btyp a =t= btyp b -> a = b.
Lemma eqt_ptyp_inj : forall a b, ptyp a =t= ptyp b -> a =t= b.
Lemma eqt_rtyp_inj : forall a b, rtyp a =t= rtyp b -> a = b.
Lemma eqt_ptyp_styp_rtyp_inj : forall s l s', ptyp (styp s l) =t= rtyp s' -> s = s'.
Definition eqt_list l1 l2 :=
beq_nat (List.length l1) (List.length l2) &&
forallb (fun x =>
match x with
((s1, t1), (s2, t2)) => (s1 == s2 :> string) && (t1 =t= t2)
end) (combine l1 l2).
Lemma eqt_styp_inv : forall ta tb la lb, styp ta la =t= styp tb lb ->
(ta == tb) && eqt_list la lb.
Lemma eqt_list_styp_inj : forall la lb ta tb, styp ta la =t= styp tb lb ->
ta = tb /\ eqt_list la lb.
Lemma eqt_styp_inv_cons : forall la lb ha hb ta tb,
styp ta (ha :: la) =t= styp tb (hb :: lb) ->
fst ha == fst hb /\
snd ha =t= snd hb /\
styp ta la =t= styp tb lb.
Lemma eqt_styp : forall la lb ha hb ta tb,
fst ha == fst hb ->
snd ha =t= snd hb ->
styp ta la =t= styp tb lb ->
styp ta (ha :: la) =t= styp tb (hb :: lb).
Lemma eqt_sym : forall a b, a =t= b -> b =t= a.
Lemma eqt_list_sym : forall l l', eqt_list l l' -> eqt_list l' l.
a context associates a tag with a list of "field/type"'s
"r_cover g t" =def= "the rtags in t appear in g"
Definition rcover (g : ctxt) (t : typ) := incl (rtags t) (uzip1 g).
Lemma rcover_ptyp_inv : forall t g, rcover g (ptyp t) -> rcover g t.
Lemma rcover_styp_inv1 : forall g tag h t, rcover g (styp tag (h :: t)) -> rcover g (snd h).
Lemma rcover_styp_inv2 : forall g tag h t, rcover g (styp tag (h :: t)) -> rcover g (styp tag t).
Lemma rcover_styp_inv : forall s tg l, rcover s (styp tg l) ->
forall t1, In t1 (Lists_ext.uzip2 l) -> rcover s t1.
Lemma rcover_ptyp_inv : forall t g, rcover g (ptyp t) -> rcover g t.
Lemma rcover_styp_inv1 : forall g tag h t, rcover g (styp tag (h :: t)) -> rcover g (snd h).
Lemma rcover_styp_inv2 : forall g tag h t, rcover g (styp tag (h :: t)) -> rcover g (styp tag t).
Lemma rcover_styp_inv : forall s tg l, rcover s (styp tg l) ->
forall t1, In t1 (Lists_ext.uzip2 l) -> rcover s t1.
"cover g t" =def= "the tags in t appear in g"
Definition cover (g : ctxt) (t : typ) := rcover g t /\ incl (stags t) g.
Lemma cover_btyp : forall g i, cover g (btyp i).
Lemma cover_ptyp : forall g t, cover g t -> cover g (ptyp t).
Lemma cover_cons : forall hd tl t, cover tl t ->
cover (hd :: tl) t.
Lemma cover_rtyp : forall s tg l, assoc_get tg s = Some l -> cover s (rtyp tg).
Lemma cover_ptyp_inv : forall t g, cover g (ptyp t) -> cover g t.
Lemma cover_styp_inv1 : forall (g : ctxt) tag fld flds,
cover g (styp tag (fld :: flds)) -> cover g (snd fld).
Lemma cover_styp_inv : forall s tg l, cover s (styp tg l) ->
forall t1, In t1 (Lists_ext.uzip2 l) -> cover s t1.
Lemma cover_btyp : forall g i, cover g (btyp i).
Lemma cover_ptyp : forall g t, cover g t -> cover g (ptyp t).
Lemma cover_cons : forall hd tl t, cover tl t ->
cover (hd :: tl) t.
Lemma cover_rtyp : forall s tg l, assoc_get tg s = Some l -> cover s (rtyp tg).
Lemma cover_ptyp_inv : forall t g, cover g (ptyp t) -> cover g t.
Lemma cover_styp_inv1 : forall (g : ctxt) tag fld flds,
cover g (styp tag (fld :: flds)) -> cover g (snd fld).
Lemma cover_styp_inv : forall s tg l, cover s (styp tg l) ->
forall t1, In t1 (Lists_ext.uzip2 l) -> cover s t1.
a relation between types, parameterize by a context, that behaves like an equality
Definition eqtm (c : ctxt) (t1 t2 : typ) := t1 =t= t2 /\ cover c t1 /\ cover c t2.
Notation "t1 '=t' g 't=' t2" := (eqtm g t1 t2) (at level 75) : minC_types.
Lemma eqtm_refl : forall (g : ctxt) (a : typ), cover g a -> a =t g t= a.
Lemma eqt_eqtm_refl : forall g t1 t2, cover g t1 -> cover g t2 -> t1 =t= t2 -> t1 =t g t= t2.
Lemma eqtm_sym : forall g a b, a =t g t= b -> b =t g t= a.
Lemma eqtm_ptyp : forall g a b, a =t g t= b -> ptyp a =t g t= ptyp b.
Lemma eqtm_btyp_ptyp_dis : forall s i t, ~ btyp i =t s t= ptyp t.
Lemma eqtm_styp_ptyp_dis : forall g a b t, ~ styp a b =t g t= ptyp t.
Lemma eqtm_rtyp_ptyp_btyp_dis : forall g s i, ~ rtyp s =t g t= ptyp (btyp i).
Lemma eqtm_rtyp_ptyp_ptyp_dis : forall g s t, ~ rtyp s =t g t= ptyp (ptyp t).
Lemma eqtm_rtyp_ptyp_rtyp_dis : forall g s t, ~ rtyp s =t g t= ptyp (rtyp t).
Lemma eqtm_btyp_rtyp_dis : forall g i0 s, ~ btyp i0 =t g t= rtyp s.
Lemma eqtm_btyp_styp_dis : forall g i0 s l, ~ btyp i0 =t g t= styp s l.
Lemma eqtm_rtyp_styp_dis : forall g t s l, ~ rtyp t =t g t= styp s l.
Ltac eqtm_dis :=
match goal with
| H : eqtm _ (btyp ?i) (ptyp ?t) |- _ =>
by move/eqtm_btyp_ptyp_dis : H
| H : eqtm _ (ptyp ?i) (btyp ?t) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_ptyp_dis
| H : eqtm _ (btyp ?i) (rtyp ?t) |- _ =>
by move/eqtm_btyp_rtyp_dis : H
| H : eqtm _ (rtyp ?t) (btyp ?i) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_rtyp_dis
| H : eqtm _ (btyp ?i) (styp ?s ?t) |- _ =>
by move/eqtm_btyp_styp_dis : H
| H : eqtm _ (styp ?s ?t) (btyp ?i) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_styp_dis
| H : eqtm _ (rtyp ?t) (styp ?s ?l) |- _ =>
by move/eqtm_rtyp_styp_dis : H
| H : eqtm _ (styp ?s ?l) (rtyp ?t) |- _ =>
move/eqtm_sym : H; by move/eqtm_rtyp_styp_dis
| H : eqtm _ (styp ?a ?b) (ptyp ?t) |- _ =>
by move/eqtm_styp_ptyp_dis : H
| H : eqtm _ (ptyp ?t) (styp ?a ?b) |- _ =>
move/eqtm_sym : H; by move/eqtm_styp_ptyp_dis
| H : eqtm _ (rtyp ?s) (ptyp (btyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_btyp_dis : H
| H : eqtm _ (rtyp ?s) (ptyp (ptyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_ptyp_dis : H
| H : eqtm _ (rtyp ?s) (ptyp (rtyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_rtyp_dis : H
end.
Lemma eqtm_rtyp_ptyp_inv : forall g s t, rtyp s =t g t= ptyp t ->
exists l, t = styp s l.
Lemma eqtm_ptyp_inj : forall g a b, ptyp a =t g t= ptyp b -> a =t g t= b.
Lemma eqtm_btyp_inj : forall (g : ctxt) (a b : ityp), btyp a =t g t= btyp b -> a = b.
Lemma eqtm_ptyp_btyp_inv : forall t g i,
t =t g t= ptyp (btyp i) -> t = ptyp (btyp i).
Lemma eqtm_btyp_inv : forall t g i, t =t g t= btyp i -> t = btyp i.
Lemma eqtm_styp_inv : forall t g tg lst, t =t g t= (styp tg lst) ->
exists lst', eqt_list lst lst' /\ t = styp tg lst'.
Notation "t1 '=t' g 't=' t2" := (eqtm g t1 t2) (at level 75) : minC_types.
Lemma eqtm_refl : forall (g : ctxt) (a : typ), cover g a -> a =t g t= a.
Lemma eqt_eqtm_refl : forall g t1 t2, cover g t1 -> cover g t2 -> t1 =t= t2 -> t1 =t g t= t2.
Lemma eqtm_sym : forall g a b, a =t g t= b -> b =t g t= a.
Lemma eqtm_ptyp : forall g a b, a =t g t= b -> ptyp a =t g t= ptyp b.
Lemma eqtm_btyp_ptyp_dis : forall s i t, ~ btyp i =t s t= ptyp t.
Lemma eqtm_styp_ptyp_dis : forall g a b t, ~ styp a b =t g t= ptyp t.
Lemma eqtm_rtyp_ptyp_btyp_dis : forall g s i, ~ rtyp s =t g t= ptyp (btyp i).
Lemma eqtm_rtyp_ptyp_ptyp_dis : forall g s t, ~ rtyp s =t g t= ptyp (ptyp t).
Lemma eqtm_rtyp_ptyp_rtyp_dis : forall g s t, ~ rtyp s =t g t= ptyp (rtyp t).
Lemma eqtm_btyp_rtyp_dis : forall g i0 s, ~ btyp i0 =t g t= rtyp s.
Lemma eqtm_btyp_styp_dis : forall g i0 s l, ~ btyp i0 =t g t= styp s l.
Lemma eqtm_rtyp_styp_dis : forall g t s l, ~ rtyp t =t g t= styp s l.
Ltac eqtm_dis :=
match goal with
| H : eqtm _ (btyp ?i) (ptyp ?t) |- _ =>
by move/eqtm_btyp_ptyp_dis : H
| H : eqtm _ (ptyp ?i) (btyp ?t) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_ptyp_dis
| H : eqtm _ (btyp ?i) (rtyp ?t) |- _ =>
by move/eqtm_btyp_rtyp_dis : H
| H : eqtm _ (rtyp ?t) (btyp ?i) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_rtyp_dis
| H : eqtm _ (btyp ?i) (styp ?s ?t) |- _ =>
by move/eqtm_btyp_styp_dis : H
| H : eqtm _ (styp ?s ?t) (btyp ?i) |- _ =>
move/eqtm_sym : H; by move/eqtm_btyp_styp_dis
| H : eqtm _ (rtyp ?t) (styp ?s ?l) |- _ =>
by move/eqtm_rtyp_styp_dis : H
| H : eqtm _ (styp ?s ?l) (rtyp ?t) |- _ =>
move/eqtm_sym : H; by move/eqtm_rtyp_styp_dis
| H : eqtm _ (styp ?a ?b) (ptyp ?t) |- _ =>
by move/eqtm_styp_ptyp_dis : H
| H : eqtm _ (ptyp ?t) (styp ?a ?b) |- _ =>
move/eqtm_sym : H; by move/eqtm_styp_ptyp_dis
| H : eqtm _ (rtyp ?s) (ptyp (btyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_btyp_dis : H
| H : eqtm _ (rtyp ?s) (ptyp (ptyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_ptyp_dis : H
| H : eqtm _ (rtyp ?s) (ptyp (rtyp ?i)) |- _ =>
by move/eqtm_rtyp_ptyp_rtyp_dis : H
end.
Lemma eqtm_rtyp_ptyp_inv : forall g s t, rtyp s =t g t= ptyp t ->
exists l, t = styp s l.
Lemma eqtm_ptyp_inj : forall g a b, ptyp a =t g t= ptyp b -> a =t g t= b.
Lemma eqtm_btyp_inj : forall (g : ctxt) (a b : ityp), btyp a =t g t= btyp b -> a = b.
Lemma eqtm_ptyp_btyp_inv : forall t g i,
t =t g t= ptyp (btyp i) -> t = ptyp (btyp i).
Lemma eqtm_btyp_inv : forall t g i, t =t g t= btyp i -> t = btyp i.
Lemma eqtm_styp_inv : forall t g tg lst, t =t g t= (styp tg lst) ->
exists lst', eqt_list lst lst' /\ t = styp tg lst'.
the context is a map
Definition map_ctxt (g : ctxt) := nodup (uzip1 g).
Lemma eqtm_rtyp_ptyp_inv2 : forall g tg l, map_ctxt g ->
rtyp tg =t g t= ptyp (styp tg l) -> assoc_get tg g = Some l.
Fixpoint canon_typ (t : typ) : typ :=
match t with
| btyp _ => t
| ptyp t' =>
match t' with
| styp tg _ => rtyp tg
| _ => ptyp (canon_typ t')
end
| rtyp _ => t
| styp _ _ => t
end.
Lemma canon_typ_idem : forall t,
canon_typ t = canon_typ (canon_typ t).
Lemma eqtm_canon_typ_P : forall g (Hg : map_ctxt g) t1 t2,
t1 =t g t= t2 <-> canon_typ t1 = canon_typ t2 /\ cover g t1 /\ cover g t2.
Lemma eqtm_trans : forall a g (Hg : map_ctxt g) b c,
a =t g t= b -> b =t g t= c -> a =t g t= c.
Definition sizeof_i t : nat :=
match t with uint32 => 4 | sint32 => 4 | uchar => 1 end.
Definition align_ityp t : nat :=
match t with uint32 => 4 | sint32 => 4 | uchar => 1 end.
Lemma eqtm_rtyp_ptyp_inv2 : forall g tg l, map_ctxt g ->
rtyp tg =t g t= ptyp (styp tg l) -> assoc_get tg g = Some l.
Fixpoint canon_typ (t : typ) : typ :=
match t with
| btyp _ => t
| ptyp t' =>
match t' with
| styp tg _ => rtyp tg
| _ => ptyp (canon_typ t')
end
| rtyp _ => t
| styp _ _ => t
end.
Lemma canon_typ_idem : forall t,
canon_typ t = canon_typ (canon_typ t).
Lemma eqtm_canon_typ_P : forall g (Hg : map_ctxt g) t1 t2,
t1 =t g t= t2 <-> canon_typ t1 = canon_typ t2 /\ cover g t1 /\ cover g t2.
Lemma eqtm_trans : forall a g (Hg : map_ctxt g) b c,
a =t g t= b -> b =t g t= c -> a =t g t= c.
Definition sizeof_i t : nat :=
match t with uint32 => 4 | sint32 => 4 | uchar => 1 end.
Definition align_ityp t : nat :=
match t with uint32 => 4 | sint32 => 4 | uchar => 1 end.
size in bytes, ignore padding issues
Fixpoint sizeof' (n : nat) (t : typ) : nat :=
match n with
| O =>
match t with
| btyp x => sizeof_i x
| ptyp _ => ptr_size
| rtyp _ => ptr_size
| styp _ _ => O
end
| S m =>
match t with
| btyp x => sizeof_i x
| ptyp _ => ptr_size
| rtyp _ => ptr_size
| styp _ l' => iplus (map (sizeof' m) (uzip2 l'))
end
end.
Definition sizeof t := sizeof' (typ_max_depth t) t.
Lemma sizeof'_upper : forall t n, typ_max_depth t <= n ->
sizeof' (typ_max_depth t) t = sizeof' n t .
Lemma sizeof_btyp : sizeof (btyp uchar) = 1%nat.
Lemma sizeof_ptyp : forall t, sizeof (ptyp t) = ptr_size.
Lemma sizeof_rtyp : forall tg, sizeof (rtyp tg) = ptr_size.
Lemma sizeof_styp_iplus : forall l s,
sizeof (styp s l) = iplus (map (fun x => sizeof (snd x)) l).
Lemma fold_left_inj_sizeof : forall {A C: Type} (f : A * list C -> typ -> A * list C)
lst h1 h2
(Hf : forall a1 k1 a2 k2 hd, In hd lst ->
sizeof hd <= length k1 ->
sizeof hd <= length k2 ->
f (a1, k1) hd = f (a2, k2) hd -> (a1, k1) = (a2, k2))
(Hf' : forall a h t a' h', f (a, h) t = (a', h') -> sizeof t + length h' >= length h)
a1 a2,
iplus (map sizeof lst) <= length h1 ->
iplus (map sizeof lst) <= length h2 ->
fold_left f lst (a1, h1) = fold_left f lst (a2, h2) ->
(a1, h1) = (a2, h2).
Lemma wft_sizeof : forall t, wft t -> O < sizeof t.
Lemma eqt_sizeof : forall t1 t2 : typ, t1 =t= t2 -> sizeof t1 = sizeof t2.
Lemma eqtm_sizeof : forall g (Hg : map_ctxt g) t1 t2, t1 =t g t= t2 ->
sizeof t1 = sizeof t2.
match n with
| O =>
match t with
| btyp x => sizeof_i x
| ptyp _ => ptr_size
| rtyp _ => ptr_size
| styp _ _ => O
end
| S m =>
match t with
| btyp x => sizeof_i x
| ptyp _ => ptr_size
| rtyp _ => ptr_size
| styp _ l' => iplus (map (sizeof' m) (uzip2 l'))
end
end.
Definition sizeof t := sizeof' (typ_max_depth t) t.
Lemma sizeof'_upper : forall t n, typ_max_depth t <= n ->
sizeof' (typ_max_depth t) t = sizeof' n t .
Lemma sizeof_btyp : sizeof (btyp uchar) = 1%nat.
Lemma sizeof_ptyp : forall t, sizeof (ptyp t) = ptr_size.
Lemma sizeof_rtyp : forall tg, sizeof (rtyp tg) = ptr_size.
Lemma sizeof_styp_iplus : forall l s,
sizeof (styp s l) = iplus (map (fun x => sizeof (snd x)) l).
Lemma fold_left_inj_sizeof : forall {A C: Type} (f : A * list C -> typ -> A * list C)
lst h1 h2
(Hf : forall a1 k1 a2 k2 hd, In hd lst ->
sizeof hd <= length k1 ->
sizeof hd <= length k2 ->
f (a1, k1) hd = f (a2, k2) hd -> (a1, k1) = (a2, k2))
(Hf' : forall a h t a' h', f (a, h) t = (a', h') -> sizeof t + length h' >= length h)
a1 a2,
iplus (map sizeof lst) <= length h1 ->
iplus (map sizeof lst) <= length h2 ->
fold_left f lst (a1, h1) = fold_left f lst (a2, h2) ->
(a1, h1) = (a2, h2).
Lemma wft_sizeof : forall t, wft t -> O < sizeof t.
Lemma eqt_sizeof : forall t1 t2 : typ, t1 =t= t2 -> sizeof t1 = sizeof t2.
Lemma eqtm_sizeof : forall g (Hg : map_ctxt g) t1 t2, t1 =t g t= t2 ->
sizeof t1 = sizeof t2.
all the elements in the context reprensent well-formed types
Definition wft_ctxt (g : ctxt) :=
forall a b, assoc_get a g = Some b -> wft (styp a b).
Lemma eqtm_wft : forall t1 t2 g,
map_ctxt g -> wft_ctxt g -> t1 =t g t= t2 -> wft t1 -> wft t2.
Definition eqt_list_ctxt g l1 l2 : Prop :=
List.length l1 = List.length l2 /\
forall x, In x (combine l1 l2) ->
match x with
((s1, t1), (s2, t2)) => (s1 == s2 :> string) /\ (t1 =t g t= t2)
end.
Lemma eqt_list_ctxt_iplus : forall g (Hg : map_ctxt g) l l',
eqt_list_ctxt g l l' ->
forall i,
iplus (map sizeof (firstn i (uzip2 l))) =
iplus (map sizeof (firstn i (uzip2 l'))).
Lemma eqt_list_ctxt_uzip1 : forall g l l', eqt_list_ctxt g l l' ->
Lists_ext.uzip1 l = Lists_ext.uzip1 l'.
Lemma eqtm_styp_inv_ctxt : forall t g tg lst,
t =t g t= styp tg lst ->
exists lst', eqt_list_ctxt g lst' lst /\ t = styp tg lst'.
Lemma eqt_list_ctxt_sym : forall g l l',
eqt_list_ctxt g l l' -> eqt_list_ctxt g l' l.
Lemma eqtm_ptyp_styp_inv : forall t g tg l,
t =t g t= ptyp (styp tg l) ->
t = rtyp tg \/
exists l', eqt_list_ctxt g l l' /\ t = ptyp (styp tg l').
Lemma eqt_list_assoc_get : forall l l', eqt_list l l' ->
forall st t, assoc_get st l = Some t ->
exists t', t =t= t' /\
assoc_get st l' = Some t'.
Lemma eqt_list_ctxt_assoc_get : forall g l l', eqt_list_ctxt g l l' ->
forall st t, assoc_get st l = Some t ->
exists t', t =t g t= t' /\
assoc_get st l' = Some t'.
Inductive value : Type :=
| bval32 of int 32
| bval8 of int 8
| pval of int ptr_len
| sval of list value.
forall a b, assoc_get a g = Some b -> wft (styp a b).
Lemma eqtm_wft : forall t1 t2 g,
map_ctxt g -> wft_ctxt g -> t1 =t g t= t2 -> wft t1 -> wft t2.
Definition eqt_list_ctxt g l1 l2 : Prop :=
List.length l1 = List.length l2 /\
forall x, In x (combine l1 l2) ->
match x with
((s1, t1), (s2, t2)) => (s1 == s2 :> string) /\ (t1 =t g t= t2)
end.
Lemma eqt_list_ctxt_iplus : forall g (Hg : map_ctxt g) l l',
eqt_list_ctxt g l l' ->
forall i,
iplus (map sizeof (firstn i (uzip2 l))) =
iplus (map sizeof (firstn i (uzip2 l'))).
Lemma eqt_list_ctxt_uzip1 : forall g l l', eqt_list_ctxt g l l' ->
Lists_ext.uzip1 l = Lists_ext.uzip1 l'.
Lemma eqtm_styp_inv_ctxt : forall t g tg lst,
t =t g t= styp tg lst ->
exists lst', eqt_list_ctxt g lst' lst /\ t = styp tg lst'.
Lemma eqt_list_ctxt_sym : forall g l l',
eqt_list_ctxt g l l' -> eqt_list_ctxt g l' l.
Lemma eqtm_ptyp_styp_inv : forall t g tg l,
t =t g t= ptyp (styp tg l) ->
t = rtyp tg \/
exists l', eqt_list_ctxt g l l' /\ t = ptyp (styp tg l').
Lemma eqt_list_assoc_get : forall l l', eqt_list l l' ->
forall st t, assoc_get st l = Some t ->
exists t', t =t= t' /\
assoc_get st l' = Some t'.
Lemma eqt_list_ctxt_assoc_get : forall g l l', eqt_list_ctxt g l l' ->
forall st t, assoc_get st l = Some t ->
exists t', t =t g t= t' /\
assoc_get st l' = Some t'.
Inductive value : Type :=
| bval32 of int 32
| bval8 of int 8
| pval of int ptr_len
| sval of list value.
some sample values
Definition int32_0 : value := bval32 (Z2s 32 0).
Definition char_0 : value := bval8 (Z2u 8 0).
Definition pval_0 : value := pval (Z2u ptr_len 0).
Section correct_value_ind.
Variables (P : value -> Prop) (Q : list value -> Prop).
Hypotheses (H : forall l, Q l -> P (sval l))
(H0 : Q nil)
(H1 : forall i : (int 32), P (bval32 i))
(H2 : forall i : (int 8), P (bval8 i))
(H3 : forall i : (int ptr_len), P (pval i))
(H4 : forall t, P t -> forall l, Q l -> Q ((t) :: l)).
Fixpoint value_ind_gen t : P t :=
match t as x return P x with
| bval32 i => H1 i
| bval8 i => H2 i
| pval i => H3 i
| sval l => H l ((fix v_ind l' : Q l' :=
match l' as x return Q x with
| nil => H0
| cons t1 tl => H4 t1 (value_ind_gen t1) tl (v_ind tl)
end) l)
end.
End correct_value_ind.
Lemma value_ind_new : forall P : value -> Prop,
(forall i, P (bval32 i)) ->
(forall i, P (bval8 i)) ->
(forall i, P (pval i)) ->
(forall l, (forall x, In x l -> P x) -> P (sval l)) ->
forall t, P t.
Fixpoint typ_val' (n : nat) (t : typ) (v : value) : bool :=
match n with
| O => match t, v with
| btyp uint32, bval32 _ => true
| btyp sint32, bval32 _ => true
| btyp uchar , bval8 _ => true
| btyp uint32, bval8 _ => false
| btyp sint32, bval8 _ => false
| btyp uchar , bval32 _ => false
| btyp uint32, pval _ => false
| btyp sint32, pval _ => false
| btyp uchar , pval _ => false
| btyp uint32, sval _ => false
| btyp sint32, sval _ => false
| btyp uchar , sval _ => false
| rtyp tg , pval v => true
| rtyp _ , bval32 _ => false
| rtyp _ , bval8 _ => false
| rtyp _ , sval _ => false
| ptyp _ , _ => false
| styp _ _, _ => false
end
| S m => match t, v with
| btyp uint32, bval32 _ => true
| btyp sint32, bval32 _ => true
| btyp uchar , bval8 _ => true
| btyp uint32, bval8 _ => false
| btyp sint32, bval8 _ => false
| btyp uchar , bval32 _ => false
| btyp uint32, pval _ => false
| btyp sint32, pval _ => false
| btyp uchar , pval _ => false
| btyp uint32, sval _ => false
| btyp sint32, sval _ => false
| btyp uchar , sval _ => false
| rtyp _ , pval _ => true
| ptyp t , pval _ => true
| styp s l, sval l' =>
beq_nat (length l) (length l') &&
forallb (fun a_b => typ_val' m (fst a_b) (snd a_b)) (combine (uzip2 l) l')
| _ , _ => false
end
end.
Definition char_0 : value := bval8 (Z2u 8 0).
Definition pval_0 : value := pval (Z2u ptr_len 0).
Section correct_value_ind.
Variables (P : value -> Prop) (Q : list value -> Prop).
Hypotheses (H : forall l, Q l -> P (sval l))
(H0 : Q nil)
(H1 : forall i : (int 32), P (bval32 i))
(H2 : forall i : (int 8), P (bval8 i))
(H3 : forall i : (int ptr_len), P (pval i))
(H4 : forall t, P t -> forall l, Q l -> Q ((t) :: l)).
Fixpoint value_ind_gen t : P t :=
match t as x return P x with
| bval32 i => H1 i
| bval8 i => H2 i
| pval i => H3 i
| sval l => H l ((fix v_ind l' : Q l' :=
match l' as x return Q x with
| nil => H0
| cons t1 tl => H4 t1 (value_ind_gen t1) tl (v_ind tl)
end) l)
end.
End correct_value_ind.
Lemma value_ind_new : forall P : value -> Prop,
(forall i, P (bval32 i)) ->
(forall i, P (bval8 i)) ->
(forall i, P (pval i)) ->
(forall l, (forall x, In x l -> P x) -> P (sval l)) ->
forall t, P t.
Fixpoint typ_val' (n : nat) (t : typ) (v : value) : bool :=
match n with
| O => match t, v with
| btyp uint32, bval32 _ => true
| btyp sint32, bval32 _ => true
| btyp uchar , bval8 _ => true
| btyp uint32, bval8 _ => false
| btyp sint32, bval8 _ => false
| btyp uchar , bval32 _ => false
| btyp uint32, pval _ => false
| btyp sint32, pval _ => false
| btyp uchar , pval _ => false
| btyp uint32, sval _ => false
| btyp sint32, sval _ => false
| btyp uchar , sval _ => false
| rtyp tg , pval v => true
| rtyp _ , bval32 _ => false
| rtyp _ , bval8 _ => false
| rtyp _ , sval _ => false
| ptyp _ , _ => false
| styp _ _, _ => false
end
| S m => match t, v with
| btyp uint32, bval32 _ => true
| btyp sint32, bval32 _ => true
| btyp uchar , bval8 _ => true
| btyp uint32, bval8 _ => false
| btyp sint32, bval8 _ => false
| btyp uchar , bval32 _ => false
| btyp uint32, pval _ => false
| btyp sint32, pval _ => false
| btyp uchar , pval _ => false
| btyp uint32, sval _ => false
| btyp sint32, sval _ => false
| btyp uchar , sval _ => false
| rtyp _ , pval _ => true
| ptyp t , pval _ => true
| styp s l, sval l' =>
beq_nat (length l) (length l') &&
forallb (fun a_b => typ_val' m (fst a_b) (snd a_b)) (combine (uzip2 l) l')
| _ , _ => false
end
end.
check if a typ and a value are compatible
Definition typ_val t v := typ_val' (typ_max_depth t) t v.
Lemma typ_val_ptyp : forall t v, typ_val (ptyp t) (pval v).
Lemma typ_val'_upper : forall t v n, typ_max_depth t <= n ->
typ_val' (typ_max_depth t) t v = typ_val' n t v.
Lemma typ_val_styp_sval_cons : forall tg h t h' t',
typ_val (snd h) h' -> typ_val (styp tg t) (sval t') ->
typ_val (styp tg (h :: t)) (sval (h' :: t')).
Lemma typ_val_styp_sval_inv : forall t1 t2 v1 v2 tag,
typ_val (styp tag (t1 :: t2)) (sval (v1 :: v2)) ->
typ_val (snd t1) v1 /\ typ_val (styp tag t2) (sval v2).
Lemma typ_val_uchar_inv : forall (v : value), typ_val (btyp uchar) v ->
exists c, v = bval8 c.
Lemma typ_val_styp_inv : forall v s l, typ_val (styp s l) v ->
exists vs, length l = length vs /\
v = sval vs /\
forallb (fun x => typ_val (fst x) (snd x)) (combine (map (fun x => snd x) l) vs).
Lemma typ_val_ptyp_inv : forall v t, typ_val (ptyp t) v -> exists p, v = pval p.
Lemma typ_val_rtyp_inv : forall v t, typ_val (rtyp t) v -> exists p, v = pval p.
Lemma typ_val_bval32_inv : forall t i, typ_val t (bval32 i) ->
t = btyp uint32 \/ t = btyp sint32.
Lemma typ_val_bval8_inv : forall (t : typ) (i : int 8), typ_val t (bval8 i) ->
t = btyp uchar.
Lemma typ_val_pval_inv : forall t v, typ_val t (pval v) ->
(exists t', t = ptyp t') \/ exists tag, t = rtyp tag.
Lemma typ_val_sval_inv : forall t vs, typ_val t (sval vs) ->
exists tag, exists l, t = styp tag l /\
length l = length vs /\
forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) vs).
Lemma typ_val_eqtm : forall t g (Hg : map_ctxt g) t' v,
typ_val t v -> t =t g t= t' -> typ_val t' v.
Definition ptr_to_int8 : int ptr_len -> list (int 8) := int_div_list _ _ _ Hptr_size.
Definition int8_to_ptr : list (int 8) -> option (int ptr_len) := int_mul_list _ _ _ Hptr_size.
Definition int32_to_int8 : int 32 -> list (int 8) := int_div_list 32 8 4 (refl_equal _).
Definition int8_to_int32 : list (int 8) -> option (int 32) := int_mul_list 32 8 4 (refl_equal _).
Lemma typ_val_ptyp : forall t v, typ_val (ptyp t) (pval v).
Lemma typ_val'_upper : forall t v n, typ_max_depth t <= n ->
typ_val' (typ_max_depth t) t v = typ_val' n t v.
Lemma typ_val_styp_sval_cons : forall tg h t h' t',
typ_val (snd h) h' -> typ_val (styp tg t) (sval t') ->
typ_val (styp tg (h :: t)) (sval (h' :: t')).
Lemma typ_val_styp_sval_inv : forall t1 t2 v1 v2 tag,
typ_val (styp tag (t1 :: t2)) (sval (v1 :: v2)) ->
typ_val (snd t1) v1 /\ typ_val (styp tag t2) (sval v2).
Lemma typ_val_uchar_inv : forall (v : value), typ_val (btyp uchar) v ->
exists c, v = bval8 c.
Lemma typ_val_styp_inv : forall v s l, typ_val (styp s l) v ->
exists vs, length l = length vs /\
v = sval vs /\
forallb (fun x => typ_val (fst x) (snd x)) (combine (map (fun x => snd x) l) vs).
Lemma typ_val_ptyp_inv : forall v t, typ_val (ptyp t) v -> exists p, v = pval p.
Lemma typ_val_rtyp_inv : forall v t, typ_val (rtyp t) v -> exists p, v = pval p.
Lemma typ_val_bval32_inv : forall t i, typ_val t (bval32 i) ->
t = btyp uint32 \/ t = btyp sint32.
Lemma typ_val_bval8_inv : forall (t : typ) (i : int 8), typ_val t (bval8 i) ->
t = btyp uchar.
Lemma typ_val_pval_inv : forall t v, typ_val t (pval v) ->
(exists t', t = ptyp t') \/ exists tag, t = rtyp tag.
Lemma typ_val_sval_inv : forall t vs, typ_val t (sval vs) ->
exists tag, exists l, t = styp tag l /\
length l = length vs /\
forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) vs).
Lemma typ_val_eqtm : forall t g (Hg : map_ctxt g) t' v,
typ_val t v -> t =t g t= t' -> typ_val t' v.
Definition ptr_to_int8 : int ptr_len -> list (int 8) := int_div_list _ _ _ Hptr_size.
Definition int8_to_ptr : list (int 8) -> option (int ptr_len) := int_mul_list _ _ _ Hptr_size.
Definition int32_to_int8 : int 32 -> list (int 8) := int_div_list 32 8 4 (refl_equal _).
Definition int8_to_int32 : list (int 8) -> option (int 32) := int_mul_list 32 8 4 (refl_equal _).
if the buffer does not contain enough bytes then it returns 0 and does not touch the buffer
Fixpoint chars2val' n t (buf : list (int 8)) {struct n} : (value * list (int 8)) :=
match n with
| O =>
match t with
| btyp uint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp sint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp uchar => if head buf is Some x then (bval8 x, tail buf) else (bval8 (Z2u 8 0), buf)
| rtyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| ptyp _ => (bval8 (Z2u 8 0), buf)
| styp _ _ => (bval8 (Z2u 8 0), buf)
end
| S m =>
match t with
| btyp uint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp sint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp uchar => if head buf is Some x then (bval8 x, tail buf) else (bval8 (Z2u 8 0), buf)
| ptyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| rtyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| styp s l =>
let subtree := fold_left
(fun a e => match a with
| (vs, b) =>
match chars2val' m e b with
| (v, b') => (vs ++ v :: nil, b')
end
end)
(uzip2 l) (nil, buf) in
match subtree with (vs, buf') => (sval vs, buf') end
end
end.
Lemma chars2val'_upper : forall t v n, typ_max_depth t <= n ->
chars2val' (typ_max_depth t) t v = chars2val' n t v.
Lemma chars2val'_styp_acc_val_end : forall (typs : list typ) (vs vs' : list value) (n : nat) (buf : list (int 8)),
fold_left (fun a e => match a with
| (vs, b) =>
match chars2val' n e b with
| (v, b') => (vs ++ v :: nil, b')
end
end) typs
(vs ++ vs', buf)
=
match
fold_left (fun a e => match a with
| (vs, b) =>
match chars2val' n e b with
| (v, b') => (vs ++ v :: nil, b')
end
end) typs
(vs', buf) with
(vs'_, buf') => (vs ++ vs'_, buf')
end.
Definition chars2val t := chars2val' (typ_max_depth t) t.
Lemma chars2val_styp_cons : forall s a va l vl b,
chars2val (snd a) b = (va, skipn (sizeof (snd a)) b) ->
chars2val (styp s l) (skipn (sizeof (snd a)) b) =
(sval vl, skipn (sizeof (styp s l)) (skipn (sizeof (snd a)) b)) ->
chars2val (styp s (a :: l)) b = (sval (va :: vl), skipn (sizeof (styp s (a :: l))) b).
match n with
| O =>
match t with
| btyp uint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp sint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp uchar => if head buf is Some x then (bval8 x, tail buf) else (bval8 (Z2u 8 0), buf)
| rtyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| ptyp _ => (bval8 (Z2u 8 0), buf)
| styp _ _ => (bval8 (Z2u 8 0), buf)
end
| S m =>
match t with
| btyp uint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp sint32 =>
if int8_to_int32 (firstn 4 buf) is Some x then (bval32 x, skipn 4 buf) else (bval32 zero32, buf)
| btyp uchar => if head buf is Some x then (bval8 x, tail buf) else (bval8 (Z2u 8 0), buf)
| ptyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| rtyp _ => if int8_to_ptr (firstn ptr_size buf) is Some x then (pval x, skipn ptr_size buf) else
(pval (Z2u ptr_len 0), buf)
| styp s l =>
let subtree := fold_left
(fun a e => match a with
| (vs, b) =>
match chars2val' m e b with
| (v, b') => (vs ++ v :: nil, b')
end
end)
(uzip2 l) (nil, buf) in
match subtree with (vs, buf') => (sval vs, buf') end
end
end.
Lemma chars2val'_upper : forall t v n, typ_max_depth t <= n ->
chars2val' (typ_max_depth t) t v = chars2val' n t v.
Lemma chars2val'_styp_acc_val_end : forall (typs : list typ) (vs vs' : list value) (n : nat) (buf : list (int 8)),
fold_left (fun a e => match a with
| (vs, b) =>
match chars2val' n e b with
| (v, b') => (vs ++ v :: nil, b')
end
end) typs
(vs ++ vs', buf)
=
match
fold_left (fun a e => match a with
| (vs, b) =>
match chars2val' n e b with
| (v, b') => (vs ++ v :: nil, b')
end
end) typs
(vs', buf) with
(vs'_, buf') => (vs ++ vs'_, buf')
end.
Definition chars2val t := chars2val' (typ_max_depth t) t.
Lemma chars2val_styp_cons : forall s a va l vl b,
chars2val (snd a) b = (va, skipn (sizeof (snd a)) b) ->
chars2val (styp s l) (skipn (sizeof (snd a)) b) =
(sval vl, skipn (sizeof (styp s l)) (skipn (sizeof (snd a)) b)) ->
chars2val (styp s (a :: l)) b = (sval (va :: vl), skipn (sizeof (styp s (a :: l))) b).
proves the correctness of the chars2val function (w.r.t., typ_val)
NB: does not require that t is wft
Lemma chars2val_typ_val : forall t l, sizeof t <= length l ->
exists v, chars2val t l = (v, skipn (sizeof t) l) /\ typ_val t v.
Lemma chars2val_same_layout : forall t g (Hg : map_ctxt g) t' l,
t =t g t= t' -> chars2val t l = chars2val t' l.
Lemma chars2val_styp_inv : forall s h t l v vs,
sizeof (styp s (h :: t)) <= length l ->
chars2val (styp s (h :: t)) l = (sval (v :: vs), skipn (sizeof (styp s (h :: t))) l) ->
chars2val (snd h) l = (v, skipn (sizeof (snd h)) l) /\
chars2val (styp s t) (skipn (sizeof (snd h)) l) =
(sval vs, skipn (sizeof (styp s t)) (skipn (sizeof (snd h)) l)).
Lemma chars2val_styp_inv_nth : forall h s l v, sizeof (styp s h) <= length l ->
chars2val (styp s h) l = (sval v, skipn (sizeof (styp s h)) l) ->
forall f idx t,
ifind f (uzip1 h) = Some idx ->
assoc_get f h = Some t ->
forall g t', map_ctxt g -> t =t g t= t' ->
chars2val t' (skipn (iplus (map sizeof (firstn idx (uzip2 h)))) l) =
(nth idx v (pval (Z2u ptr_len 0)), skipn (iplus (map sizeof (firstn (S idx) (uzip2 h)))) l).
Lemma chars2val_inj : forall t h1 h2, sizeof t <= length h1 ->
sizeof t <= length h2 -> chars2val t h1 = chars2val t h2 -> h1 = h2.
Lemma chars2val_app : forall m l t v k, sizeof t <= length l ->
chars2val t l = (v, k) -> chars2val t (l ++ m) = (v, k ++ m).
Lemma chars2val_firstn : forall t l v k, sizeof t <= length l ->
chars2val t l = (v, k) ->
chars2val t (firstn (sizeof t) l) = (v, nil).
Fixpoint val2chars' n (v : value) (t : typ) {struct n} : list (int 8) :=
match n with
| O =>
match v, t with
| bval32 i, btyp uint32 => int32_to_int8 i
| bval32 i, btyp sint32 => int32_to_int8 i
| bval8 c, btyp uchar => c :: nil
| pval i, ptyp t' => ptr_to_int8 i
| pval i, rtyp tag => ptr_to_int8 i
| sval _ , _ => nil
| bval32 _, btyp uchar => nil
| bval32 _, ptyp _ => nil
| bval32 _, rtyp _ => nil
| bval32 _, styp _ _ => nil
| bval8 _, btyp uint32 => nil
| bval8 _, btyp sint32 => nil
| bval8 _, ptyp _ => nil
| bval8 _, rtyp _ => nil
| bval8 _, styp _ _ => nil
| pval _, btyp _ => nil
| pval _, styp _ _ => nil
end
| S m =>
match v, t with
| sval l, styp s' l' =>
list_flat
(fold_right
(fun e a => match e with (v, t) => val2chars' m v t end :: a)
nil (combine l (uzip2 l')))
| bval32 i, btyp uint32 => int32_to_int8 i
| bval32 i, btyp sint32 => int32_to_int8 i
| bval8 c, btyp uchar => c :: nil
| pval i, ptyp t' => ptr_to_int8 i
| pval i, rtyp tag => ptr_to_int8 i
| _, _ => nil
end
end.
Fixpoint val_max_depth v : nat :=
match v with
| bval32 _ => O
| bval8 _ => O
| pval _ => O
| sval l => S (max_list (map (fun x => val_max_depth x) l) O)
end.
Lemma val2chars'_upper : forall v t n, val_max_depth v <= n ->
val2chars' (val_max_depth v) v t = val2chars' n v t .
Definition val2chars v := val2chars' (val_max_depth v) v.
Lemma eqtm_val2chars : forall g (Hg : map_ctxt g) v t1 t2,
t1 =t g t= t2 -> val2chars v t1 = val2chars v t2.
Lemma len_val2chars_ok : forall v t, typ_val t v -> (List.length (val2chars v t) = sizeof t)%nat.
Lemma len_val2chars_bound : forall v t, length (val2chars v t) <= sizeof t.
Lemma val2chars_sval_styp : forall v0 v1 tag hd tl,
val2chars (sval (v0 :: v1)) (styp tag (hd :: tl)) =
val2chars v0 (snd hd) ++ val2chars (sval v1) (styp tag tl).
Lemma chars2val_val2chars : forall t v, typ_val t v ->
chars2val t (val2chars v t) = (v, nil).
Fixpoint charss2vals' (t : typ) (lst : list (list (int 8))) : list value :=
match lst with
| nil => nil
| h :: rem =>
match chars2val t h with
| (x, nil) => x :: charss2vals' t rem
| (x, _ :: _) => nil
end
end.
Lemma len_charss2vals' : forall k l t, length l = k ->
(forall x, In x l -> length x = sizeof t) ->
length (charss2vals' t l) = k.
exists v, chars2val t l = (v, skipn (sizeof t) l) /\ typ_val t v.
Lemma chars2val_same_layout : forall t g (Hg : map_ctxt g) t' l,
t =t g t= t' -> chars2val t l = chars2val t' l.
Lemma chars2val_styp_inv : forall s h t l v vs,
sizeof (styp s (h :: t)) <= length l ->
chars2val (styp s (h :: t)) l = (sval (v :: vs), skipn (sizeof (styp s (h :: t))) l) ->
chars2val (snd h) l = (v, skipn (sizeof (snd h)) l) /\
chars2val (styp s t) (skipn (sizeof (snd h)) l) =
(sval vs, skipn (sizeof (styp s t)) (skipn (sizeof (snd h)) l)).
Lemma chars2val_styp_inv_nth : forall h s l v, sizeof (styp s h) <= length l ->
chars2val (styp s h) l = (sval v, skipn (sizeof (styp s h)) l) ->
forall f idx t,
ifind f (uzip1 h) = Some idx ->
assoc_get f h = Some t ->
forall g t', map_ctxt g -> t =t g t= t' ->
chars2val t' (skipn (iplus (map sizeof (firstn idx (uzip2 h)))) l) =
(nth idx v (pval (Z2u ptr_len 0)), skipn (iplus (map sizeof (firstn (S idx) (uzip2 h)))) l).
Lemma chars2val_inj : forall t h1 h2, sizeof t <= length h1 ->
sizeof t <= length h2 -> chars2val t h1 = chars2val t h2 -> h1 = h2.
Lemma chars2val_app : forall m l t v k, sizeof t <= length l ->
chars2val t l = (v, k) -> chars2val t (l ++ m) = (v, k ++ m).
Lemma chars2val_firstn : forall t l v k, sizeof t <= length l ->
chars2val t l = (v, k) ->
chars2val t (firstn (sizeof t) l) = (v, nil).
Fixpoint val2chars' n (v : value) (t : typ) {struct n} : list (int 8) :=
match n with
| O =>
match v, t with
| bval32 i, btyp uint32 => int32_to_int8 i
| bval32 i, btyp sint32 => int32_to_int8 i
| bval8 c, btyp uchar => c :: nil
| pval i, ptyp t' => ptr_to_int8 i
| pval i, rtyp tag => ptr_to_int8 i
| sval _ , _ => nil
| bval32 _, btyp uchar => nil
| bval32 _, ptyp _ => nil
| bval32 _, rtyp _ => nil
| bval32 _, styp _ _ => nil
| bval8 _, btyp uint32 => nil
| bval8 _, btyp sint32 => nil
| bval8 _, ptyp _ => nil
| bval8 _, rtyp _ => nil
| bval8 _, styp _ _ => nil
| pval _, btyp _ => nil
| pval _, styp _ _ => nil
end
| S m =>
match v, t with
| sval l, styp s' l' =>
list_flat
(fold_right
(fun e a => match e with (v, t) => val2chars' m v t end :: a)
nil (combine l (uzip2 l')))
| bval32 i, btyp uint32 => int32_to_int8 i
| bval32 i, btyp sint32 => int32_to_int8 i
| bval8 c, btyp uchar => c :: nil
| pval i, ptyp t' => ptr_to_int8 i
| pval i, rtyp tag => ptr_to_int8 i
| _, _ => nil
end
end.
Fixpoint val_max_depth v : nat :=
match v with
| bval32 _ => O
| bval8 _ => O
| pval _ => O
| sval l => S (max_list (map (fun x => val_max_depth x) l) O)
end.
Lemma val2chars'_upper : forall v t n, val_max_depth v <= n ->
val2chars' (val_max_depth v) v t = val2chars' n v t .
Definition val2chars v := val2chars' (val_max_depth v) v.
Lemma eqtm_val2chars : forall g (Hg : map_ctxt g) v t1 t2,
t1 =t g t= t2 -> val2chars v t1 = val2chars v t2.
Lemma len_val2chars_ok : forall v t, typ_val t v -> (List.length (val2chars v t) = sizeof t)%nat.
Lemma len_val2chars_bound : forall v t, length (val2chars v t) <= sizeof t.
Lemma val2chars_sval_styp : forall v0 v1 tag hd tl,
val2chars (sval (v0 :: v1)) (styp tag (hd :: tl)) =
val2chars v0 (snd hd) ++ val2chars (sval v1) (styp tag tl).
Lemma chars2val_val2chars : forall t v, typ_val t v ->
chars2val t (val2chars v t) = (v, nil).
Fixpoint charss2vals' (t : typ) (lst : list (list (int 8))) : list value :=
match lst with
| nil => nil
| h :: rem =>
match chars2val t h with
| (x, nil) => x :: charss2vals' t rem
| (x, _ :: _) => nil
end
end.
Lemma len_charss2vals' : forall k l t, length l = k ->
(forall x, In x l -> length x = sizeof t) ->
length (charss2vals' t l) = k.
turn a list of bytes into a list of values
(in other words, "extract" the list of values in a memory-allocated array)
Definition chars2vals (t : typ) (lst : list (int 8)) : list value :=
charss2vals' t (firstns (sizeof t) lst).
Lemma chars2vals_char : forall l, map (fun x : int 8 => bval8 x) l = chars2vals (btyp uchar) l.
Lemma chars2vals_prop : forall (lst : list (int 8)) (t : typ) k, wft t ->
length lst = k * sizeof t -> length (chars2vals t lst) = k.
Lemma chars2vals_app_cons : forall t l, wft t -> sizeof t <= length l ->
chars2vals t (firstn (sizeof t) l ++ skipn (sizeof t) l) =
(fst (chars2val t (firstn (sizeof t) l))) :: chars2vals t (skipn (sizeof t) l).
Lemma chars2vals_same_layout: forall t (g : ctxt), map_ctxt g ->
forall t' chars, t =t g t= t' ->
chars2vals t chars = chars2vals t' chars.
charss2vals' t (firstns (sizeof t) lst).
Lemma chars2vals_char : forall l, map (fun x : int 8 => bval8 x) l = chars2vals (btyp uchar) l.
Lemma chars2vals_prop : forall (lst : list (int 8)) (t : typ) k, wft t ->
length lst = k * sizeof t -> length (chars2vals t lst) = k.
Lemma chars2vals_app_cons : forall t l, wft t -> sizeof t <= length l ->
chars2vals t (firstn (sizeof t) l ++ skipn (sizeof t) l) =
(fst (chars2val t (firstn (sizeof t) l))) :: chars2vals t (skipn (sizeof t) l).
Lemma chars2vals_same_layout: forall t (g : ctxt), map_ctxt g ->
forall t' chars, t =t g t= t' ->
chars2vals t chars = chars2vals t' chars.