Library mcertikos.mm.DAbsHandlerCode
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import ContainerGenSpec.
Require Import DAbsHandlerCSource.
Require Import TacticsForTesting.
Require Import DAbsHandler.
Require Import AbstractDataType.
Module DABSHANDLERCODE.
Open Scope Z_scope.
Lemma convert_quota : ∀ i, Int.unsigned i < num_id →
Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 0) = Int.unsigned i × CSIZE + QUOTA.
Proof.
intros i Hi.
assert (Hrange:= Int.unsigned_range_2 i).
rewrite Int.mul_signed.
rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
Qed.
Lemma convert_usage : ∀ i, Int.unsigned i < num_id →
Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 4) = Int.unsigned i × CSIZE + USAGE.
Proof.
intros i Hi.
assert (Hrange:= Int.unsigned_range_2 i).
rewrite Int.mul_signed.
rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
Qed.
Lemma convert_parent : ∀ i, Int.unsigned i < num_id →
Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 8) = Int.unsigned i × CSIZE + PARENT.
Proof.
intros i Hi.
assert (Hrange:= Int.unsigned_range_2 i).
rewrite Int.mul_signed.
rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
Qed.
Lemma convert_nchildren : ∀ i, Int.unsigned i < num_id →
Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 12) = Int.unsigned i × CSIZE + NCHILDREN.
Proof.
intros i Hi.
assert (Hrange:= Int.unsigned_range_2 i).
rewrite Int.mul_signed.
rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
Qed.
Lemma convert_used : ∀ i, Int.unsigned i < num_id →
Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 16) = Int.unsigned i × CSIZE + USED.
Proof.
intros i Hi.
assert (Hrange:= Int.unsigned_range_2 i).
rewrite Int.mul_signed.
rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
Qed.
Close Scope Z_scope.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Opaque PTree.get PTree.set.
Local Open Scope Z_scope.
Section ContainerInit.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops) (cdata_prf:= dabshandler_data_prf)) :=
AC_LOC ↦ container_loc_type ⊕ boot_loader ↦ gensem bootloader0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section InitBody.
Context `{Hwb: WritableBlockOps}.
Context `{Hwbg: WritableBlockAllowGlobals WB}.
Variable (s: stencil).
Variables (ge: genv) (b_ac b_bl: block).
Hypothesis Hstencil_matches: stencil_matches s ge.
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Hypothesis hboot_loader1 : Genv.find_symbol ge boot_loader = Some b_bl.
Hypothesis hboot_loader2 : Genv.find_funct_ptr ge b_bl =
Some (External (EF_external boot_loader
(signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Lemma container_init_body_correct:
∀ m m´ (d d´ : cdata RData) env le mbi (m1 m2 m3 m4 : memb),
env = PTree.empty _ → le ! _mbi = Some (Vint mbi) →
bootloader0_spec (Int.unsigned mbi) d = Some d´ →
Mem.store Mint32 m b_ac QUOTA (Vint (Int.repr root_quota)) = Some m1 →
Mem.store Mint32 m1 b_ac USAGE (Vint Int.zero) = Some m2 →
Mem.store Mint32 m2 b_ac PARENT (Vint Int.zero) = Some m3 →
Mem.store Mint32 m3 b_ac NCHILDREN (Vint Int.zero) = Some m4 →
Mem.store Mint32 m4 b_ac USED (Vint Int.one) = Some m´ →
exec_stmt ge env le (m, d) container_init_body E0 le (m´, d´) Out_normal.
Proof.
intros; subst.
assert (Hmax:= max_unsigned_val).
unfold Int.zero in *; unfold Int.one in ×.
unfold container_init_body.
generalize sizeof_AC; intro acsize.
replace E0 with (E0 ** E0 ** E0 ** E0 ** E0 ** E0); auto.
Require Import CommonTactic.
unfold bootloader0_spec in H1; subdestruct; inv H1.
vcgen; vcgen.
repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
repeat vcgen; simpl.
unfold QUOTA in H2; rewrite H2; auto.
vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
repeat vcgen; simpl.
unfold USAGE in H3; rewrite H3; auto.
vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
repeat vcgen; simpl.
unfold PARENT in H4; rewrite H4; auto.
vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
repeat vcgen; simpl.
unfold NCHILDREN in H5; rewrite H5; auto.
unfold Mem.storev; simpl; unfold lift; simpl.
repeat vcgen; simpl.
unfold USED in H6; rewrite H6; auto.
Qed.
End InitBody.
Theorem container_init_code_correct:
spec_le (container_init ↦ container_init_spec_low)
(〚container_init ↦ f_container_init〛 L).
Proof.
fbigstep_pre L.
econstructor; eauto.
simpl; unfold type_of_function; auto.
simpl; auto.
econstructor; eauto.
repeat constructor; simpl; auto.
intros a1 a2 Ha1 Ha2; inv Ha2.
assert (Hexec:= container_init_body_correct _ _ _ _ makeglobalenv H0 Hb2fs Hb2fp m0 m´0 labd labd´
(PTree.empty _) (PTree.set _mbi (Vint mbi) (PTree.empty _)) mbi m1 m2 m3 m4).
simpl; apply Hexec; auto.
simpl; auto.
simpl; auto.
Qed.
End ContainerInit.
Section ContainerGetParent.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) := AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetParentBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv) (b_ac: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_get_parent_body_correct:
∀ m d env le v i,
env = PTree.empty _ → le ! _id = Some (Vint i) → 0 ≤ Int.unsigned i < num_id →
Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + PARENT) = Some (Vint v) →
exec_stmt ge env le (m, d) container_get_parent_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
Proof.
intros; subst.
vcgen; vcgen; vcgen.
vcgen; vcgen.
{
vcgen.
vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
vcgen.
}
{
assert (0 ≤ sizeof t_struct_AC ≤ Int.max_unsigned) as Hsize.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
vcgen.
apply deref_loc_copy; auto.
rewrite Int.unsigned_repr; auto.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
}
{
repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
unfold Mem.loadv.
rewrite Int.unsigned_repr.
rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
rewrite max_unsigned_val; omega.
}
Qed.
End GetParentBody.
Theorem container_get_parent_code_correct:
spec_le (container_get_parent ↦ container_get_parent_spec_low)
(〚container_get_parent ↦ f_container_get_parent〛 L).
Proof.
fbigstep_pre L.
fbigstep (container_get_parent_body_correct _ _ H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_get_parent) (Vint i :: nil) (PTree.empty _))) m´.
Qed.
End ContainerGetParent.
Section ContainerGetQuota.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) := AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetQuotaBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv) (b_ac: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_get_quota_body_correct:
∀ m d env le v i,
env = PTree.empty _ → le ! _id = Some (Vint i) → 0 ≤ Int.unsigned i < num_id →
Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint v) →
exec_stmt ge env le (m, d) container_get_quota_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
Proof.
intros; subst.
vcgen; vcgen; vcgen.
vcgen; vcgen.
{
vcgen.
vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
vcgen.
}
{
assert (0 ≤ sizeof t_struct_AC ≤ Int.max_unsigned) as Hsize.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
vcgen.
apply deref_loc_copy; auto.
rewrite Int.unsigned_repr; auto.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
}
{
repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
unfold Mem.loadv.
rewrite Int.unsigned_repr.
rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
rewrite max_unsigned_val; omega.
}
Qed.
End GetQuotaBody.
Theorem container_get_quota_code_correct:
spec_le (container_get_quota ↦ container_get_quota_spec_low)
(〚container_get_quota ↦ f_container_get_quota〛 L).
Proof.
fbigstep_pre L.
fbigstep (container_get_quota_body_correct _ _ H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_get_quota) (Vint i :: nil) (PTree.empty _))) m´.
Qed.
End ContainerGetQuota.
Section ContainerGetUsage.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) := AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetUsageBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv) (b_ac: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_get_usage_body_correct:
∀ m d env le v i,
env = PTree.empty _ → le ! _id = Some (Vint i) → 0 ≤ Int.unsigned i < num_id →
Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint v) →
exec_stmt ge env le (m, d) container_get_usage_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
Proof.
intros; subst.
vcgen; vcgen; vcgen.
vcgen; vcgen.
{
vcgen.
vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
vcgen.
}
{
assert (0 ≤ sizeof t_struct_AC ≤ Int.max_unsigned) as Hsize.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
vcgen.
apply deref_loc_copy; auto.
rewrite Int.unsigned_repr; auto.
rewrite max_unsigned_val; rewrite sizeof_AC; omega.
}
{
repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
unfold Mem.loadv.
rewrite Int.unsigned_repr.
rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
rewrite max_unsigned_val; omega.
}
Qed.
End GetUsageBody.
Theorem container_get_usage_code_correct:
spec_le (container_get_usage ↦ container_get_usage_spec_low)
(〚container_get_usage ↦ f_container_get_usage〛 L).
Proof.
fbigstep_pre L.
fbigstep (container_get_usage_body_correct _ _ H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_get_usage) (Vint i :: nil) (PTree.empty _))) m´.
Qed.
End ContainerGetUsage.
Section ContainerCanConsume.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) := AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CanConsumeBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv) (b_ac: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_can_consume_body_correct:
∀ m d env le i n q u,
env = PTree.empty _ → le ! _id = Some (Vint i) → le ! _n = Some (Vint n) →
0 ≤ Int.unsigned i < num_id →
Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint q) →
Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
exec_stmt ge env le (m, d) container_can_consume_body E0 le (m, d)
(Out_return (Some (Vint
(match (Int.unsigned n <=? Int.unsigned q,
Int.unsigned u <=? Int.unsigned q - Int.unsigned n) with
| (true, true) ⇒ Int.one
| _ ⇒ Int.zero end), tint))).
Proof.
intros; subst.
assert (((Int.unsigned n <=? Int.unsigned q) = true ∧
(Int.unsigned u <=? Int.unsigned q - Int.unsigned n) = true) ∨
((Int.unsigned n <=? Int.unsigned q) = true ∧
(Int.unsigned u <=? Int.unsigned q - Int.unsigned n) = false) ∨
(Int.unsigned n <=? Int.unsigned q) = false) as Hcases.
destruct (Int.unsigned n <=? Int.unsigned q); auto.
destruct (Int.unsigned u <=? Int.unsigned q - Int.unsigned n); auto.
destruct Hcases as [Hcase1|Hcase2].
destruct Hcase1 as [Hle1 Hle2].
rewrite Hle1; rewrite Hle2.
vcgen; vcgen; try discriminate.
vcgen; simpl.
{
vcgen; vcgen; eauto.
vcgen; vcgen.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold QUOTA; omega.
vcgen.
}
{
vcgen; simpl; unfold bool_val; simpl.
destruct (zlt (Int.unsigned q) (Int.unsigned n)); simpl; unfold Int.eq.
rewrite Z.leb_le in Hle1; omega.
destruct (zeq (Int.unsigned Int.one) (Int.unsigned Int.zero)); simpl.
inv e.
eauto.
}
{
vcgen; simpl.
vcgen.
vcgen.
vcgen.
vcgen; vcgen.
vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_usage; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold USAGE; omega.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen; vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold QUOTA; omega.
vcgen; eauto.
vcgen.
vcgen.
simpl.
rewrite Int.unsigned_repr.
destruct (zlt (Int.unsigned q - Int.unsigned n) (Int.unsigned u)).
rewrite Z.leb_le in Hle2; omega.
vcgen.
rewrite Z.leb_le in Hle1; assert (Hrange := Int.unsigned_range_2 q).
rewrite max_unsigned_val in Hrange |- ×.
split; try omega.
apply Z.le_trans with (m := Int.unsigned q); try omega.
assert (Hrange´ := Int.unsigned_range_2 n); omega.
simpl; vcgen; vcgen.
}
replace E0 with (E0 ** E0).
vcgen; vcgen.
{
destruct Hcase2 as [[Hle1 Hle2]|Hle].
vcgen.
{
vcgen; vcgen; eauto.
vcgen.
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold QUOTA; omega.
vcgen; eauto.
}
{
simpl; destruct (zlt (Int.unsigned q) (Int.unsigned n)).
rewrite Z.leb_le in Hle1; omega.
vcgen.
}
{
vcgen.
vcgen; vcgen; eauto.
vcgen.
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_usage; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold USAGE; omega.
vcgen; eauto.
vcgen.
vcgen.
vcgen.
vcgen.
vcgen; vcgen.
vcgen.
vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold QUOTA; omega.
vcgen; eauto.
vcgen.
vcgen.
simpl.
rewrite Int.unsigned_repr.
destruct (zlt (Int.unsigned q - Int.unsigned n) (Int.unsigned u)).
vcgen.
rewrite Z.leb_nle in Hle2; omega.
rewrite Z.leb_le in Hle1; assert (Hrange := Int.unsigned_range_2 q).
rewrite max_unsigned_val in Hrange |- ×.
split; try omega.
apply Z.le_trans with (m := Int.unsigned q); try omega.
assert (Hrange´ := Int.unsigned_range_2 n); omega.
simpl; vcgen.
}
vcgen.
vcgen; vcgen; eauto.
vcgen.
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
apply deref_loc_copy; auto.
vcgen.
vcgen.
apply deref_loc_value with (chunk := Mint32); auto.
unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
rewrite Int.add_unsigned.
rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
unfold CSIZE; unfold QUOTA; omega.
vcgen; eauto.
simpl.
destruct (zlt (Int.unsigned q) (Int.unsigned n)).
vcgen.
rewrite Z.leb_nle in Hle; omega.
simpl; vcgen.
}
{
destruct Hcase2 as [[Hle1 Hle2]|Hle].
rewrite Hle1; rewrite Hle2; vcgen; vcgen.
rewrite Hle; vcgen; vcgen.
}
{
simpl; auto.
}
Qed.
End CanConsumeBody.
Theorem container_can_consume_code_correct:
spec_le (container_can_consume ↦ container_can_consume_spec_low)
(〚container_can_consume ↦ f_container_can_consume〛 L).
Proof.
fbigstep_pre L.
fbigstep (container_can_consume_body_correct _ _ H (fst m´) (snd m´) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_can_consume)
(Vint i :: Vint n :: nil) (PTree.empty _))) m´.
Qed.
End ContainerCanConsume.
Section ContainerSplit.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) :=
AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SplitBody.
Context `{Hwb: WritableBlockOps}.
Context `{Hwbg: WritableBlockAllowGlobals WB}.
Variable (s: stencil).
Variables (ge: genv) (b_ac b_bl: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_split_body_correct:
∀ m m´ (d : cdata RData) env le i n j u nc (m1 m2 m3 m4 m5 m6: memb),
env = PTree.empty _ → le ! _id = Some (Vint i) → le ! _n = Some (Vint n) →
le ! _child = Some (Vint j) → 0 ≤ Int.unsigned i < num_id → 0 ≤ Int.unsigned j < num_id →
Mem.load Mint32 m b_ac (Int.unsigned i × CSIZE + USED) = Some (Vint Int.one) →
Mem.load Mint32 m b_ac (Int.unsigned j × CSIZE + USED) = Some (Vint Int.zero) →
Mem.load Mint32 m b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
Mem.load Mint32 m b_ac (Int.unsigned i × CSIZE + NCHILDREN) = Some (Vint nc) →
Mem.store Mint32 m b_ac (Int.unsigned j × CSIZE + USED) (Vint Int.one) = Some m1 →
Mem.store Mint32 m1 b_ac (Int.unsigned j × CSIZE + QUOTA) (Vint n) = Some m2 →
Mem.store Mint32 m2 b_ac (Int.unsigned j × CSIZE + USAGE) (Vint Int.zero) = Some m3 →
Mem.store Mint32 m3 b_ac (Int.unsigned j × CSIZE + PARENT) (Vint i) = Some m4 →
Mem.store Mint32 m4 b_ac (Int.unsigned j × CSIZE + NCHILDREN) (Vint Int.zero) = Some m5 →
Mem.store Mint32 m5 b_ac (Int.unsigned i × CSIZE + USAGE) (Vint (Int.add u n)) = Some m6 →
Mem.store Mint32 m6 b_ac (Int.unsigned i × CSIZE + NCHILDREN) (Vint (Int.add nc Int.one)) = Some m´ →
exec_stmt ge env le (m, d) container_split_body E0 le (m´, d) (Out_return (Some (Vint j, tint))).
Proof.
intros; subst.
assert (Hmax:= max_unsigned_val).
assert (Hsep: ∀ m k1 k2 a b : Z, a ≠ b → 0 ≤ m →
0 ≤ k1 → k1 + size_chunk Mint32 ≤ m → 0 ≤ k2 → k2 + size_chunk Mint32 ≤ m →
a × m + k1 + size_chunk Mint32 ≤ b × m + k2 ∨ b × m + k2 + size_chunk Mint32 ≤ a × m + k1).
intros m0 k1 k2 a1 a2 Ha_neq Hm_0 Hk1_0 Hle1 Hk2_0 Hle2.
assert (a1 < a2 ∨ a2 < a1) as Ha; try omega.
destruct Ha; [left | right].
apply Z.le_trans with (m := a1 × m0 + m0); try omega.
replace (a1 × m0 + m0) with ((a1 + 1) × m0).
assert (a1 + 1 ≤ a2) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m0) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
apply Z.le_trans with (m := a2 × m0 + m0); try omega.
replace (a2 × m0 + m0) with ((a2 + 1) × m0).
assert (a2 + 1 ≤ a1) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m0) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
unfold CSIZE in *; unfold QUOTA in *; unfold USAGE in *;
unfold PARENT in *; unfold NCHILDREN in *; unfold USED in ×.
unfold size_chunk in Hsep.
assert (Hneq: Int.unsigned i ≠ Int.unsigned j).
intro Hcon; rewrite Hcon in H5; rewrite H5 in H6; inv H6.
unfold Int.zero in *; unfold Int.one in ×.
replace E0 with (E0 ** E0 ** E0 ** E0 ** E0 ** E0 ** E0 ** E0); auto.
vcgen; vcgen.
vcgen; vcgen; vcgen; eauto.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul j (Int.repr 20)) with (Int.repr (Int.unsigned j × 20)); auto.
apply deref_loc_copy; auto.
unfold sizeof; repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold CSIZE, USED in H9; rewrite H9; auto.
vcgen.
vcgen; vcgen; vcgen; eauto.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul j (Int.repr 20)) with (Int.repr (Int.unsigned j × 20)); auto.
apply deref_loc_copy; auto.
unfold sizeof; repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold CSIZE, QUOTA in H10; rewrite H10; auto.
vcgen.
vcgen; vcgen; vcgen; eauto.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul j (Int.repr 20)) with (Int.repr (Int.unsigned j × 20)); auto.
apply deref_loc_copy; auto.
unfold sizeof; repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold CSIZE, USAGE in H11; rewrite H11; auto.
vcgen.
vcgen; vcgen; vcgen; eauto.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul j (Int.repr 20)) with (Int.repr (Int.unsigned j × 20)); auto.
apply deref_loc_copy; auto.
unfold sizeof; repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold CSIZE, PARENT in H12; rewrite H12; auto.
vcgen.
vcgen; vcgen; vcgen; eauto.
vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul j (Int.repr 20)) with (Int.repr (Int.unsigned j × 20)); auto.
apply deref_loc_copy; auto.
unfold sizeof; repeat vcgen.
unfold Mem.storev; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold CSIZE, NCHILDREN in H13; rewrite H13; auto.
vcgen.
vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul i (Int.repr 20)) with (Int.repr (Int.unsigned i × 20)); auto.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul i (Int.repr 20)) with (Int.repr (Int.unsigned i × 20)); auto.
unfold Mem.loadv; unfold set; simpl; unfold lift; simpl.
rewrite 2 Int.unsigned_repr; try omega.
rewrite (Mem.load_store_other _ _ _ _ _ _ H13); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H12); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H11); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H10); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H9); try solve [right; apply Hsep; auto; try omega]; eauto.
rewrite Int.unsigned_repr; try omega.
omega.
vcgen.
vcgen.
unfold Mem.storev; unfold set; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
rewrite <- Int.add_unsigned; rewrite H14; eauto.
omega.
omega.
vcgen.
vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul i (Int.repr 20)) with (Int.repr (Int.unsigned i × 20)); auto.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
simpl; unfold sem_add; simpl; unfold align; simpl.
rewrite Int.add_zero_l; rewrite Int.mul_commut.
replace (Int.mul i (Int.repr 20)) with (Int.repr (Int.unsigned i × 20)); auto.
unfold Mem.loadv; unfold set; simpl; unfold lift; simpl.
rewrite 2 Int.unsigned_repr; try omega.
rewrite (Mem.load_store_other _ _ _ _ _ _ H14); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H13); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H12); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H11); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H10); try solve [right; apply Hsep; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ H9); try solve [right; apply Hsep; auto; try omega]; eauto.
right; unfold size_chunk; omega.
rewrite Int.unsigned_repr; try omega.
omega.
vcgen.
vcgen.
unfold Mem.storev; unfold set; simpl; unfold lift; simpl.
rewrite Int.unsigned_repr; try omega.
unfold Int.one; rewrite <- Int.add_unsigned; rewrite H15; eauto.
omega.
omega.
repeat vcgen.
Qed.
End SplitBody.
Theorem container_split_code_correct:
spec_le (container_split ↦ container_split_spec_low)
(〚container_split ↦ f_container_split〛 L).
Proof.
fbigstep_pre L.
destruct H6, H7, H8, H9, H10, H11, H12.
econstructor; eauto.
simpl; unfold type_of_function; auto.
simpl; auto.
econstructor; eauto.
repeat constructor; simpl; auto.
intro Ht; destruct Ht as [Ht|[Ht|Ht]]; inv Ht.
intro Ht; destruct Ht as [Ht|Ht]; inv Ht.
intros a1 a2 Ha1 Ha2; inv Ha2.
assert (Hexec:= container_split_body_correct _ _ H (fst m) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_split)
(Vint i :: Vint n :: Vint j :: nil) (PTree.empty val))
i n j u nc (fst m1) (fst m2) (fst m3) (fst m4) (fst m5) (fst m6)).
simpl; destruct m as [mm1 mm2]; apply Hexec; simpl in *; auto.
simpl; split; auto; discriminate.
assert (Heq: π_data m = π_data m´) by congruence.
destruct m´ as [mm1´ mm2´].
simpl in *; rewrite <- Heq; auto.
Qed.
End ContainerSplit.
Section ContainerAlloc.
Let L: compatlayer (cdata RData (cdata_ops:= dabshandler_data_ops)) := AC_LOC ↦ container_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section AllocBody.
Context `{Hwb: WritableBlockOps}.
Context `{Hwbg: WritableBlockAllowGlobals WB}.
Variable (s: stencil).
Variables (ge: genv) (b_ac: block).
Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.
Lemma container_alloc_body_correct0:
∀ m d env i u,
env = PTree.empty _ →
0 ≤ Int.unsigned i < num_id →
Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint u) →
exec_stmt ge env (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))
(m,d) container_alloc_body E0
(PTree.set t_q (Vint u) (PTree.set t_u (Vint u)
(PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))))
(m,d) (Out_return (Some (Vzero,tint))).
Proof.
intros m d env i u Henv Hi Hl1 Hl2; subst.
assert (Hmax:= max_unsigned_val).
replace E0 with (E0 ** E0 ** E0); auto.
vcgen; vcgen; [|vcgen].
{
vcgen; vcgen; vcgen; try solve [vcgen].
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
repeat vcgen.
vcgen.
apply deref_loc_copy; auto.
eapply deref_loc_value; simpl; auto.
unfold lift; unfold align; simpl; repeat vcgen.
rewrite Z.mul_comm; apply Hl1.
}
{
vcgen.
vcgen; vcgen; vcgen; try solve [vcgen].
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
repeat vcgen.
vcgen.
apply deref_loc_copy; auto.
simpl; unfold lift; unfold align; simpl; repeat vcgen.
rewrite Z.mul_comm; apply Hl2.
}
apply exec_Sseq_2; try discriminate; repeat vcgen.
Qed.
Lemma container_alloc_body_correct1:
∀ m m´ d env i u q,
env = PTree.empty _ →
0 ≤ Int.unsigned i < num_id → Int.unsigned u < Int.unsigned q →
Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint q) →
Mem.store Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) (Vint (Int.add u Int.one)) = Some (m´,d) →
exec_stmt ge env (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))
(m,d) container_alloc_body E0
(PTree.set t_q (Vint q) (PTree.set t_u (Vint u)
(PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))))
(m´,d) (Out_return (Some (Vone,tint))).
Proof.
intros m m´ d env i u q Henv Hi Hlt Hl1 Hl2 Hs; subst.
assert (Hmax:= max_unsigned_val).
replace E0 with (E0 ** E0 ** E0 ** E0 ** E0); auto.
vcgen; vcgen; [|vcgen]; [| |vcgen]; [| | |vcgen].
{
vcgen; vcgen; vcgen; try solve [vcgen].
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
vcgen; eauto.
vcgen.
vcgen.
apply deref_loc_copy; auto.
eapply deref_loc_value; simpl; auto.
unfold lift; unfold align; simpl; repeat vcgen.
rewrite Z.mul_comm; apply Hl1.
}
{
vcgen.
vcgen; vcgen; vcgen; try solve [vcgen].
vcgen.
vcgen; vcgen.
vcgen; vcgen; eauto.
apply deref_loc_reference; auto.
repeat vcgen.
vcgen.
apply deref_loc_copy; auto.
simpl; unfold lift; unfold align; simpl; repeat vcgen.
rewrite Z.mul_comm; apply Hl2.
}
{
repeat vcgen.
}
{
vcgen.
vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; eauto; try discriminate.
apply deref_loc_reference; auto.
repeat vcgen.
vcgen.
repeat vcgen.
vcgen.
simpl; repeat vcgen.
rewrite Z.mul_comm.
simpl in *; unfold lift in *; simpl in ×.
rewrite Int.unsigned_repr.
rewrite <- Int.unsigned_one; rewrite <- Int.add_unsigned.
unfold CSIZE, USAGE in Hs; rewrite Hs; eauto.
omega.
}
repeat vcgen.
Qed.
End AllocBody.
Theorem container_alloc_code_correct:
spec_le (container_alloc ↦ container_alloc_spec_low)
(〚container_alloc ↦ f_container_alloc〛 L).
Proof.
fbigstep_pre L.
{
econstructor; eauto.
simpl; unfold type_of_function; auto.
simpl; auto.
econstructor; eauto.
repeat constructor; simpl; auto.
intros a1 a2 Ha1 Ha2.
inv Ha1.
inv Ha2; try discriminate.
inv H4; try discriminate.
inv H5.
inv H4.
assert (Hexec:= container_alloc_body_correct0 _ _ H (fst m´) (snd m´) (PTree.empty _) i u).
replace (fst m´, snd m´) with m´ in Hexec; [| destruct m´; auto].
simpl in *; apply Hexec; auto.
simpl; split; auto; discriminate.
simpl; auto.
}
{
econstructor; eauto.
simpl; unfold type_of_function; auto.
simpl; auto.
econstructor; eauto.
repeat constructor; simpl; auto.
intros a1 a2 Ha1 Ha2.
inv Ha1.
inv Ha2; try discriminate.
inv H6; try discriminate.
inv H7.
inv H6.
assert (Hexec:= container_alloc_body_correct1 _ _ H (fst m) (fst m´) (snd m) (PTree.empty _) i u q).
replace (fst m, snd m) with m in Hexec; [| destruct m; auto].
simpl in *; apply Hexec; auto.
unfold lift in *; simpl in ×.
destruct H4 as [H4 _]; rewrite H4; auto.
simpl; split; auto; discriminate.
simpl; destruct H4 as [_ H4].
destruct m´; simpl in *; subst; auto.
}
Qed.
End ContainerAlloc.
End WithPrimitives.
End DABSHANDLERCODE.