Library C_expr
Require Classical.
Require Import Permutation.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext String_ext Lists_ext Max_ext.
Require Import machine_int.
Import MachineInt.
Local Close Scope Z_scope.
Require Import C_types.
Definition complete (g : ctxt) :=
forall tag ss_ts, assoc_get tag g = Some ss_ts ->
forall t, In t (uzip2 ss_ts) ->
forall tag', In tag' (rtags t) ->
exists ss_ts', assoc_get tag' g = Some ss_ts'.
Definition var := string.
Definition eq_var := eq_string.
Inductive binop_e : Type := add_e | sub_e | mul_e | and_e | or_e | shl_e | le_e | lt_e | gt_e | land_e | lor_e
| eq_e | neq_e .
Inductive binop_pe : Type := peq_e.
Require Import Permutation.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext String_ext Lists_ext Max_ext.
Require Import machine_int.
Import MachineInt.
Local Close Scope Z_scope.
Require Import C_types.
Definition complete (g : ctxt) :=
forall tag ss_ts, assoc_get tag g = Some ss_ts ->
forall t, In t (uzip2 ss_ts) ->
forall tag', In tag' (rtags t) ->
exists ss_ts', assoc_get tag' g = Some ss_ts'.
Definition var := string.
Definition eq_var := eq_string.
Inductive binop_e : Type := add_e | sub_e | mul_e | and_e | or_e | shl_e | le_e | lt_e | gt_e | land_e | lor_e
| eq_e | neq_e .
Inductive binop_pe : Type := peq_e.
Modulo operation
This is a specialized version for powers of 2
E.g.,
<<
ciph_len mod 2 != 0
>>
becomes
<<
(bopk_ne mod2n_e (var_e "ciph_len") 1) \!=e cst32_0
>>
becomes 2 is 2^1
Inductive binopk_e : Type := mod2n_e.
Definition binop_e_interp b :=
match b with
| add_e => @add 32
| sub_e => @sub 32
| mul_e => @mul 32
| and_e => @int_and 32
| or_e => @int_or 32
| shl_e => fun a k : int 32 => @shl (Zabs_nat (u2Z k)) 32 a
| le_e => fun a b => if @le_n 32 a b then Z2u 32 1 else Z2u 32 0
| lt_e => fun a b => if @lt_n 32 a b then Z2u 32 1 else Z2u 32 0
| gt_e => fun a b => if @lt_n 32 b a then Z2u 32 1 else Z2u 32 0
| land_e => fun a b => if (u2Z a == Z0 ) || (u2Z b == Z0) then Z2u 32 0 else Z2u 32 1
| lor_e => fun a b => if (u2Z a == Z0) && (u2Z b == Z0) then Z2u 32 0 else Z2u 32 1
| eq_e => fun a b => if u2Z a == u2Z b then Z2u 32 1 else Z2u 32 0
| neq_e => fun a b => if u2Z a == u2Z b then Z2u 32 0 else Z2u 32 1
end.
Definition binop_e_interp8 b :=
match b with
| add_e => @add 8
| sub_e => @sub 8
| mul_e => @mul 8
| and_e => @int_and 8
| or_e => @int_or 8
| shl_e => fun a k : int 8 => @shl (Zabs_nat (u2Z k)) 8 a
| le_e => fun a b => if @le_n 8 a b then Z2u 8 1 else Z2u 8 0
| lt_e => fun a b => if @lt_n 8 a b then Z2u 8 1 else Z2u 8 0
| gt_e => fun a b => if @lt_n 8 b a then Z2u 8 1 else Z2u 8 0
| land_e => fun a b => if (u2Z a == Z0) || (u2Z b == Z0) then Z2u 8 0 else Z2u 8 1
| lor_e => fun a b => if (u2Z a == Z0) && (u2Z b == Z0) then Z2u 8 0 else Z2u 8 1
| eq_e => fun a b => if u2Z a == u2Z b then Z2u 8 1 else Z2u 8 0
| neq_e => fun a b => if u2Z a == u2Z b then Z2u 8 0 else Z2u 8 1
end.
Definition binopk_e_interp b :=
match b with
| mod2n_e => fun (a : int 32) (k : nat) => (@rem 32 _ (@rem k _ a))
end.
Definition binop_pe_interp b :=
match b with
| peq_e => fun (a b : int ptr_len) => if u2Z a == u2Z b then Z2u 32 1 else Z2u 32 0
end.
Inductive cast : Type := uchar_to_int.
Inductive exp : Type :=
| var_e of var
| cst32 of int 32
| cst8 of int 8
| cast_e of cast & exp
| bop_ne of binop_e & exp & exp
| bopk_ne of binopk_e & exp & nat
| ifte_e of exp & exp & exp
| fld of exp & string
| fld' of exp & string
| cst_pe : forall t : typ, wft t -> int ptr_len -> exp
| add_pe of exp & exp
| sub_pe of exp & exp
| bop_pe of exp & exp
| cst_se : forall tg l vs,
wft (styp tg l) -> length l = length vs ->
forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) vs) -> exp.
Implicit Arguments cst_pe [t].
Notation "'(c2i)' x" := (cast_e uchar_to_int x) (at level 58) : minC_expr_scope.
Notation "v 'CST_SE' Hv" := (cst_se _ _ v Hv (refl_equal _) (refl_equal _))
(at level 76, no associativity) : minC_expr_scope.
Notation "a '\+e' b" := (bop_ne add_e a b) (at level 60) : minC_expr_scope.
Notation "a '\-e' b" := (bop_ne sub_e a b) (at level 60) : minC_expr_scope.
Notation "a '\*e' b" := (bop_ne mul_e a b) (at level 59) : minC_expr_scope.
Notation "a '\&e' b" := (bop_ne and_e a b) (at level 60) : minC_expr_scope.
Notation "a '\|e' b" := (bop_ne or_e a b) (at level 60) : minC_expr_scope.
Notation "a '\<<e' b" := (bop_ne shl_e a b) (at level 60) : minC_expr_scope.
Notation "a '\%e' b" := (bopk_ne mod2n_e a b) (at level 60) : minC_expr_scope.
Notation "a '.\' b" := (fld a b) (at level 75) : minC_expr_scope.
Notation "a '.->' b" := (fld' a b) (at level 75) : minC_expr_scope.
Notation "a '\<=e' b" := (bop_ne le_e a b) (at level 60) : minC_expr_scope.
Notation "a '\<e' b" := (bop_ne lt_e a b) (at level 60) : minC_expr_scope.
Notation "a '\>e' b" := (bop_ne gt_e a b) (at level 60) : minC_expr_scope.
Notation "a '\&&e' b" := (bop_ne land_e a b) (at level 60) : minC_expr_scope.
Notation "a '\||e' b" := (bop_ne lor_e a b) (at level 60) : minC_expr_scope.
Notation "a '\=e' b" := (bop_ne eq_e a b) (at level 60) : minC_expr_scope.
Notation "a '\!=e' b" := (bop_ne neq_e a b) (at level 60) : minC_expr_scope.
Notation "a '\=pe' b" := (bop_pe a b) (at level 60) : minC_expr_scope.
Definition binop_e_interp b :=
match b with
| add_e => @add 32
| sub_e => @sub 32
| mul_e => @mul 32
| and_e => @int_and 32
| or_e => @int_or 32
| shl_e => fun a k : int 32 => @shl (Zabs_nat (u2Z k)) 32 a
| le_e => fun a b => if @le_n 32 a b then Z2u 32 1 else Z2u 32 0
| lt_e => fun a b => if @lt_n 32 a b then Z2u 32 1 else Z2u 32 0
| gt_e => fun a b => if @lt_n 32 b a then Z2u 32 1 else Z2u 32 0
| land_e => fun a b => if (u2Z a == Z0 ) || (u2Z b == Z0) then Z2u 32 0 else Z2u 32 1
| lor_e => fun a b => if (u2Z a == Z0) && (u2Z b == Z0) then Z2u 32 0 else Z2u 32 1
| eq_e => fun a b => if u2Z a == u2Z b then Z2u 32 1 else Z2u 32 0
| neq_e => fun a b => if u2Z a == u2Z b then Z2u 32 0 else Z2u 32 1
end.
Definition binop_e_interp8 b :=
match b with
| add_e => @add 8
| sub_e => @sub 8
| mul_e => @mul 8
| and_e => @int_and 8
| or_e => @int_or 8
| shl_e => fun a k : int 8 => @shl (Zabs_nat (u2Z k)) 8 a
| le_e => fun a b => if @le_n 8 a b then Z2u 8 1 else Z2u 8 0
| lt_e => fun a b => if @lt_n 8 a b then Z2u 8 1 else Z2u 8 0
| gt_e => fun a b => if @lt_n 8 b a then Z2u 8 1 else Z2u 8 0
| land_e => fun a b => if (u2Z a == Z0) || (u2Z b == Z0) then Z2u 8 0 else Z2u 8 1
| lor_e => fun a b => if (u2Z a == Z0) && (u2Z b == Z0) then Z2u 8 0 else Z2u 8 1
| eq_e => fun a b => if u2Z a == u2Z b then Z2u 8 1 else Z2u 8 0
| neq_e => fun a b => if u2Z a == u2Z b then Z2u 8 0 else Z2u 8 1
end.
Definition binopk_e_interp b :=
match b with
| mod2n_e => fun (a : int 32) (k : nat) => (@rem 32 _ (@rem k _ a))
end.
Definition binop_pe_interp b :=
match b with
| peq_e => fun (a b : int ptr_len) => if u2Z a == u2Z b then Z2u 32 1 else Z2u 32 0
end.
Inductive cast : Type := uchar_to_int.
Inductive exp : Type :=
| var_e of var
| cst32 of int 32
| cst8 of int 8
| cast_e of cast & exp
| bop_ne of binop_e & exp & exp
| bopk_ne of binopk_e & exp & nat
| ifte_e of exp & exp & exp
| fld of exp & string
| fld' of exp & string
| cst_pe : forall t : typ, wft t -> int ptr_len -> exp
| add_pe of exp & exp
| sub_pe of exp & exp
| bop_pe of exp & exp
| cst_se : forall tg l vs,
wft (styp tg l) -> length l = length vs ->
forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) vs) -> exp.
Implicit Arguments cst_pe [t].
Notation "'(c2i)' x" := (cast_e uchar_to_int x) (at level 58) : minC_expr_scope.
Notation "v 'CST_SE' Hv" := (cst_se _ _ v Hv (refl_equal _) (refl_equal _))
(at level 76, no associativity) : minC_expr_scope.
Notation "a '\+e' b" := (bop_ne add_e a b) (at level 60) : minC_expr_scope.
Notation "a '\-e' b" := (bop_ne sub_e a b) (at level 60) : minC_expr_scope.
Notation "a '\*e' b" := (bop_ne mul_e a b) (at level 59) : minC_expr_scope.
Notation "a '\&e' b" := (bop_ne and_e a b) (at level 60) : minC_expr_scope.
Notation "a '\|e' b" := (bop_ne or_e a b) (at level 60) : minC_expr_scope.
Notation "a '\<<e' b" := (bop_ne shl_e a b) (at level 60) : minC_expr_scope.
Notation "a '\%e' b" := (bopk_ne mod2n_e a b) (at level 60) : minC_expr_scope.
Notation "a '.\' b" := (fld a b) (at level 75) : minC_expr_scope.
Notation "a '.->' b" := (fld' a b) (at level 75) : minC_expr_scope.
Notation "a '\<=e' b" := (bop_ne le_e a b) (at level 60) : minC_expr_scope.
Notation "a '\<e' b" := (bop_ne lt_e a b) (at level 60) : minC_expr_scope.
Notation "a '\>e' b" := (bop_ne gt_e a b) (at level 60) : minC_expr_scope.
Notation "a '\&&e' b" := (bop_ne land_e a b) (at level 60) : minC_expr_scope.
Notation "a '\||e' b" := (bop_ne lor_e a b) (at level 60) : minC_expr_scope.
Notation "a '\=e' b" := (bop_ne eq_e a b) (at level 60) : minC_expr_scope.
Notation "a '\!=e' b" := (bop_ne neq_e a b) (at level 60) : minC_expr_scope.
Notation "a '\=pe' b" := (bop_pe a b) (at level 60) : minC_expr_scope.
sample expressions
Definition cst32_0 : exp := cst32 (Z2s 32 0).
Definition cst32_1 : exp := cst32 (Z2s 32 1).
Local Open Scope minC_expr_scope.
Fixpoint vars e :=
match e with
| var_e v => v :: nil
| cst32 i => nil
| cst8 c => nil
| cast_e c e' => vars e'
| bop_ne bo e1 e2 => vars e1 ++ vars e2
| bopk_ne bo e1 k => vars e1
| ifte_e e1 e2 e3 => vars e1 ++ vars e2 ++ vars e3
| fld e' f => vars e'
| fld' e' f => vars e'
| cst_pe _ wf_t i => nil
| add_pe e1 e2 => vars e1 ++ vars e2
| sub_pe e1 e2 => vars e1 ++ vars e2
| bop_pe e1 e2 => vars e1 ++ vars e2
| cst_se s ss_ts vs H Hlen Htypval => nil
end.
Definition cst32_1 : exp := cst32 (Z2s 32 1).
Local Open Scope minC_expr_scope.
Fixpoint vars e :=
match e with
| var_e v => v :: nil
| cst32 i => nil
| cst8 c => nil
| cast_e c e' => vars e'
| bop_ne bo e1 e2 => vars e1 ++ vars e2
| bopk_ne bo e1 k => vars e1
| ifte_e e1 e2 e3 => vars e1 ++ vars e2 ++ vars e3
| fld e' f => vars e'
| fld' e' f => vars e'
| cst_pe _ wf_t i => nil
| add_pe e1 e2 => vars e1 ++ vars e2
| sub_pe e1 e2 => vars e1 ++ vars e2
| bop_pe e1 e2 => vars e1 ++ vars e2
| cst_se s ss_ts vs H Hlen Htypval => nil
end.
typing environment
Definition tenv := list (var * typ).
Local Open Scope minC_types.
Fixpoint typ_of (c : ctxt) (env : tenv) e :=
match e with
| var_e v => assoc_get v env
| cst32 _ => Some (btyp sint32)
| cst8 _ => Some (btyp uchar)
| cast_e ca e' => match typ_of c env e' with
| Some t' => match ca with
| uchar_to_int => if t' =t= btyp uchar then
Some (btyp uint32)
else
None
end
| None => None
end
| bop_ne _ e1 e2 =>
match typ_of c env e1, typ_of c env e2 with
| Some (btyp uint32), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uchar), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uint32), Some (btyp uchar) => Some (btyp uint32)
| Some (btyp sint32), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp sint32), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uint32), Some (btyp sint32) => Some (btyp uint32)
| Some (btyp sint32), Some (btyp uchar) => Some (btyp sint32)
| Some (btyp uchar), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp uchar), Some (btyp uchar) => Some (btyp uchar)
| _, _ => None
end
| bopk_ne _ e1 k =>
match typ_of c env e1 with
| Some (btyp uint32) => Some (btyp uint32)
| Some (btyp sint32) => Some (btyp sint32)
| _ => None
end
| ifte_e e1 e2 e3 =>
match typ_of c env e1 with
| Some (btyp _) =>
match typ_of c env e2, typ_of c env e3 with
| Some (btyp uint32), Some (btyp _) => Some (btyp uint32)
| Some (btyp _), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp _), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp sint32), Some (btyp _) => Some (btyp sint32)
| Some (btyp _), Some (btyp _) => Some (btyp uchar)
| _, _ => None
end
| _ => None
end
| fld e' f =>
match typ_of c env e' with
| Some (styp _ ss_ts) => assoc_get f ss_ts
| _ => None
end
| fld' e' f =>
match typ_of c env e' with
| Some (ptyp (styp s ss_ts)) =>
match assoc_get f ss_ts with
| Some t' => Some (ptyp t')
| None => None
end
| Some (rtyp tg) =>
match assoc_get tg c with
| Some lst =>
match assoc_get f lst with
| Some t' => Some (ptyp t')
| None => None
end
| None => None
end
| _ => None
end
| cst_pe t _ _ => Some (ptyp t)
| add_pe e1 e2 =>
match typ_of c env e2 with
| Some (btyp sint32) =>
match typ_of c env e1 with
| Some (ptyp t) => Some (ptyp t)
| Some (rtyp tg) =>
match assoc_get tg c with
| Some lst => Some (ptyp (styp tg lst))
| None => None
end
| _ => None
end
| _ => None
end
| sub_pe e1 e2 =>
match typ_of c env e1 with
| Some (ptyp (btyp uchar)) =>
match typ_of c env e2 with
| Some (ptyp (btyp uchar)) => Some (btyp sint32)
| _ => None
end
| _ => None
end
| bop_pe e1 e2 =>
match typ_of c env e1 with
| Some (ptyp t) =>
match typ_of c env e2 with
| Some (ptyp t') => Some (btyp uint32)
| Some (rtyp t') => Some (btyp uint32)
| _ => None
end
| Some (rtyp t) =>
match typ_of c env e2 with
| Some (ptyp t') => Some (btyp uint32)
| Some (rtyp t') => Some (btyp uint32)
| _ => None
end
| _ => None
end
| cst_se s ss_ts vs H Hlen Htypval => Some (styp s ss_ts)
end.
Inductive typ_of_bop_ne_spec : typ -> typ -> typ -> Prop :=
| bop_ne_u32_u32 : typ_of_bop_ne_spec (btyp uint32) (btyp uint32) (btyp uint32)
| bop_ne_uchar_u32 : typ_of_bop_ne_spec (btyp uchar) (btyp uint32) (btyp uint32)
| bop_ne_u32_uchar : typ_of_bop_ne_spec (btyp uint32) (btyp uchar) (btyp uint32)
| bop_ne_s32_s32 : typ_of_bop_ne_spec (btyp sint32) (btyp sint32) (btyp sint32)
| bop_ne_s32_u32 : typ_of_bop_ne_spec (btyp sint32) (btyp uint32) (btyp uint32)
| bop_ne_u32_s32 : typ_of_bop_ne_spec (btyp uint32) (btyp sint32) (btyp uint32)
| bop_ne_s32_uchar : typ_of_bop_ne_spec (btyp sint32) (btyp uchar) (btyp sint32)
| bop_ne_uchar_s32 : typ_of_bop_ne_spec (btyp uchar) (btyp sint32) (btyp sint32)
| bop_ne_uchar_uchar : typ_of_bop_ne_spec (btyp uchar) (btyp uchar) (btyp uchar).
Inductive typ_of_bopk_ne_spec : typ -> typ -> Prop :=
| bopk_ne_u32 : typ_of_bopk_ne_spec (btyp uint32) (btyp uint32)
| bopk_ne_s32 : typ_of_bopk_ne_spec (btyp sint32) (btyp sint32).
Inductive typ_of_ifte_e_spec : typ -> typ -> typ -> Prop :=
| ifte_e_u32_x t : typ_of_ifte_e_spec (btyp uint32) (btyp t) (btyp uint32)
| ifte_e_x_u32 t : typ_of_ifte_e_spec (btyp t) (btyp uint32) (btyp uint32)
| ifte_e_s32_x t : t <> uint32 -> typ_of_ifte_e_spec (btyp sint32) (btyp t) (btyp sint32)
| ifte_e_x_s32 t : t <> uint32 -> typ_of_ifte_e_spec (btyp t) (btyp sint32) (btyp sint32)
| ifte_e_uchar : typ_of_ifte_e_spec (btyp uchar) (btyp uchar) (btyp uchar).
Inductive typ_of_bop_pe_spec : typ -> typ -> typ -> Prop :=
| bop_pe_pp t t' : typ_of_bop_pe_spec (ptyp t) (ptyp t') (btyp uint32)
| bop_pe_rp t t' : typ_of_bop_pe_spec (rtyp t) (ptyp t') (btyp uint32)
| bop_pe_pr t t' : typ_of_bop_pe_spec (ptyp t) (rtyp t') (btyp uint32)
| bop_pe_rr t t' : typ_of_bop_pe_spec (rtyp t) (rtyp t') (btyp uint32).
Inductive typ_of_spec (g : ctxt) (env : tenv) : exp -> typ -> Prop :=
| typ_of_var_e :
forall v t,
assoc_get v env = Some t ->
typ_of_spec g env (var_e v) t
| typ_of_cst32 :
forall x,
typ_of_spec g env (cst32 x) (btyp sint32)
| typ_of_cst8 :
forall x,
typ_of_spec g env (cst8 x) (btyp uchar)
| typ_of_cast_e : forall e, typ_of_spec g env e (btyp uchar) ->
typ_of_spec g env (cast_e uchar_to_int e) (btyp uint32)
| typ_of_bop_ne :
forall bop e1 e2 t1 t2 t,
typ_of_spec g env e1 t1 ->
typ_of_spec g env e2 t2 ->
typ_of_bop_ne_spec t1 t2 t ->
typ_of_spec g env (bop_ne bop e1 e2) t
| typ_of_bopk_ne bopk :
forall e1 k t1 t,
typ_of_spec g env e1 t1 ->
typ_of_bopk_ne_spec t1 t ->
typ_of_spec g env (bopk_ne bopk e1 k) t
| typ_of_ifte_e :
forall e1 e2 e3 t1 t2 t3 t,
typ_of_spec g env e1 (btyp t1) ->
typ_of_spec g env e2 t2 ->
typ_of_spec g env e3 t3 ->
typ_of_ifte_e_spec t2 t3 t ->
typ_of_spec g env (ifte_e e1 e2 e3) t
| typ_of_fld :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (styp tg ss_ts) ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld e1 f) t
| typ_of_fld'_ptyp :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (ptyp (styp tg ss_ts)) ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld' e1 f) (ptyp t)
| typ_of_fld'_rtyp :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (rtyp tg) ->
assoc_get tg g = Some ss_ts ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld' e1 f) (ptyp t)
| typ_of_cst_pe_t :
forall t wft_t p,
typ_of_spec g env (@cst_pe t wft_t p) (ptyp t)
| typ_of_add_pe_ptyp :
forall e1 e2 t,
typ_of_spec g env e1 (ptyp t) ->
typ_of_spec g env e2 (btyp sint32) ->
typ_of_spec g env (add_pe e1 e2) (ptyp t)
| typ_of_add_pe_rtyp :
forall e1 e2 tg lst,
typ_of_spec g env e1 (rtyp tg) ->
assoc_get tg g = Some lst ->
typ_of_spec g env e2 (btyp sint32) ->
typ_of_spec g env (add_pe e1 e2) (ptyp (styp tg lst))
| typ_of_sub_pe :
forall e1 e2,
typ_of_spec g env e1 (ptyp (btyp uchar)) ->
typ_of_spec g env e2 (ptyp (btyp uchar)) ->
typ_of_spec g env (sub_pe e1 e2) (btyp sint32)
| typ_of_bop_pe :
forall e1 e2 t1 t2 t,
typ_of_spec g env e1 t1 ->
typ_of_spec g env e2 t2 ->
typ_of_bop_pe_spec t1 t2 t ->
typ_of_spec g env (bop_pe e1 e2) t
| typ_of_cst_se :
forall s ss_ts vs H Hlen Htypval,
typ_of_spec g env (cst_se s ss_ts vs H Hlen Htypval) (styp s ss_ts).
Lemma typ_of_P : forall e g te t,
typ_of g te e = Some t <-> typ_of_spec g te e t.
Local Open Scope minC_types.
Local Open Scope minC_types.
Fixpoint typ_of (c : ctxt) (env : tenv) e :=
match e with
| var_e v => assoc_get v env
| cst32 _ => Some (btyp sint32)
| cst8 _ => Some (btyp uchar)
| cast_e ca e' => match typ_of c env e' with
| Some t' => match ca with
| uchar_to_int => if t' =t= btyp uchar then
Some (btyp uint32)
else
None
end
| None => None
end
| bop_ne _ e1 e2 =>
match typ_of c env e1, typ_of c env e2 with
| Some (btyp uint32), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uchar), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uint32), Some (btyp uchar) => Some (btyp uint32)
| Some (btyp sint32), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp sint32), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp uint32), Some (btyp sint32) => Some (btyp uint32)
| Some (btyp sint32), Some (btyp uchar) => Some (btyp sint32)
| Some (btyp uchar), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp uchar), Some (btyp uchar) => Some (btyp uchar)
| _, _ => None
end
| bopk_ne _ e1 k =>
match typ_of c env e1 with
| Some (btyp uint32) => Some (btyp uint32)
| Some (btyp sint32) => Some (btyp sint32)
| _ => None
end
| ifte_e e1 e2 e3 =>
match typ_of c env e1 with
| Some (btyp _) =>
match typ_of c env e2, typ_of c env e3 with
| Some (btyp uint32), Some (btyp _) => Some (btyp uint32)
| Some (btyp _), Some (btyp uint32) => Some (btyp uint32)
| Some (btyp _), Some (btyp sint32) => Some (btyp sint32)
| Some (btyp sint32), Some (btyp _) => Some (btyp sint32)
| Some (btyp _), Some (btyp _) => Some (btyp uchar)
| _, _ => None
end
| _ => None
end
| fld e' f =>
match typ_of c env e' with
| Some (styp _ ss_ts) => assoc_get f ss_ts
| _ => None
end
| fld' e' f =>
match typ_of c env e' with
| Some (ptyp (styp s ss_ts)) =>
match assoc_get f ss_ts with
| Some t' => Some (ptyp t')
| None => None
end
| Some (rtyp tg) =>
match assoc_get tg c with
| Some lst =>
match assoc_get f lst with
| Some t' => Some (ptyp t')
| None => None
end
| None => None
end
| _ => None
end
| cst_pe t _ _ => Some (ptyp t)
| add_pe e1 e2 =>
match typ_of c env e2 with
| Some (btyp sint32) =>
match typ_of c env e1 with
| Some (ptyp t) => Some (ptyp t)
| Some (rtyp tg) =>
match assoc_get tg c with
| Some lst => Some (ptyp (styp tg lst))
| None => None
end
| _ => None
end
| _ => None
end
| sub_pe e1 e2 =>
match typ_of c env e1 with
| Some (ptyp (btyp uchar)) =>
match typ_of c env e2 with
| Some (ptyp (btyp uchar)) => Some (btyp sint32)
| _ => None
end
| _ => None
end
| bop_pe e1 e2 =>
match typ_of c env e1 with
| Some (ptyp t) =>
match typ_of c env e2 with
| Some (ptyp t') => Some (btyp uint32)
| Some (rtyp t') => Some (btyp uint32)
| _ => None
end
| Some (rtyp t) =>
match typ_of c env e2 with
| Some (ptyp t') => Some (btyp uint32)
| Some (rtyp t') => Some (btyp uint32)
| _ => None
end
| _ => None
end
| cst_se s ss_ts vs H Hlen Htypval => Some (styp s ss_ts)
end.
Inductive typ_of_bop_ne_spec : typ -> typ -> typ -> Prop :=
| bop_ne_u32_u32 : typ_of_bop_ne_spec (btyp uint32) (btyp uint32) (btyp uint32)
| bop_ne_uchar_u32 : typ_of_bop_ne_spec (btyp uchar) (btyp uint32) (btyp uint32)
| bop_ne_u32_uchar : typ_of_bop_ne_spec (btyp uint32) (btyp uchar) (btyp uint32)
| bop_ne_s32_s32 : typ_of_bop_ne_spec (btyp sint32) (btyp sint32) (btyp sint32)
| bop_ne_s32_u32 : typ_of_bop_ne_spec (btyp sint32) (btyp uint32) (btyp uint32)
| bop_ne_u32_s32 : typ_of_bop_ne_spec (btyp uint32) (btyp sint32) (btyp uint32)
| bop_ne_s32_uchar : typ_of_bop_ne_spec (btyp sint32) (btyp uchar) (btyp sint32)
| bop_ne_uchar_s32 : typ_of_bop_ne_spec (btyp uchar) (btyp sint32) (btyp sint32)
| bop_ne_uchar_uchar : typ_of_bop_ne_spec (btyp uchar) (btyp uchar) (btyp uchar).
Inductive typ_of_bopk_ne_spec : typ -> typ -> Prop :=
| bopk_ne_u32 : typ_of_bopk_ne_spec (btyp uint32) (btyp uint32)
| bopk_ne_s32 : typ_of_bopk_ne_spec (btyp sint32) (btyp sint32).
Inductive typ_of_ifte_e_spec : typ -> typ -> typ -> Prop :=
| ifte_e_u32_x t : typ_of_ifte_e_spec (btyp uint32) (btyp t) (btyp uint32)
| ifte_e_x_u32 t : typ_of_ifte_e_spec (btyp t) (btyp uint32) (btyp uint32)
| ifte_e_s32_x t : t <> uint32 -> typ_of_ifte_e_spec (btyp sint32) (btyp t) (btyp sint32)
| ifte_e_x_s32 t : t <> uint32 -> typ_of_ifte_e_spec (btyp t) (btyp sint32) (btyp sint32)
| ifte_e_uchar : typ_of_ifte_e_spec (btyp uchar) (btyp uchar) (btyp uchar).
Inductive typ_of_bop_pe_spec : typ -> typ -> typ -> Prop :=
| bop_pe_pp t t' : typ_of_bop_pe_spec (ptyp t) (ptyp t') (btyp uint32)
| bop_pe_rp t t' : typ_of_bop_pe_spec (rtyp t) (ptyp t') (btyp uint32)
| bop_pe_pr t t' : typ_of_bop_pe_spec (ptyp t) (rtyp t') (btyp uint32)
| bop_pe_rr t t' : typ_of_bop_pe_spec (rtyp t) (rtyp t') (btyp uint32).
Inductive typ_of_spec (g : ctxt) (env : tenv) : exp -> typ -> Prop :=
| typ_of_var_e :
forall v t,
assoc_get v env = Some t ->
typ_of_spec g env (var_e v) t
| typ_of_cst32 :
forall x,
typ_of_spec g env (cst32 x) (btyp sint32)
| typ_of_cst8 :
forall x,
typ_of_spec g env (cst8 x) (btyp uchar)
| typ_of_cast_e : forall e, typ_of_spec g env e (btyp uchar) ->
typ_of_spec g env (cast_e uchar_to_int e) (btyp uint32)
| typ_of_bop_ne :
forall bop e1 e2 t1 t2 t,
typ_of_spec g env e1 t1 ->
typ_of_spec g env e2 t2 ->
typ_of_bop_ne_spec t1 t2 t ->
typ_of_spec g env (bop_ne bop e1 e2) t
| typ_of_bopk_ne bopk :
forall e1 k t1 t,
typ_of_spec g env e1 t1 ->
typ_of_bopk_ne_spec t1 t ->
typ_of_spec g env (bopk_ne bopk e1 k) t
| typ_of_ifte_e :
forall e1 e2 e3 t1 t2 t3 t,
typ_of_spec g env e1 (btyp t1) ->
typ_of_spec g env e2 t2 ->
typ_of_spec g env e3 t3 ->
typ_of_ifte_e_spec t2 t3 t ->
typ_of_spec g env (ifte_e e1 e2 e3) t
| typ_of_fld :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (styp tg ss_ts) ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld e1 f) t
| typ_of_fld'_ptyp :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (ptyp (styp tg ss_ts)) ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld' e1 f) (ptyp t)
| typ_of_fld'_rtyp :
forall e1 tg ss_ts f t,
typ_of_spec g env e1 (rtyp tg) ->
assoc_get tg g = Some ss_ts ->
assoc_get f ss_ts = Some t ->
typ_of_spec g env (fld' e1 f) (ptyp t)
| typ_of_cst_pe_t :
forall t wft_t p,
typ_of_spec g env (@cst_pe t wft_t p) (ptyp t)
| typ_of_add_pe_ptyp :
forall e1 e2 t,
typ_of_spec g env e1 (ptyp t) ->
typ_of_spec g env e2 (btyp sint32) ->
typ_of_spec g env (add_pe e1 e2) (ptyp t)
| typ_of_add_pe_rtyp :
forall e1 e2 tg lst,
typ_of_spec g env e1 (rtyp tg) ->
assoc_get tg g = Some lst ->
typ_of_spec g env e2 (btyp sint32) ->
typ_of_spec g env (add_pe e1 e2) (ptyp (styp tg lst))
| typ_of_sub_pe :
forall e1 e2,
typ_of_spec g env e1 (ptyp (btyp uchar)) ->
typ_of_spec g env e2 (ptyp (btyp uchar)) ->
typ_of_spec g env (sub_pe e1 e2) (btyp sint32)
| typ_of_bop_pe :
forall e1 e2 t1 t2 t,
typ_of_spec g env e1 t1 ->
typ_of_spec g env e2 t2 ->
typ_of_bop_pe_spec t1 t2 t ->
typ_of_spec g env (bop_pe e1 e2) t
| typ_of_cst_se :
forall s ss_ts vs H Hlen Htypval,
typ_of_spec g env (cst_se s ss_ts vs H Hlen Htypval) (styp s ss_ts).
Lemma typ_of_P : forall e g te t,
typ_of g te e = Some t <-> typ_of_spec g te e t.
Local Open Scope minC_types.
slight generalization of eqtm; for practical purposes
Definition oeqt g t1 t2 :=
match t1 with
| Some t1' => t1' =t g t= t2
| None => false
end.
Notation "t1 '=ot' g 'ot=' t2" := (oeqt g t1 t2) (at level 75) : minC_types.
Lemma eqtm_trans_oeqt : forall g (Hg : map_ctxt g) a t1 t2, a =ot g ot= t1 -> a =ot g ot= t2 -> t1 =t g t= t2.
Lemma oeqt_trans : forall g (Hg : map_ctxt g) a t1 t2,
a =ot g ot= t1 -> t1 =t g t= t2 -> a =ot g ot= t2.
Lemma typ_of_Some_In : forall e g te t, typ_of g te e = Some t ->
forall y, In y (vars e) -> In y (uzip1 te).
match t1 with
| Some t1' => t1' =t g t= t2
| None => false
end.
Notation "t1 '=ot' g 'ot=' t2" := (oeqt g t1 t2) (at level 75) : minC_types.
Lemma eqtm_trans_oeqt : forall g (Hg : map_ctxt g) a t1 t2, a =ot g ot= t1 -> a =ot g ot= t2 -> t1 =t g t= t2.
Lemma oeqt_trans : forall g (Hg : map_ctxt g) a t1 t2,
a =ot g ot= t1 -> t1 =t g t= t2 -> a =ot g ot= t2.
Lemma typ_of_Some_In : forall e g te t, typ_of g te e = Some t ->
forall y, In y (vars e) -> In y (uzip1 te).
embed a value into a constant of the expression language
Definition val2cst (g : ctxt) (t : typ) (v : value) : option exp :=
match t, v return option exp with
| btyp uint32, bval32 i => Some (cst32 i)
| btyp sint32, bval32 i => Some (cst32 i)
| btyp uchar, bval8 c => Some (cst8 c)
| ptyp t, pval p =>
match bool_dec (wft t) true with
| left wft_t => Some (cst_pe wft_t p)
| _ => None
end
| rtyp tg, pval p =>
match assoc_get tg g with
| None => None
| Some ss_ts =>
match bool_dec (wft (styp tg ss_ts)) true with
| left wft_t => Some (cst_pe wft_t p)
| _ => None
end
end
| styp s l, sval l' =>
match bool_dec (wft (styp s l)) true with
| left H =>
match eq_nat_dec (length l) (length l') with
| left H' =>
match bool_dec
(forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) l'))
true
with
| left H'' =>
match typ_val (styp s l) (sval l') with
| true => Some (cst_se s l l' H H' H'')
| false => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| btyp uint32, bval8 _ => None
| btyp sint32, bval8 _ => None
| btyp uint32, pval _ => None
| btyp sint32, pval _ => None
| btyp uint32, sval _ => None
| btyp sint32, sval _ => None
| btyp uchar, bval32 _ => None
| btyp uchar, pval _ => None
| btyp uchar, sval _ => None
| ptyp _, bval32 _ => None
| ptyp _, bval8 _ => None
| ptyp _, sval _ => None
| rtyp _, bval32 _ => None
| rtyp _, bval8 _ => None
| rtyp _, sval _ => None
| styp _ _, bval32 _ => None
| styp _ _, bval8 _ => None
| styp _ _, pval _ => None
end.
Lemma typ_val_val2cst : forall g (wf_g : wft_ctxt g) (complete_g : complete g) t (g_t : rcover g t) v,
wft t -> typ_val t v -> exists y, val2cst g t v = Some y.
Lemma val2cst_chars2val : forall t g (wf_g : wft_ctxt g) (complete_g : complete g) l,
wft t ->
rcover g t ->
sizeof t <= length l ->
exists e : exp, val2cst g t (fst (chars2val t l)) = Some e.
Fixpoint vals2csts (g : ctxt) (t : typ) (vs : list value) : option (list exp) :=
match vs with
| nil => Some nil
| hd :: tl => match vals2csts g t tl with
| None => None
| Some x => match val2cst g t hd with
| None => None
| Some y => Some (y :: x)
end
end
end.
Lemma vals2csts_prop : forall g lst,
vals2csts g (btyp uchar) (map (fun x => bval8 x) lst) =
Some (map (fun x => cst8 x) lst).
Lemma vals2csts_chars2vals_Some : forall n lst g (wf_g : wft_ctxt g) (complete_g : complete g)
(t : typ) (g_t : rcover g t ), wft t ->
length lst = n ->
forall q,
length lst = (S q) * sizeof t ->
exists es, vals2csts g t (chars2vals t lst) = Some es.
Lemma vals2csts_Some_len : forall l g t es, vals2csts g t l = Some es ->
length l = length es.
Local Open Scope machine_int_scope.
match t, v return option exp with
| btyp uint32, bval32 i => Some (cst32 i)
| btyp sint32, bval32 i => Some (cst32 i)
| btyp uchar, bval8 c => Some (cst8 c)
| ptyp t, pval p =>
match bool_dec (wft t) true with
| left wft_t => Some (cst_pe wft_t p)
| _ => None
end
| rtyp tg, pval p =>
match assoc_get tg g with
| None => None
| Some ss_ts =>
match bool_dec (wft (styp tg ss_ts)) true with
| left wft_t => Some (cst_pe wft_t p)
| _ => None
end
end
| styp s l, sval l' =>
match bool_dec (wft (styp s l)) true with
| left H =>
match eq_nat_dec (length l) (length l') with
| left H' =>
match bool_dec
(forallb (fun x => typ_val (fst x) (snd x)) (combine (uzip2 l) l'))
true
with
| left H'' =>
match typ_val (styp s l) (sval l') with
| true => Some (cst_se s l l' H H' H'')
| false => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| btyp uint32, bval8 _ => None
| btyp sint32, bval8 _ => None
| btyp uint32, pval _ => None
| btyp sint32, pval _ => None
| btyp uint32, sval _ => None
| btyp sint32, sval _ => None
| btyp uchar, bval32 _ => None
| btyp uchar, pval _ => None
| btyp uchar, sval _ => None
| ptyp _, bval32 _ => None
| ptyp _, bval8 _ => None
| ptyp _, sval _ => None
| rtyp _, bval32 _ => None
| rtyp _, bval8 _ => None
| rtyp _, sval _ => None
| styp _ _, bval32 _ => None
| styp _ _, bval8 _ => None
| styp _ _, pval _ => None
end.
Lemma typ_val_val2cst : forall g (wf_g : wft_ctxt g) (complete_g : complete g) t (g_t : rcover g t) v,
wft t -> typ_val t v -> exists y, val2cst g t v = Some y.
Lemma val2cst_chars2val : forall t g (wf_g : wft_ctxt g) (complete_g : complete g) l,
wft t ->
rcover g t ->
sizeof t <= length l ->
exists e : exp, val2cst g t (fst (chars2val t l)) = Some e.
Fixpoint vals2csts (g : ctxt) (t : typ) (vs : list value) : option (list exp) :=
match vs with
| nil => Some nil
| hd :: tl => match vals2csts g t tl with
| None => None
| Some x => match val2cst g t hd with
| None => None
| Some y => Some (y :: x)
end
end
end.
Lemma vals2csts_prop : forall g lst,
vals2csts g (btyp uchar) (map (fun x => bval8 x) lst) =
Some (map (fun x => cst8 x) lst).
Lemma vals2csts_chars2vals_Some : forall n lst g (wf_g : wft_ctxt g) (complete_g : complete g)
(t : typ) (g_t : rcover g t ), wft t ->
length lst = n ->
forall q,
length lst = (S q) * sizeof t ->
exists es, vals2csts g t (chars2vals t lst) = Some es.
Lemma vals2csts_Some_len : forall l g t es, vals2csts g t l = Some es ->
length l = length es.
Local Open Scope machine_int_scope.
store of values
store of typed values
Definition tstore := list (var * (value * typ)).
Definition tstore_vstore (s : tstore) : vstore := map (fun x => (fst x, fst (snd x))) s.
Definition tstore_tenv (s : tstore) : tenv := map (fun x => (fst x, snd (snd x))) s.
Lemma assoc_get_tstore : forall (s : tstore) x v t,
assoc_get x (tstore_tenv s) = Some t ->
assoc_get x (tstore_vstore s) = Some v ->
assoc_get x s = Some (v, t).
Lemma assoc_get_tstore_store_tenv : forall s a,
assoc_get a (tstore_vstore s) = None -> assoc_get a (tstore_tenv s) = None.
Lemma assoc_get_tstore_store : forall (s : tstore) x v t,
assoc_get x s = Some (v, t) -> assoc_get x (tstore_vstore s) = Some v.
Lemma assoc_get_tstore_tenv : forall (s : tstore) x v t,
assoc_get x s = Some (v, t) ->
assoc_get x (tstore_tenv s) = Some t.
Lemma In_tenv_inv : forall (s : tstore) x1 (x3 : typ),
In (x1, x3) (tstore_tenv s) -> exists x2, In (x1, (x2, x3)) s.
Definition to_tstore (l : vstore) (te : tenv) : tstore :=
combine (uzip1 l) (combine (uzip2 l) (uzip2 te)).
Definition tstore_vstore (s : tstore) : vstore := map (fun x => (fst x, fst (snd x))) s.
Definition tstore_tenv (s : tstore) : tenv := map (fun x => (fst x, snd (snd x))) s.
Lemma assoc_get_tstore : forall (s : tstore) x v t,
assoc_get x (tstore_tenv s) = Some t ->
assoc_get x (tstore_vstore s) = Some v ->
assoc_get x s = Some (v, t).
Lemma assoc_get_tstore_store_tenv : forall s a,
assoc_get a (tstore_vstore s) = None -> assoc_get a (tstore_tenv s) = None.
Lemma assoc_get_tstore_store : forall (s : tstore) x v t,
assoc_get x s = Some (v, t) -> assoc_get x (tstore_vstore s) = Some v.
Lemma assoc_get_tstore_tenv : forall (s : tstore) x v t,
assoc_get x s = Some (v, t) ->
assoc_get x (tstore_tenv s) = Some t.
Lemma In_tenv_inv : forall (s : tstore) x1 (x3 : typ),
In (x1, x3) (tstore_tenv s) -> exists x2, In (x1, (x2, x3)) s.
Definition to_tstore (l : vstore) (te : tenv) : tstore :=
combine (uzip1 l) (combine (uzip2 l) (uzip2 te)).
store is well-formed w.r.t. a type environment (generalization of typ_val)
Definition wf_tstore (s : tstore) := forall x v t,
assoc_get x s = Some (v, t) -> typ_val t v.
Definition empty_tstore : tstore := nil.
Definition tstore_get (v : var) (sto : tstore) : option value :=
assoc_get v (tstore_vstore sto).
Definition tstore_upd (x : var) (v : value) (sto : tstore) : tstore :=
to_tstore
(assoc_upd x v (tstore_vstore sto))
(tstore_tenv sto).
Lemma compose_l : forall (l : tstore),
combine (uzip1 (tstore_vstore l)) (combine (uzip2 (tstore_vstore l)) (uzip2 (tstore_tenv l))) = l.
Lemma tstore_upd_eq : forall x v w l, tstore_upd x v ((x, w) :: l) = (x, (v, snd w)) :: l.
Lemma tstore_get_upd_eq : forall (s : tstore) x v, In x (uzip1 s) ->
tstore_get x (tstore_upd x v s) = Some v.
Lemma tstore_get_upd_neq : forall s x y v, x <> y ->
tstore_get x (tstore_upd y v s) = tstore_get x s.
Lemma In_uzip1_assoc_upd_inv : forall s (x : var) (v : value) y, x <> y ->
In y (uzip1 (assoc_upd x v s)) -> In y (uzip1 s).
Lemma tstore_tenv_tstore_upd : forall s x v, tstore_tenv (tstore_upd x v s) = tstore_tenv s.
Lemma uzip1_store_upd : forall s x v, In x (uzip1 s) -> uzip1 (tstore_upd x v s) = uzip1 s.
Lemma assoc_get_tstore_upd_eq : forall s x v t,
assoc_get x (tstore_tenv s) = Some t ->
assoc_get x (tstore_upd x v s) = Some (v, t).
Lemma assoc_get_tstore_upd_neq : forall s x y v, x <> y ->
assoc_get x (tstore_upd y v s) = assoc_get x s.
assoc_get x s = Some (v, t) -> typ_val t v.
Definition empty_tstore : tstore := nil.
Definition tstore_get (v : var) (sto : tstore) : option value :=
assoc_get v (tstore_vstore sto).
Definition tstore_upd (x : var) (v : value) (sto : tstore) : tstore :=
to_tstore
(assoc_upd x v (tstore_vstore sto))
(tstore_tenv sto).
Lemma compose_l : forall (l : tstore),
combine (uzip1 (tstore_vstore l)) (combine (uzip2 (tstore_vstore l)) (uzip2 (tstore_tenv l))) = l.
Lemma tstore_upd_eq : forall x v w l, tstore_upd x v ((x, w) :: l) = (x, (v, snd w)) :: l.
Lemma tstore_get_upd_eq : forall (s : tstore) x v, In x (uzip1 s) ->
tstore_get x (tstore_upd x v s) = Some v.
Lemma tstore_get_upd_neq : forall s x y v, x <> y ->
tstore_get x (tstore_upd y v s) = tstore_get x s.
Lemma In_uzip1_assoc_upd_inv : forall s (x : var) (v : value) y, x <> y ->
In y (uzip1 (assoc_upd x v s)) -> In y (uzip1 s).
Lemma tstore_tenv_tstore_upd : forall s x v, tstore_tenv (tstore_upd x v s) = tstore_tenv s.
Lemma uzip1_store_upd : forall s x v, In x (uzip1 s) -> uzip1 (tstore_upd x v s) = uzip1 s.
Lemma assoc_get_tstore_upd_eq : forall s x v t,
assoc_get x (tstore_tenv s) = Some t ->
assoc_get x (tstore_upd x v s) = Some (v, t).
Lemma assoc_get_tstore_upd_neq : forall s x y v, x <> y ->
assoc_get x (tstore_upd y v s) = assoc_get x s.
typed store with context
Record store :=
{ _ctxt : ctxt ; Hctxt : map_ctxt _ctxt ; wf_ctxt : wft_ctxt _ctxt ;
_tstore : tstore }.
Ltac Cover_Rtyp :=
match goal with
| H : (assoc_get ?tg (_ctxt ?s) = Some ?l) |- cover (_ctxt ?s) (rtyp ?tg) =>
apply (cover_rtyp _ _ _ H)
end.
Ltac Cover :=
match goal with
| |- cover _ (ptyp ?t) => apply cover_ptyp; Cover
| |- cover _ (btyp _) => by rewrite /cover /stags /= /rcover /rtags /= /incl
| H : (assoc_get ?tg (_ctxt ?s) = Some ?l) |- cover (_ctxt ?s) (rtyp ?tg) =>
Cover_Rtyp
| |- cover _ _ => idtac
| |- _ => fail "not a (Cover _ _) goal!"
end.
Definition store_tenv (s : store) : tenv := tstore_tenv (_tstore s).
Definition typof (s : store) e := typ_of (_ctxt s) (store_tenv s) e.
Definition store_vstore (s : store) : vstore := tstore_vstore (_tstore s).
Lemma assoc_get_store_env_exists_tstore : forall s x t,
assoc_get x (store_tenv s) = Some t ->
exists v, assoc_get x (_tstore s) = Some (v, t).
Definition store_upd x (v : value) (s : store) :=
{| _ctxt := _ctxt s ; Hctxt := Hctxt s ; wf_ctxt := wf_ctxt s ;
_tstore := tstore_upd x v (_tstore s) |}.
Lemma store_tenv_store_upd : forall s x v,
store_tenv (store_upd x v s) = store_tenv s.
Lemma typof_upd : forall e s x v, typof (store_upd x v s) e = typof s e.
Lemma wf_tstore_tstore_upd : forall s x t v, wf_tstore s ->
assoc_get x (tstore_tenv s) = Some t ->
typ_val t v ->
wf_tstore (tstore_upd x v s) .
Notation " s '|t-' v -| t " :=
(assoc_get v (store_tenv s) = Some t) (at level 80) : minC_expr_scope.
Lemma store_upd_ctxt : forall s x v, _ctxt s = _ctxt (store_upd x v s).
Lemma In_tstore : forall s str t, s |t- str -| t -> In str (uzip1 (_tstore s)).
Notation " g |v- e -| t " :=
(assoc_get e (store_vstore g) = Some t) (at level 80) : minC_expr_scope.
Lemma store_upd_vstore_neq : forall s a b v t,
s |v- b -| t -> a != b -> store_upd a v s |v- b -| t.
Notation " g '|g-' t -| l " :=
(assoc_get (mkStag t) (_ctxt g) = Some l) (at level 80) : minC_expr_scope.
Lemma wf_tstore_store_store_upd : forall s x t v, wf_tstore (_tstore s) ->
s |t- x -| t -> typ_val t v ->
wf_tstore (_tstore (store_upd x v s)).
Definition store2ctxt_tenv (s : store) : ctxt * tenv :=
(_ctxt s, store_tenv s).
Lemma In_uzip1_store_tenv : forall s x,
In x (uzip1 (_tstore s)) -> In x (uzip1 (store_tenv s)).
Definition fields_typs_of (g : ctxt) (env : tenv) (e : exp) :=
match typ_of g env e with
| Some (styp s ss_ts) => Some ss_ts
| _ => None
end.
Definition deref (p : int ptr_len) f (ss_ts : list (string * typ))
: option value :=
match ifind f (uzip1 ss_ts) with
| Some idx =>
Some (pval (p [.+]
(Z2u ptr_len (Z_of_nat (iplus (map sizeof (firstn idx (uzip2 ss_ts))))))
))
| None => None
end.
Lemma deref_inv : forall p f lst v,deref p f lst = Some v ->
exists i, ifind f (uzip1 lst) = Some i /\
v = pval (p [.+]
Z2u ptr_len (Z_of_nat (iplus (map sizeof (firstn i (uzip2 lst)))))).
{ _ctxt : ctxt ; Hctxt : map_ctxt _ctxt ; wf_ctxt : wft_ctxt _ctxt ;
_tstore : tstore }.
Ltac Cover_Rtyp :=
match goal with
| H : (assoc_get ?tg (_ctxt ?s) = Some ?l) |- cover (_ctxt ?s) (rtyp ?tg) =>
apply (cover_rtyp _ _ _ H)
end.
Ltac Cover :=
match goal with
| |- cover _ (ptyp ?t) => apply cover_ptyp; Cover
| |- cover _ (btyp _) => by rewrite /cover /stags /= /rcover /rtags /= /incl
| H : (assoc_get ?tg (_ctxt ?s) = Some ?l) |- cover (_ctxt ?s) (rtyp ?tg) =>
Cover_Rtyp
| |- cover _ _ => idtac
| |- _ => fail "not a (Cover _ _) goal!"
end.
Definition store_tenv (s : store) : tenv := tstore_tenv (_tstore s).
Definition typof (s : store) e := typ_of (_ctxt s) (store_tenv s) e.
Definition store_vstore (s : store) : vstore := tstore_vstore (_tstore s).
Lemma assoc_get_store_env_exists_tstore : forall s x t,
assoc_get x (store_tenv s) = Some t ->
exists v, assoc_get x (_tstore s) = Some (v, t).
Definition store_upd x (v : value) (s : store) :=
{| _ctxt := _ctxt s ; Hctxt := Hctxt s ; wf_ctxt := wf_ctxt s ;
_tstore := tstore_upd x v (_tstore s) |}.
Lemma store_tenv_store_upd : forall s x v,
store_tenv (store_upd x v s) = store_tenv s.
Lemma typof_upd : forall e s x v, typof (store_upd x v s) e = typof s e.
Lemma wf_tstore_tstore_upd : forall s x t v, wf_tstore s ->
assoc_get x (tstore_tenv s) = Some t ->
typ_val t v ->
wf_tstore (tstore_upd x v s) .
Notation " s '|t-' v -| t " :=
(assoc_get v (store_tenv s) = Some t) (at level 80) : minC_expr_scope.
Lemma store_upd_ctxt : forall s x v, _ctxt s = _ctxt (store_upd x v s).
Lemma In_tstore : forall s str t, s |t- str -| t -> In str (uzip1 (_tstore s)).
Notation " g |v- e -| t " :=
(assoc_get e (store_vstore g) = Some t) (at level 80) : minC_expr_scope.
Lemma store_upd_vstore_neq : forall s a b v t,
s |v- b -| t -> a != b -> store_upd a v s |v- b -| t.
Notation " g '|g-' t -| l " :=
(assoc_get (mkStag t) (_ctxt g) = Some l) (at level 80) : minC_expr_scope.
Lemma wf_tstore_store_store_upd : forall s x t v, wf_tstore (_tstore s) ->
s |t- x -| t -> typ_val t v ->
wf_tstore (_tstore (store_upd x v s)).
Definition store2ctxt_tenv (s : store) : ctxt * tenv :=
(_ctxt s, store_tenv s).
Lemma In_uzip1_store_tenv : forall s x,
In x (uzip1 (_tstore s)) -> In x (uzip1 (store_tenv s)).
Definition fields_typs_of (g : ctxt) (env : tenv) (e : exp) :=
match typ_of g env e with
| Some (styp s ss_ts) => Some ss_ts
| _ => None
end.
Definition deref (p : int ptr_len) f (ss_ts : list (string * typ))
: option value :=
match ifind f (uzip1 ss_ts) with
| Some idx =>
Some (pval (p [.+]
(Z2u ptr_len (Z_of_nat (iplus (map sizeof (firstn idx (uzip2 ss_ts))))))
))
| None => None
end.
Lemma deref_inv : forall p f lst v,deref p f lst = Some v ->
exists i, ifind f (uzip1 lst) = Some i /\
v = pval (p [.+]
Z2u ptr_len (Z_of_nat (iplus (map sizeof (firstn i (uzip2 lst)))))).
NB: about pointer subtraction:
Below, sub_pe returns a signed integer. It would be more appropriate to
introduce a ptrdiff_t type for this purpose instead.
Reserved Notation "'[' e ']_' s" (at level 9).
Fixpoint eval (e : exp) (s : store) : option value :=
match e with
| var_e v => tstore_get v (_tstore s)
| cst32 i => Some (bval32 i)
| cst8 c => Some (bval8 c)
| cast_e uchat_to_int e' => match [ e' ]_ s with
| Some (bval8 uc) => Some (bval32 (zext 24 uc))
| N_ => None
end
| bop_ne bo e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (bval32 i1), Some (bval32 i2) =>
Some (bval32 (binop_e_interp bo i1 i2))
| Some (bval8 c1), Some (bval32 i2) =>
Some (bval32 (binop_e_interp bo (zext 24 c1) i2))
| Some (bval32 i1), Some (bval8 c2) =>
Some (bval32 (binop_e_interp bo i1 (zext 24 c2)))
| Some (bval8 c1), Some (bval8 c2) =>
Some (bval8 (binop_e_interp8 bo c1 c2))
| _, _ => None
end
| bopk_ne bo e1 k =>
match [ e1 ]_ s with
| Some (bval32 i1) => Some (bval32 (binopk_e_interp bo i1 k))
| _ => None
end
| ifte_e e1 e2 e3 =>
match [ e1 ]_ s with
| Some (bval32 i1) =>
match dec_int i1 zero32 with
| left _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval8 c3) => Some (bval8 c3)
| Some (bval32 _), Some (bval8 c3) => Some (bval32 (zext 24 c3))
| _, _ => None
end
| right _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 i2), Some (bval32 _) => Some (bval32 i2)
| Some (bval8 c2), Some (bval32 _) => Some (bval32 (zext 24 c2))
| Some (bval8 c2), Some (bval8 _) => Some (bval8 c2)
| Some (bval32 i2), Some (bval8 c3) => Some (bval32 i2)
| _, _ => None
end
end
| Some (bval8 c1) =>
match dec_int c1 (Z2u 8 0) with
| left _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval8 c3) => Some (bval8 c3)
| Some (bval32 _), Some (bval8 c3) => Some (bval32 (zext 24 c3))
| _, _ => None
end
| right _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 i2), Some (bval32 _) => Some (bval32 i2)
| Some (bval8 c2), Some (bval32 _) => Some (bval32 (zext 24 c2))
| Some (bval8 c2), Some (bval8 _) => Some (bval8 c2)
| Some (bval32 i2), Some (bval8 c3) => Some (bval32 i2)
| _, _ => None
end
end
| _ => None
end
| fld s_l f =>
match fields_typs_of s.(_ctxt) (store_tenv s) s_l with
| Some ss_ts =>
match assoc_get f ss_ts with
| Some _ =>
match [ s_l ]_ s with
| Some (sval l') =>
match ifind f (uzip1 (ss_ts)) with
| Some idx => ith idx l'
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
end
| fld' e' f =>
match [ e' ]_ s with
| Some (pval p) =>
match typof s e' with
| Some (ptyp (styp _ ss_ts)) => deref p f ss_ts
| Some (rtyp tg) =>
match assoc_get tg (_ctxt s) with
| Some lst => deref p f lst
| None => None
end
| _ => None
end
| _ => None
end
| cst_pe t_ Ht adr => Some (pval adr)
| add_pe e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (pval i1), Some (bval32 i2) =>
match typof s e2 with
| Some (btyp sint32) =>
match typof s e1 with
| Some (ptyp t) => Some (pval (scalez i1 (sizeof t) (s2Z i2)))
| Some (rtyp tg) =>
match assoc_get tg (_ctxt s) with
| Some lst => Some (pval (scalez i1 (sizeof (styp tg lst)) (s2Z i2)))
| None => None
end
| _ => None
end
| _ => None
end
| _, _ => None
end
| sub_pe e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (pval i1), Some (pval i2) =>
match typof s e1 with
| Some (ptyp (btyp uchar)) =>
match typof s e2 with
| Some (ptyp (btyp uchar)) =>
Some (bval32 (Z2s _ (s2Z (sub i1 i2))))
| _ => None
end
| _ => None
end
| _, _ => None
end
| bop_pe e1 e2 =>
match [ e1 ]_ s with
| Some (pval p1) =>
match [ e2 ]_ s with
| Some (pval p2) =>
match typof s e1 with
| Some (ptyp t) =>
match typof s e2 with
| Some (ptyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| Some (rtyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| _ => None
end
| Some (rtyp t) =>
match typof s e2 with
| Some (ptyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| Some (rtyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| cst_se s ss_ts vs H Hlen Hforall => Some (sval vs)
end
where "'[' e ']_' s" := (eval e s) : minC_expr_scope.
Inductive eval_bop_ne_spec bo : value -> value -> value -> Prop :=
| eval_bop_ne_int_int :
forall i1 i2,
eval_bop_ne_spec bo (bval32 i1) (bval32 i2)
(bval32 (binop_e_interp bo i1 i2))
| eval_bop_ne_char_int :
forall c1 i2,
eval_bop_ne_spec bo (bval8 c1) (bval32 i2)
(bval32 (binop_e_interp bo (zext 24 c1) i2))
| eval_bop_ne_int_char :
forall i1 c2,
eval_bop_ne_spec bo (bval32 i1) (bval8 c2)
(bval32 (binop_e_interp bo i1 (zext 24 c2)))
| eval_bop_ne_char_char :
forall c1 c2,
eval_bop_ne_spec bo (bval8 c1) (bval8 c2)
(bval8 (binop_e_interp8 bo c1 c2)).
Inductive eval_ifte_e_promotion_spec : value -> value -> value -> Prop :=
| eval_ifte_e_promotion_int_int :
forall i1 i2,
eval_ifte_e_promotion_spec (bval32 i1) (bval32 i2) (bval32 i1)
| eval_ifte_e_promotion_int_char :
forall i1 c2,
eval_ifte_e_promotion_spec (bval32 i1) (bval8 c2) (bval32 i1)
| eval_ifte_e_promotion_char_int :
forall c1 i2,
eval_ifte_e_promotion_spec (bval8 c1) (bval32 i2) (bval32 (zext 24 c1))
| eval_ifte_e_promotion_char_char :
forall c1 c2,
eval_ifte_e_promotion_spec (bval8 c1) (bval8 c2) (bval8 c1).
Inductive eval_true_spec : value -> Prop :=
| eval_true_spec_int :
forall i1,
i1 <> zero32 -> eval_true_spec (bval32 i1)
| eval_true_spec_char :
forall c1,
c1 <> (Z2u 8 0) -> eval_true_spec (bval8 c1).
Inductive eval_false_spec : value -> Prop :=
| eval_false_spec_int :
forall i1,
i1 = zero32 -> eval_false_spec (bval32 i1)
| eval_false_spec_char :
forall c1,
c1 = (Z2u 8 0) -> eval_false_spec (bval8 c1).
Inductive eval_spec (s : store) : exp -> value -> Prop :=
| eval_var_e :
forall v val,
tstore_get v (_tstore s) = Some val ->
eval_spec s (var_e v) val
| eval_cst32 :
forall i,
eval_spec s (cst32 i) (bval32 i)
| eval_cst8 :
forall i,
eval_spec s (cst8 i) (bval8 i)
| eval_cast_e : forall e i, eval_spec s e (bval8 i) ->
eval_spec s (cast_e uchar_to_int e) (bval32 (zext 24 i))
| eval_bop_ne :
forall bo e1 e2 val1 val2 val,
eval_spec s e1 val1 ->
eval_spec s e2 val2 ->
eval_bop_ne_spec bo val1 val2 val ->
eval_spec s (bop_ne bo e1 e2) val
| eval_bopk_ne :
forall bo e1 i1 k,
eval_spec s e1 (bval32 i1) ->
eval_spec s (bopk_ne bo e1 k) (bval32 (binopk_e_interp bo i1 k))
| eval_ifte_e_true :
forall e1 e2 e3 v1 v2 v3 val,
eval_spec s e1 v1 ->
eval_true_spec v1 ->
eval_spec s e2 v2 ->
eval_spec s e3 v3 ->
eval_ifte_e_promotion_spec v2 v3 val ->
eval_spec s (ifte_e e1 e2 e3) val
| eval_ifte_e_false :
forall e1 e2 e3 v1 v2 v3 val,
eval_spec s e1 v1 ->
eval_false_spec v1 ->
eval_spec s e2 v2 ->
eval_spec s e3 v3 ->
eval_ifte_e_promotion_spec v3 v2 val ->
eval_spec s (ifte_e e1 e2 e3) val
| eval_fld_spec :
forall s_l f ss_ts t l' idx val,
fields_typs_of s.(_ctxt) (store_tenv s) s_l = Some ss_ts ->
assoc_get f ss_ts = Some t ->
eval_spec s s_l (sval l') ->
ifind f (uzip1 ss_ts) = Some idx ->
ith idx l' = Some val ->
eval_spec s (fld s_l f) val
| eval_fld'_spec_ptyp :
forall e' f p tg ss_ts val,
eval_spec s e' (pval p) ->
typ_of_spec s.(_ctxt) (store_tenv s) e' (ptyp (styp tg ss_ts)) ->
deref p f ss_ts = Some val ->
eval_spec s (fld' e' f) val
| eval_fld'_spec_rtyp :
forall e' f p tg lst val,
eval_spec s e' (pval p) ->
typ_of_spec s.(_ctxt) (store_tenv s) e' (rtyp tg) ->
assoc_get tg (_ctxt s) = Some lst ->
deref p f lst = Some val ->
eval_spec s (fld' e' f) val
| eval_cst_pe :
forall t Ht adr,
eval_spec s (@cst_pe t Ht adr) (pval adr)
| eval_add_pe_ptyp :
forall e1 e2 i1 i2 t,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (bval32 i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (btyp sint32) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (ptyp t) ->
eval_spec s (add_pe e1 e2) (pval (scalez i1 (sizeof t) (s2Z i2)))
| eval_add_pe_rtyp :
forall e1 e2 i1 i2 tg lst,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (bval32 i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (btyp sint32) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (rtyp tg) ->
assoc_get tg (_ctxt s) = Some lst ->
eval_spec s (add_pe e1 e2) (pval (scalez i1 (sizeof (styp tg lst)) (s2Z i2)))
| eval_sub_pe :
forall e1 e2 i1 i2,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (pval i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (ptyp (btyp uchar)) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (ptyp (btyp uchar)) ->
eval_spec s (sub_pe e1 e2) (bval32 (Z2s _ (s2Z (sub i1 i2))))
| eval_bop_pe_eq :
forall e1 e2 p1 p2,
typ_of_spec s.(_ctxt) (store_tenv s) (bop_pe e1 e2) (btyp uint32) ->
eval_spec s e1 (pval p1) ->
eval_spec s e2 (pval p2) ->
u2Z p1 = u2Z p2 ->
eval_spec s (bop_pe e1 e2) (bval32 (Z2u 32 1))
| eval_bop_pe_ne :
forall e1 e2 p1 p2,
typ_of_spec s.(_ctxt) (store_tenv s) (bop_pe e1 e2) (btyp uint32) ->
eval_spec s e1 (pval p1) ->
eval_spec s e2 (pval p2) ->
u2Z p1 <> u2Z p2 ->
eval_spec s (bop_pe e1 e2) (bval32 (Z2u 32 0))
| eval_cst_se :
forall tg ss_ts vs H Hlen Hforall,
eval_spec s (cst_se tg ss_ts vs H Hlen Hforall) (sval vs).
Lemma evalP : forall e s v, [ e ]_ s = Some v <-> eval_spec s e v.
Lemma eval_upd : forall e s v x, ~ In x (vars e) ->
[ e ]_ (store_upd x v s) = [ e ]_ s.
Lemma typ_of_bop_ne_Some_inv : forall b g env e1 e2 t,
typ_of g env (bop_ne b e1 e2) = Some t ->
t = btyp uint32 \/ t = btyp sint32 \/ t = btyp uchar.
Lemma typ_of_fld_Some_inv : forall e g env f t,
typ_of g env (fld e f) = Some t ->
exists s, exists l, typ_of g env e = Some (styp s l).
Lemma typ_of_Some_wft : forall e (g : ctxt) (wf_g : wft_ctxt g) (env : tenv) t,
(forall x t, In x (vars e) -> assoc_get x env = Some t ->
wft t) ->
typ_of g env e = Some t -> wft t.
Lemma eval_typ_of_typ_val : forall e (s : store) v, wf_tstore (_tstore s) ->
[ e ]_ s = Some v -> exists t, typof s e = Some t /\ typ_val t v.
Lemma typof_eval : forall e s t, wf_tstore (_tstore s) -> typof s e = Some t ->
exists v, [ e ]_ s = Some v /\ typ_val t v.
Lemma val2cst_eval : forall (g : ctxt) (t : typ) (v : value) (e : exp) (s : store),
val2cst g t v = Some e -> [e ]_ s = Some v.
Lemma add_pe_0 : forall e s j, wf_tstore (_tstore s) ->
typof s e =ot _ctxt s ot= ptyp (btyp j) ->
[e ]_ s = [add_pe e (cst32 (Z2s 32 0)) ]_ s.
Local Open Scope zarith_ext_scope.
Local Open Scope Z_scope.
Lemma add_Z2s : forall l a b,
0 <= a ->
0 <= b ->
a + b < 2 ^^ l ->
Z2s (S l) a [.+] Z2s (S l) b = Z2s (S l) (a + b).
Lemma add_pe_assoc : forall a b c s vb vc, wf_tstore (_tstore s) ->
[ b ]_ s = Some (bval32 vb) ->
[ c ]_ s = Some (bval32 vc) ->
0 <= s2Z vb ->
0 <= s2Z vc ->
s2Z vb + s2Z vc < 2 ^^ 31 ->
typof s a =ot _ctxt s ot= ptyp (btyp uchar) ->
typof s b =ot _ctxt s ot= btyp sint32 ->
typof s c =ot _ctxt s ot= btyp sint32 ->
[add_pe (add_pe a b) c ]_s = [add_pe a (b \+e c) ]_s.
Local Close Scope Z_scope.
Lemma add_pe_reg : forall a b c s,
wf_tstore (_tstore s) ->
typof s b =ot _ctxt s ot= btyp sint32 ->
typof s c =ot _ctxt s ot= btyp sint32 ->
[ b ]_ s = [ c ]_s ->
[add_pe a b]_s = [add_pe a c]_s.
Lemma assoc_get_ptyp_styp_inv : forall str (s : store) tg flds,
assoc_get str (store_tenv s) =ot _ctxt s ot= ptyp (styp tg flds) ->
(exists flds',
eqt_list_ctxt (_ctxt s) flds flds' /\
assoc_get str (store_tenv s) = Some (ptyp (styp tg flds'))) \/
assoc_get str (store_tenv s) = Some (rtyp tg).
Lemma typ_of_add_pe : forall (g : ctxt) (wf_g : wft_ctxt g) (mp_g : map_ctxt g) (te : tenv) e t i,
typ_of g te e =ot g ot= ptyp t ->
typ_of g te (add_pe e (cst32 i)) =ot g ot= ptyp t.
Lemma oeqt_ptyp : forall g (Hg : map_ctxt g) a t1 t2,
a =ot g ot= ptyp t1 -> t1 =t g t= t2 -> a =ot g ot= ptyp t2.
Inductive bexp :=
| exp2bexp : exp -> bexp
| bneg : bexp -> bexp.
Fixpoint vars_b e :=
match e with
| exp2bexp e' => vars e'
| bneg e' => vars_b e'
end.
Fixpoint beval (e : bexp) (s : store) : bool :=
match e with
| exp2bexp e' =>
match [ e' ]_s with
| Some (bval32 v) => if u2Z v == Z0 then false else true
| Some (bval8 c) => if u2Z c == Z0 then false else true
| Some (pval p) => match u2Z p == Z0 with true => false | _ => true end
| Some (sval v) => false
| None => false
end
| bneg e => negb (beval e s)
end.
Notation "'[' e ']b_' s" := (beval e s) (at level 9) : minC_expr_scope.
Lemma evalb_upd : forall e s v x, ~ In x (vars_b e) ->
[ e ]b_ (store_upd x v s) = [ e ]b_ s.
Lemma neg_exp2bexp : forall s (wf_s : wf_tstore (_tstore s)) a b i,
s |t- a -| btyp i ->
~~ [exp2bexp (var_e a \!=e cst32 b)]b_s ->
[exp2bexp (var_e a \=e cst32 b)]b_s.
Lemma exp2bexp_neq : forall s (wf_s : wf_tstore (_tstore s)) v b,
s |t- v -| btyp sint32 ->
[exp2bexp (var_e v \=e cst32 b) ]b_ s ->
[var_e v]_ s = Some (bval32 b).
Ltac Store_upd :=
match goal with
| H : (wf_tstore (_tstore ?s)) , K : (?s |t- ?x -| ?t) |-
wf_tstore (_tstore (store_upd ?str ?v ?s)) =>
rewrite /=; apply wf_tstore_tstore_upd with t; [exact H | exact K| done]
| |- (store_upd ?str ?v ?s |v- ?str -| ?t ) =>
fail "store_upd_vstore_eq?"
| |- (store_upd ?str1 ?v ?s |v- ?str2 -| ?t ) =>
apply store_upd_vstore_neq
| |- context i [ _ctxt (store_upd ?str ?v ?s) ] =>
rewrite -store_upd_ctxt
| |- context i [ store_tenv (store_upd ?x ?v ?s) ] =>
rewrite store_tenv_store_upd
| |- context i [ typof (store_upd ?x ?v ?s) _ ] =>
rewrite typof_upd
| H : (?s |t- ?str -| ?t) |- context i [ [var_e ?str]_ (store_upd ?str ?v ?s) ] =>
simpl ( [var_e str]_ (store_upd str v s) ) ;
rewrite tstore_get_upd_eq; [idtac | by apply In_tstore with t]
| |- context i [ [var_e ?str1]_ (store_upd ?str2 ?v ?s) ] =>
rewrite (eval_upd (var_e str1) s v str2); [idtac | by apply/(In_inb_false eq_string_eq eq_string_refl)]
end.
Ltac typ_var :=
match goal with
| H : context [assoc_get ?i ?s = Some ?x ] |-
context [assoc_get ?i ?s] =>
rewrite (_ : assoc_get i s = Some x); last by tauto
end.
Ltac typ_var2 :=
match goal with
| H : context [assoc_get ?i ?s = Some ?x ],
K : context [assoc_get ?i ?s] |- _ =>
cutrewrite (assoc_get i s = Some x) in K; last by tauto
end.
Ltac Eqtm_inj :=
match goal with
| |- ptyp ?t1 =t ?c t= ptyp ?t2 => apply eqtm_ptyp
end.
Ltac Eqtm_Rtyp_Ptyp_Styp :=
match goal with
| |- rtyp ?tg =t ?c t= ptyp (styp ?tg ?l) =>
rewrite /eqtm /eqt /= eqxx;
split; first by done
end.
Ltac Eqtm :=
match goal with
| |- context i [ assoc_get ?x (store_tenv ?s) ] =>
typ_var; rewrite /=; apply eqtm_refl; Cover
| |- ?t =t _ctxt ?s t= ?t =>
apply eqtm_refl; Cover
| |- rtyp ?tg =t ?c t= ptyp (styp ?tg ?l) =>
Eqtm_Rtyp_Ptyp_Styp
end.
Ltac OEqtm :=
match goal with
| H : (?s |t- ?x -| ?t) |- typof ?s (var_e ?x) =ot _ctxt ?s ot= ?t =>
rewrite /typof /=; Eqtm
| |- typof ?s _ =ot _ctxt ?s ot= ?t =>
rewrite /typof /=; Eqtm
end.
Fixpoint eval (e : exp) (s : store) : option value :=
match e with
| var_e v => tstore_get v (_tstore s)
| cst32 i => Some (bval32 i)
| cst8 c => Some (bval8 c)
| cast_e uchat_to_int e' => match [ e' ]_ s with
| Some (bval8 uc) => Some (bval32 (zext 24 uc))
| N_ => None
end
| bop_ne bo e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (bval32 i1), Some (bval32 i2) =>
Some (bval32 (binop_e_interp bo i1 i2))
| Some (bval8 c1), Some (bval32 i2) =>
Some (bval32 (binop_e_interp bo (zext 24 c1) i2))
| Some (bval32 i1), Some (bval8 c2) =>
Some (bval32 (binop_e_interp bo i1 (zext 24 c2)))
| Some (bval8 c1), Some (bval8 c2) =>
Some (bval8 (binop_e_interp8 bo c1 c2))
| _, _ => None
end
| bopk_ne bo e1 k =>
match [ e1 ]_ s with
| Some (bval32 i1) => Some (bval32 (binopk_e_interp bo i1 k))
| _ => None
end
| ifte_e e1 e2 e3 =>
match [ e1 ]_ s with
| Some (bval32 i1) =>
match dec_int i1 zero32 with
| left _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval8 c3) => Some (bval8 c3)
| Some (bval32 _), Some (bval8 c3) => Some (bval32 (zext 24 c3))
| _, _ => None
end
| right _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 i2), Some (bval32 _) => Some (bval32 i2)
| Some (bval8 c2), Some (bval32 _) => Some (bval32 (zext 24 c2))
| Some (bval8 c2), Some (bval8 _) => Some (bval8 c2)
| Some (bval32 i2), Some (bval8 c3) => Some (bval32 i2)
| _, _ => None
end
end
| Some (bval8 c1) =>
match dec_int c1 (Z2u 8 0) with
| left _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval32 i3) => Some (bval32 i3)
| Some (bval8 _), Some (bval8 c3) => Some (bval8 c3)
| Some (bval32 _), Some (bval8 c3) => Some (bval32 (zext 24 c3))
| _, _ => None
end
| right _ =>
match [ e2 ]_ s, [ e3 ]_ s with
| Some (bval32 i2), Some (bval32 _) => Some (bval32 i2)
| Some (bval8 c2), Some (bval32 _) => Some (bval32 (zext 24 c2))
| Some (bval8 c2), Some (bval8 _) => Some (bval8 c2)
| Some (bval32 i2), Some (bval8 c3) => Some (bval32 i2)
| _, _ => None
end
end
| _ => None
end
| fld s_l f =>
match fields_typs_of s.(_ctxt) (store_tenv s) s_l with
| Some ss_ts =>
match assoc_get f ss_ts with
| Some _ =>
match [ s_l ]_ s with
| Some (sval l') =>
match ifind f (uzip1 (ss_ts)) with
| Some idx => ith idx l'
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
end
| fld' e' f =>
match [ e' ]_ s with
| Some (pval p) =>
match typof s e' with
| Some (ptyp (styp _ ss_ts)) => deref p f ss_ts
| Some (rtyp tg) =>
match assoc_get tg (_ctxt s) with
| Some lst => deref p f lst
| None => None
end
| _ => None
end
| _ => None
end
| cst_pe t_ Ht adr => Some (pval adr)
| add_pe e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (pval i1), Some (bval32 i2) =>
match typof s e2 with
| Some (btyp sint32) =>
match typof s e1 with
| Some (ptyp t) => Some (pval (scalez i1 (sizeof t) (s2Z i2)))
| Some (rtyp tg) =>
match assoc_get tg (_ctxt s) with
| Some lst => Some (pval (scalez i1 (sizeof (styp tg lst)) (s2Z i2)))
| None => None
end
| _ => None
end
| _ => None
end
| _, _ => None
end
| sub_pe e1 e2 =>
match [ e1 ]_ s, [ e2 ]_ s with
| Some (pval i1), Some (pval i2) =>
match typof s e1 with
| Some (ptyp (btyp uchar)) =>
match typof s e2 with
| Some (ptyp (btyp uchar)) =>
Some (bval32 (Z2s _ (s2Z (sub i1 i2))))
| _ => None
end
| _ => None
end
| _, _ => None
end
| bop_pe e1 e2 =>
match [ e1 ]_ s with
| Some (pval p1) =>
match [ e2 ]_ s with
| Some (pval p2) =>
match typof s e1 with
| Some (ptyp t) =>
match typof s e2 with
| Some (ptyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| Some (rtyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| _ => None
end
| Some (rtyp t) =>
match typof s e2 with
| Some (ptyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| Some (rtyp t') =>
if u2Z p1 == u2Z p2 then Some (bval32 (Z2u 32 1)) else Some (bval32 (Z2u 32 0))
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| cst_se s ss_ts vs H Hlen Hforall => Some (sval vs)
end
where "'[' e ']_' s" := (eval e s) : minC_expr_scope.
Inductive eval_bop_ne_spec bo : value -> value -> value -> Prop :=
| eval_bop_ne_int_int :
forall i1 i2,
eval_bop_ne_spec bo (bval32 i1) (bval32 i2)
(bval32 (binop_e_interp bo i1 i2))
| eval_bop_ne_char_int :
forall c1 i2,
eval_bop_ne_spec bo (bval8 c1) (bval32 i2)
(bval32 (binop_e_interp bo (zext 24 c1) i2))
| eval_bop_ne_int_char :
forall i1 c2,
eval_bop_ne_spec bo (bval32 i1) (bval8 c2)
(bval32 (binop_e_interp bo i1 (zext 24 c2)))
| eval_bop_ne_char_char :
forall c1 c2,
eval_bop_ne_spec bo (bval8 c1) (bval8 c2)
(bval8 (binop_e_interp8 bo c1 c2)).
Inductive eval_ifte_e_promotion_spec : value -> value -> value -> Prop :=
| eval_ifte_e_promotion_int_int :
forall i1 i2,
eval_ifte_e_promotion_spec (bval32 i1) (bval32 i2) (bval32 i1)
| eval_ifte_e_promotion_int_char :
forall i1 c2,
eval_ifte_e_promotion_spec (bval32 i1) (bval8 c2) (bval32 i1)
| eval_ifte_e_promotion_char_int :
forall c1 i2,
eval_ifte_e_promotion_spec (bval8 c1) (bval32 i2) (bval32 (zext 24 c1))
| eval_ifte_e_promotion_char_char :
forall c1 c2,
eval_ifte_e_promotion_spec (bval8 c1) (bval8 c2) (bval8 c1).
Inductive eval_true_spec : value -> Prop :=
| eval_true_spec_int :
forall i1,
i1 <> zero32 -> eval_true_spec (bval32 i1)
| eval_true_spec_char :
forall c1,
c1 <> (Z2u 8 0) -> eval_true_spec (bval8 c1).
Inductive eval_false_spec : value -> Prop :=
| eval_false_spec_int :
forall i1,
i1 = zero32 -> eval_false_spec (bval32 i1)
| eval_false_spec_char :
forall c1,
c1 = (Z2u 8 0) -> eval_false_spec (bval8 c1).
Inductive eval_spec (s : store) : exp -> value -> Prop :=
| eval_var_e :
forall v val,
tstore_get v (_tstore s) = Some val ->
eval_spec s (var_e v) val
| eval_cst32 :
forall i,
eval_spec s (cst32 i) (bval32 i)
| eval_cst8 :
forall i,
eval_spec s (cst8 i) (bval8 i)
| eval_cast_e : forall e i, eval_spec s e (bval8 i) ->
eval_spec s (cast_e uchar_to_int e) (bval32 (zext 24 i))
| eval_bop_ne :
forall bo e1 e2 val1 val2 val,
eval_spec s e1 val1 ->
eval_spec s e2 val2 ->
eval_bop_ne_spec bo val1 val2 val ->
eval_spec s (bop_ne bo e1 e2) val
| eval_bopk_ne :
forall bo e1 i1 k,
eval_spec s e1 (bval32 i1) ->
eval_spec s (bopk_ne bo e1 k) (bval32 (binopk_e_interp bo i1 k))
| eval_ifte_e_true :
forall e1 e2 e3 v1 v2 v3 val,
eval_spec s e1 v1 ->
eval_true_spec v1 ->
eval_spec s e2 v2 ->
eval_spec s e3 v3 ->
eval_ifte_e_promotion_spec v2 v3 val ->
eval_spec s (ifte_e e1 e2 e3) val
| eval_ifte_e_false :
forall e1 e2 e3 v1 v2 v3 val,
eval_spec s e1 v1 ->
eval_false_spec v1 ->
eval_spec s e2 v2 ->
eval_spec s e3 v3 ->
eval_ifte_e_promotion_spec v3 v2 val ->
eval_spec s (ifte_e e1 e2 e3) val
| eval_fld_spec :
forall s_l f ss_ts t l' idx val,
fields_typs_of s.(_ctxt) (store_tenv s) s_l = Some ss_ts ->
assoc_get f ss_ts = Some t ->
eval_spec s s_l (sval l') ->
ifind f (uzip1 ss_ts) = Some idx ->
ith idx l' = Some val ->
eval_spec s (fld s_l f) val
| eval_fld'_spec_ptyp :
forall e' f p tg ss_ts val,
eval_spec s e' (pval p) ->
typ_of_spec s.(_ctxt) (store_tenv s) e' (ptyp (styp tg ss_ts)) ->
deref p f ss_ts = Some val ->
eval_spec s (fld' e' f) val
| eval_fld'_spec_rtyp :
forall e' f p tg lst val,
eval_spec s e' (pval p) ->
typ_of_spec s.(_ctxt) (store_tenv s) e' (rtyp tg) ->
assoc_get tg (_ctxt s) = Some lst ->
deref p f lst = Some val ->
eval_spec s (fld' e' f) val
| eval_cst_pe :
forall t Ht adr,
eval_spec s (@cst_pe t Ht adr) (pval adr)
| eval_add_pe_ptyp :
forall e1 e2 i1 i2 t,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (bval32 i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (btyp sint32) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (ptyp t) ->
eval_spec s (add_pe e1 e2) (pval (scalez i1 (sizeof t) (s2Z i2)))
| eval_add_pe_rtyp :
forall e1 e2 i1 i2 tg lst,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (bval32 i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (btyp sint32) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (rtyp tg) ->
assoc_get tg (_ctxt s) = Some lst ->
eval_spec s (add_pe e1 e2) (pval (scalez i1 (sizeof (styp tg lst)) (s2Z i2)))
| eval_sub_pe :
forall e1 e2 i1 i2,
eval_spec s e1 (pval i1) ->
eval_spec s e2 (pval i2) ->
typ_of_spec s.(_ctxt) (store_tenv s) e1 (ptyp (btyp uchar)) ->
typ_of_spec s.(_ctxt) (store_tenv s) e2 (ptyp (btyp uchar)) ->
eval_spec s (sub_pe e1 e2) (bval32 (Z2s _ (s2Z (sub i1 i2))))
| eval_bop_pe_eq :
forall e1 e2 p1 p2,
typ_of_spec s.(_ctxt) (store_tenv s) (bop_pe e1 e2) (btyp uint32) ->
eval_spec s e1 (pval p1) ->
eval_spec s e2 (pval p2) ->
u2Z p1 = u2Z p2 ->
eval_spec s (bop_pe e1 e2) (bval32 (Z2u 32 1))
| eval_bop_pe_ne :
forall e1 e2 p1 p2,
typ_of_spec s.(_ctxt) (store_tenv s) (bop_pe e1 e2) (btyp uint32) ->
eval_spec s e1 (pval p1) ->
eval_spec s e2 (pval p2) ->
u2Z p1 <> u2Z p2 ->
eval_spec s (bop_pe e1 e2) (bval32 (Z2u 32 0))
| eval_cst_se :
forall tg ss_ts vs H Hlen Hforall,
eval_spec s (cst_se tg ss_ts vs H Hlen Hforall) (sval vs).
Lemma evalP : forall e s v, [ e ]_ s = Some v <-> eval_spec s e v.
Lemma eval_upd : forall e s v x, ~ In x (vars e) ->
[ e ]_ (store_upd x v s) = [ e ]_ s.
Lemma typ_of_bop_ne_Some_inv : forall b g env e1 e2 t,
typ_of g env (bop_ne b e1 e2) = Some t ->
t = btyp uint32 \/ t = btyp sint32 \/ t = btyp uchar.
Lemma typ_of_fld_Some_inv : forall e g env f t,
typ_of g env (fld e f) = Some t ->
exists s, exists l, typ_of g env e = Some (styp s l).
Lemma typ_of_Some_wft : forall e (g : ctxt) (wf_g : wft_ctxt g) (env : tenv) t,
(forall x t, In x (vars e) -> assoc_get x env = Some t ->
wft t) ->
typ_of g env e = Some t -> wft t.
Lemma eval_typ_of_typ_val : forall e (s : store) v, wf_tstore (_tstore s) ->
[ e ]_ s = Some v -> exists t, typof s e = Some t /\ typ_val t v.
Lemma typof_eval : forall e s t, wf_tstore (_tstore s) -> typof s e = Some t ->
exists v, [ e ]_ s = Some v /\ typ_val t v.
Lemma val2cst_eval : forall (g : ctxt) (t : typ) (v : value) (e : exp) (s : store),
val2cst g t v = Some e -> [e ]_ s = Some v.
Lemma add_pe_0 : forall e s j, wf_tstore (_tstore s) ->
typof s e =ot _ctxt s ot= ptyp (btyp j) ->
[e ]_ s = [add_pe e (cst32 (Z2s 32 0)) ]_ s.
Local Open Scope zarith_ext_scope.
Local Open Scope Z_scope.
Lemma add_Z2s : forall l a b,
0 <= a ->
0 <= b ->
a + b < 2 ^^ l ->
Z2s (S l) a [.+] Z2s (S l) b = Z2s (S l) (a + b).
Lemma add_pe_assoc : forall a b c s vb vc, wf_tstore (_tstore s) ->
[ b ]_ s = Some (bval32 vb) ->
[ c ]_ s = Some (bval32 vc) ->
0 <= s2Z vb ->
0 <= s2Z vc ->
s2Z vb + s2Z vc < 2 ^^ 31 ->
typof s a =ot _ctxt s ot= ptyp (btyp uchar) ->
typof s b =ot _ctxt s ot= btyp sint32 ->
typof s c =ot _ctxt s ot= btyp sint32 ->
[add_pe (add_pe a b) c ]_s = [add_pe a (b \+e c) ]_s.
Local Close Scope Z_scope.
Lemma add_pe_reg : forall a b c s,
wf_tstore (_tstore s) ->
typof s b =ot _ctxt s ot= btyp sint32 ->
typof s c =ot _ctxt s ot= btyp sint32 ->
[ b ]_ s = [ c ]_s ->
[add_pe a b]_s = [add_pe a c]_s.
Lemma assoc_get_ptyp_styp_inv : forall str (s : store) tg flds,
assoc_get str (store_tenv s) =ot _ctxt s ot= ptyp (styp tg flds) ->
(exists flds',
eqt_list_ctxt (_ctxt s) flds flds' /\
assoc_get str (store_tenv s) = Some (ptyp (styp tg flds'))) \/
assoc_get str (store_tenv s) = Some (rtyp tg).
Lemma typ_of_add_pe : forall (g : ctxt) (wf_g : wft_ctxt g) (mp_g : map_ctxt g) (te : tenv) e t i,
typ_of g te e =ot g ot= ptyp t ->
typ_of g te (add_pe e (cst32 i)) =ot g ot= ptyp t.
Lemma oeqt_ptyp : forall g (Hg : map_ctxt g) a t1 t2,
a =ot g ot= ptyp t1 -> t1 =t g t= t2 -> a =ot g ot= ptyp t2.
Inductive bexp :=
| exp2bexp : exp -> bexp
| bneg : bexp -> bexp.
Fixpoint vars_b e :=
match e with
| exp2bexp e' => vars e'
| bneg e' => vars_b e'
end.
Fixpoint beval (e : bexp) (s : store) : bool :=
match e with
| exp2bexp e' =>
match [ e' ]_s with
| Some (bval32 v) => if u2Z v == Z0 then false else true
| Some (bval8 c) => if u2Z c == Z0 then false else true
| Some (pval p) => match u2Z p == Z0 with true => false | _ => true end
| Some (sval v) => false
| None => false
end
| bneg e => negb (beval e s)
end.
Notation "'[' e ']b_' s" := (beval e s) (at level 9) : minC_expr_scope.
Lemma evalb_upd : forall e s v x, ~ In x (vars_b e) ->
[ e ]b_ (store_upd x v s) = [ e ]b_ s.
Lemma neg_exp2bexp : forall s (wf_s : wf_tstore (_tstore s)) a b i,
s |t- a -| btyp i ->
~~ [exp2bexp (var_e a \!=e cst32 b)]b_s ->
[exp2bexp (var_e a \=e cst32 b)]b_s.
Lemma exp2bexp_neq : forall s (wf_s : wf_tstore (_tstore s)) v b,
s |t- v -| btyp sint32 ->
[exp2bexp (var_e v \=e cst32 b) ]b_ s ->
[var_e v]_ s = Some (bval32 b).
Ltac Store_upd :=
match goal with
| H : (wf_tstore (_tstore ?s)) , K : (?s |t- ?x -| ?t) |-
wf_tstore (_tstore (store_upd ?str ?v ?s)) =>
rewrite /=; apply wf_tstore_tstore_upd with t; [exact H | exact K| done]
| |- (store_upd ?str ?v ?s |v- ?str -| ?t ) =>
fail "store_upd_vstore_eq?"
| |- (store_upd ?str1 ?v ?s |v- ?str2 -| ?t ) =>
apply store_upd_vstore_neq
| |- context i [ _ctxt (store_upd ?str ?v ?s) ] =>
rewrite -store_upd_ctxt
| |- context i [ store_tenv (store_upd ?x ?v ?s) ] =>
rewrite store_tenv_store_upd
| |- context i [ typof (store_upd ?x ?v ?s) _ ] =>
rewrite typof_upd
| H : (?s |t- ?str -| ?t) |- context i [ [var_e ?str]_ (store_upd ?str ?v ?s) ] =>
simpl ( [var_e str]_ (store_upd str v s) ) ;
rewrite tstore_get_upd_eq; [idtac | by apply In_tstore with t]
| |- context i [ [var_e ?str1]_ (store_upd ?str2 ?v ?s) ] =>
rewrite (eval_upd (var_e str1) s v str2); [idtac | by apply/(In_inb_false eq_string_eq eq_string_refl)]
end.
Ltac typ_var :=
match goal with
| H : context [assoc_get ?i ?s = Some ?x ] |-
context [assoc_get ?i ?s] =>
rewrite (_ : assoc_get i s = Some x); last by tauto
end.
Ltac typ_var2 :=
match goal with
| H : context [assoc_get ?i ?s = Some ?x ],
K : context [assoc_get ?i ?s] |- _ =>
cutrewrite (assoc_get i s = Some x) in K; last by tauto
end.
Ltac Eqtm_inj :=
match goal with
| |- ptyp ?t1 =t ?c t= ptyp ?t2 => apply eqtm_ptyp
end.
Ltac Eqtm_Rtyp_Ptyp_Styp :=
match goal with
| |- rtyp ?tg =t ?c t= ptyp (styp ?tg ?l) =>
rewrite /eqtm /eqt /= eqxx;
split; first by done
end.
Ltac Eqtm :=
match goal with
| |- context i [ assoc_get ?x (store_tenv ?s) ] =>
typ_var; rewrite /=; apply eqtm_refl; Cover
| |- ?t =t _ctxt ?s t= ?t =>
apply eqtm_refl; Cover
| |- rtyp ?tg =t ?c t= ptyp (styp ?tg ?l) =>
Eqtm_Rtyp_Ptyp_Styp
end.
Ltac OEqtm :=
match goal with
| H : (?s |t- ?x -| ?t) |- typof ?s (var_e ?x) =ot _ctxt ?s ot= ?t =>
rewrite /typof /=; Eqtm
| |- typof ?s _ =ot _ctxt ?s ot= ?t =>
rewrite /typof /=; Eqtm
end.