| The usual suspects in type systems describing heap-allocated values |
Require Import Arith ArithUtil Bool Bvector Eqdep.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Vector.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Monad.
Require Import Asm.Util.Tactics.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.AbsInt.WeakUpdateTypes.
Require Import ProofOS.AbsInt.WeakDriver.
Require Import ProofOS.AbsInt.Sal.
Set Implicit Arguments.
Definition var := nat.
Inductive memoryTy : Set :=
| Constant : int32 -> memoryTy
| Product : productTy -> memoryTy
| Sum : memoryTy -> memoryTy -> memoryTy
| Var : var -> memoryTy
| Recursive : var -> memoryTy -> memoryTy
with productTy : Set :=
| PT_Nil
| PT_Cons : memoryTy -> productTy -> productTy.
Parameter print_memoryTy : memoryTy -> unit.
Fixpoint subst (x : var) (t b : memoryTy) {struct b} : memoryTy :=
match b with
| Constant _ => b
| Product ts => Product (substProduct x t ts)
| Sum b1 b2 => Sum (subst x t b1) (subst x t b2)
| Var x' =>
if eq_nat_dec x x'
then t
else b
| Recursive x' b =>
if eq_nat_dec x x'
then b
else Recursive x' (subst x t b)
end
with substProduct (x : var) (t : memoryTy) (ts : productTy) {struct ts} : productTy :=
match ts with
| PT_Nil => ts
| PT_Cons b ts => PT_Cons (subst x t b) (substProduct x t ts)
end.
Inductive hasMemoryTy : (int32 -> option memoryTy) -> int32 -> memoryTy -> Prop :=
| HT_Constant : forall ctx v,
hasMemoryTy ctx v (Constant v)
| HT_Unit : forall ctx v,
hasMemoryTy ctx v (Product PT_Nil)
| HT_Product : forall ctx v t ts,
ctx v = Some t
-> hasMemoryTy ctx (binc4 v) (Product ts)
-> hasMemoryTy ctx v (Product (PT_Cons t ts))
| HT_Suml : forall ctx v t1 t2,
hasMemoryTy ctx v
(Product (PT_Cons (Constant bzero32)
(PT_Cons t1 PT_Nil)))
-> hasMemoryTy ctx v (Sum t1 t2)
| HT_Sumr : forall ctx v t1 t2,
hasMemoryTy ctx v
(Product (PT_Cons (Constant bone32)
(PT_Cons t2 PT_Nil)))
-> hasMemoryTy ctx v (Sum t1 t2)
| HT_Recursive : forall ctx x t v,
hasMemoryTy ctx v (subst x (Recursive x t) t)
-> hasMemoryTy ctx v (Recursive x t).
Module MemoryTySys <: WEAK_UPDATE_TYPE_SYSTEM.
Definition ty := memoryTy.
Definition print_ty := print_memoryTy.
Definition hasTy := hasMemoryTy.
Hint Unfold hasTy.
Hint Constructors hasMemoryTy.
Definition tyTop := Product PT_Nil.
Definition tyTopSound := HT_Unit.
Definition tyConst := Constant.
Definition tyConstSound1 := HT_Constant.
Theorem tyConstSound2 : forall ctx v1 v2, hasTy ctx v1 (tyConst v2) -> v1 = v2.
Definition isTyConst : forall (t : ty), sig_option (fun n => t = tyConst n).
Fixpoint ty_eq_dec' (a b : ty) {struct b} : bool :=
match (a, b) with
| (Constant k1, Constant k2) => sum_to_bool (int32_eq_dec k1 k2)
| (Product ts1, Product ts2) => product_eq_dec' ts1 ts2
| (Sum t1 u1, Sum t2 u2) => ty_eq_dec' t1 t2 && ty_eq_dec' u1 u2
| (Recursive t1 u1, Recursive t2 u2) => sum_to_bool (eq_nat_dec t1 t2) && ty_eq_dec' u1 u2
| (Var x1, Var x2) => sum_to_bool (eq_nat_dec x1 x2)
| _ => false
end
with product_eq_dec' (a b : productTy) {struct b} : bool :=
match (a, b) with
| (PT_Nil, PT_Nil) => true
| (PT_Cons t1 ts1, PT_Cons t2 ts2) =>
ty_eq_dec' t1 t2 && product_eq_dec' ts1 ts2
| _ => false
end.
Scheme ty_ind := Induction for memoryTy Sort Prop
with productTy_ind := Induction for productTy Sort Prop.
Lemma and_true : forall b1 b2,
b1 && b2 = true -> b1 = true /\ b2 = true.
Lemma and_false : forall b1 b2,
b1 && b2 = false -> b1 = false \/ b2 = false.
Lemma ty_eq_dec'_sound1 : forall (b a : ty),
ty_eq_dec' a b = true
-> a = b.
Lemma ty_eq_dec'_sound2 : forall (b a : ty),
ty_eq_dec' a b = false
-> a <> b.
Definition ty_eq_dec : forall (a b : ty), {a = b} + {a <> b}.
Fixpoint subTy' (t1 t2 : ty) {struct t1} : bool :=
match (t1, t2) with
| (_, Product PT_Nil) => true
| (Product ts1, Product ts2) => subProduct' ts1 ts2
| (Sum t1 u1, Sum t2 u2) => ty_eq_dec' t1 t2 && ty_eq_dec' u1 u2
| (Product (PT_Cons (Constant n) (PT_Cons t PT_Nil)), Sum t1 t2) =>
(sum_to_bool (int32_eq_dec n bzero32)
&& ty_eq_dec' t t1)
|| (sum_to_bool (int32_eq_dec n bone32)
&& ty_eq_dec' t t2)
| (Constant n1, Constant n2) =>
if int32_eq_dec n1 n2
then true
else false
| (Var x1, Var x2) =>
if eq_nat_dec x1 x2
then true
else false
| (Recursive x1 b1, Recursive x2 b2) =>
if eq_nat_dec x1 x2
then ty_eq_dec' b1 b2
else false
| _ => false
end
with subProduct' (ts1 ts2 : productTy) {struct ts1} : bool :=
match (ts1, ts2) with
| (_, PT_Nil) => true
| (PT_Cons t1 ts1, PT_Cons t2 ts2) =>
ty_eq_dec' t1 t2 && subProduct' ts1 ts2
| _ => false
end.
Lemma or_true : forall b1 b2,
b1 || b2 = true -> b1 = true \/ b2 = true.
Lemma subTy'_sound : forall (t2 t1 : ty),
subTy' t1 t2 = true
-> forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2.
Hint Resolve subTy'_sound.
Definition subTy2 : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
Definition subTy1 : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
Definition subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
Import Datatypes.
Lemma btn_four : forall len, bvec_to_nat (nat_to_bvec (S (S (S len))) 4) = 4.
Lemma eqMod_refl' : forall m n1 n2,
n1 = n2
-> eqMod m n1 n2.
Lemma four_lt_pow2 : forall len, 4 <= pow2 (S (S len)).
Lemma add_sub_four : forall n v,
bvec_to_nat n >= 4
-> badd32 n v = badd32 (bsub32 n four) (binc4 v).
Lemma bzero_inv : forall len (n : Bvector len),
bvec_to_nat n = 0
-> n = @bzero len.
Definition seekInProduct : forall (n : int32) (ts : productTy),
{ts' : _
| forall ctx v, hasTy ctx v (Product ts)
-> hasTy ctx (badd32 n v) (Product ts')}.
Definition typeofArith : forall (aop : arith_op) (t1 t2 : ty),
{t : ty
| forall ctx v1 v2,
hasTy ctx v1 t1
-> hasTy ctx v2 t2
-> hasTy ctx (eval_arith aop v1 v2) t}.
Definition typeofCell : forall (t : ty),
sig_option (fun t' =>
forall ctx v,
hasTy ctx v t
-> ctx v = Some t').
Definition considerNeq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx v1,
hasTy ctx v1 t
-> v1 <> v
-> hasTy ctx v1 t'}.
Lemma zero_one_neq : forall len, @bzero (S len) <> @bone (S len).
Definition considerDerefEq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx st v1,
(forall a,
match ctx a with
| None => True
| Some t2 => hasTy ctx (get_mem32 st a) t2
end)
-> hasTy ctx v1 t
-> get_mem32 st v1 = v
-> hasTy ctx v1 t'}.
Definition considerDerefNeq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx st v1,
(forall a,
match ctx a with
| None => True
| Some t2 => hasTy ctx (get_mem32 st a) t2
end)
-> hasTy ctx v1 t
-> get_mem32 st v1 <> v
-> hasTy ctx v1 t'}.
End MemoryTySys.
Module Verifier (Param : DRIVER_REGIONS).
Module MyParam <: DRIVER_PARAM.
Module Regions := Param.
Module Sys := MemoryTySys.
End MyParam.
Module Dr := Driver(MyParam).
End Verifier.