Library mcertikos.devdrivers.MQTicketLockCode
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 LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import MQTicketLock.
Require Import ZArith.Zwf.
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 ConsoleBuffIntroGenSpec.
Require Import MQTicketLockCSource.
Require Import AbstractDataType.
Module MQTICKETLOCKCODE.
Section WithPrimitives.
Context `{real_params_ops: RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
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}.
Local Open Scope Z_scope.
Section CONS_BUF_WPOS.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_WPOS_Body.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_wpos_body_correct: ∀ m d env le val,
env = PTree.empty _ →
Mem.load Mint32 (m, d) bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_wpos_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_wpos_body.
esplit.
repeat vcgen.
Qed.
End CONS_BUF_WPOS_Body.
Theorem cons_buf_wpos_correct:
spec_le (cons_buf_wpos ↦ cons_buf_wpos_concrete_spec_low) (〚cons_buf_wpos ↦ f_cons_buf_wpos 〛L).
Proof.
fbigstep_pre L.
fbigstep (cons_buf_wpos_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_wpos)
(nil)
(create_undef_temps (fn_temps f_cons_buf_wpos)))) m´.
Qed.
End CONS_BUF_WPOS.
Section CONS_BUF_INIT.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_INIT_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_init_body_correct: ∀ m m0 m´ d env le,
env = PTree.empty _ →
Mem.store Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.zero)) = Some m0 →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint (Int.zero)) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_init_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_init_body.
simpl in ×.
repeat vcgen.
Opaque Z.mul.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (Int.repr 0) with Int.zero.
rewrite H0.
reflexivity.
omega.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (Int.repr 0) with Int.zero.
rewrite H1.
reflexivity.
omega.
Qed.
End CONS_BUF_INIT_Body.
Theorem cons_buf_init_correct:
spec_le (cons_buf_init ↦ cons_buf_init_concrete_spec_low) (〚cons_buf_init ↦ f_cons_buf_init 〛L).
Proof.
fbigstep_pre L. destruct H0, H1.
fbigstep (cons_buf_init_body_correct (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_init)
(nil)
(create_undef_temps (fn_temps f_cons_buf_init)))) m.
simpl.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_INIT.
Section CONS_BUF_READ.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_READ_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_read_body_correct1: ∀ m d env le rpos wpos,
env = PTree.empty _ →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
Int.unsigned rpos = Int.unsigned wpos →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_read_body E0 le´ (m, d) (Out_return (Some (Vint (Int.zero), tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_read_body.
esplit.
repeat vcgen.
Qed.
Lemma cons_buf_read_body_correct2: ∀ m m´ d env le rpos wpos c,
env = PTree.empty _ →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
Int.unsigned rpos ≠ Int.unsigned wpos →
Mem.load Mint32 m bcons_buf_loc ((Int.unsigned rpos) × 4) = Some (Vint c) →
Mem.store Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.repr((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE))) = Some m´ →
0 ≤ Int.unsigned rpos < CONSOLE_BUFFER_SIZE →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_read_body E0 le´ (m´, d) (Out_return (Some (Vint c, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_read_body.
esplit.
repeat vcgen.
Opaque Z.mul.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite Z.mul_comm.
assumption.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
change (512 × 4) with 2048 in H4.
rewrite H4.
reflexivity.
omega.
Qed.
End CONS_BUF_READ_Body.
Theorem cons_buf_read_correct:
spec_le (cons_buf_read ↦ cons_buf_read_concrete_spec_low) (〚cons_buf_read ↦ f_cons_buf_read 〛L).
Proof.
fbigstep_pre L.
fbigstep (cons_buf_read_body_correct1 (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_read)
(nil)
(create_undef_temps (fn_temps f_cons_buf_read)))) m´.
destruct H4.
fbigstep (cons_buf_read_body_correct2 (Genv.globalenv p) b0 H (fst m) (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_read)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_read)))) m.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_READ.
Section CONS_BUF_WRITE.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_WRITE_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_write_body_correct1: ∀ m m0 m´ d env le rpos wpos wpos´ c,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
Mem.store Mint32 m bcons_buf_loc (Int.unsigned wpos × 4) (Vint c) = Some m0 →
wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Int.unsigned wpos´ ≠ Int.unsigned rpos →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_write_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_write_body.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 ≤ Int.max_unsigned).
{
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
}
repeat vcgen.
Opaque Z.mul.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite Z.mul_comm.
rewrite H3.
reflexivity.
omega.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (513 × 4) with 2052 in H1.
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
eassumption.
right.
right.
simpl.
omega.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
lift_unfold.
rewrite Int.unsigned_repr.
discharge_cmp.
change (513 × 4) with 2052 in H7.
rewrite H7.
reflexivity.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite (Mem.load_store_other _ _ _ _ _ _ H7).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H5.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
change (513 × 4) with 2052 in H7.
rewrite (Mem.load_store_same _ _ _ _ _ _ H7).
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
rewrite Int.unsigned_repr in H6.
repeat vcgen.
assumption.
repeat vcgen.
Qed.
Lemma cons_buf_write_body_correct2: ∀ m m0 m1 m´ d env le rpos wpos wpos´ rpos´ c,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
Mem.store Mint32 m bcons_buf_loc (Int.unsigned wpos × 4) (Vint c) = Some m0 →
wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m1 →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Int.unsigned wpos´ = Int.unsigned rpos →
rpos´ = Int.repr ((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.store Mint32 m1 bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint rpos´) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_write_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_write_body.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 ≤ Int.max_unsigned).
{
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
}
Require Import TacticsForTesting.
Opaque align.
d3 vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
change (align 0 4) with 0.
discharge_cmp.
lift_unfold.
rewrite Z.mul_comm.
rewrite H3.
reflexivity.
eassumption.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
discharge_cmp.
Opaque Z.mul Z.add.
repeat vcgen.
change (align 0 4) with 0.
change (align (0 + 4 × 512) 4) with 2048.
change (align (2048 + 4) 4) with 2052.
lift_unfold.
rewrite Int.unsigned_repr; try omega.
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
eassumption.
right.
right.
simpl.
omega.
change (align (align (align 0 4 + 4 × Z.max 0 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
lift_unfold.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
change ((512 + 1) × 4) with 2052 in H5.
rewrite H5.
reflexivity.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
rewrite (Mem.load_store_other _ _ _ _ _ _ H5).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H6.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
lift_unfold.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
change ((512 + 1) × 4) with 2052 in H5.
rewrite (Mem.load_store_same _ _ _ _ _ _ H5).
reflexivity.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
repeat vcgen.
rewrite Int.unsigned_repr in H7; try omega.
repeat vcgen.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
rewrite (Mem.load_store_other _ _ _ _ _ _ H5).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H6.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
discharge_cmp.
change (512 × 4) with 2048 in H9.
rewrite H9.
reflexivity.
rewrite <- H7.
rewrite Int.unsigned_repr; try omega.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
Qed.
End CONS_BUF_WRITE_Body.
Theorem cons_buf_write_correct:
spec_le (cons_buf_write ↦ cons_buf_write_concrete_spec_low) (〚cons_buf_write ↦ f_cons_buf_write 〛L).
Proof.
fbigstep_pre L. destruct H2, H6.
fbigstep (cons_buf_write_body_correct1 (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_write)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_write)))) m.
simpl.
destruct m´.
reflexivity.
destruct H2, H4, H8.
fbigstep (cons_buf_write_body_correct2 (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m1) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_write)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_write)))) m.
simpl.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_WRITE.
End WithPrimitives.
End MQTICKETLOCKCODE.
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 LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import MQTicketLock.
Require Import ZArith.Zwf.
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 ConsoleBuffIntroGenSpec.
Require Import MQTicketLockCSource.
Require Import AbstractDataType.
Module MQTICKETLOCKCODE.
Section WithPrimitives.
Context `{real_params_ops: RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
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}.
Local Open Scope Z_scope.
Section CONS_BUF_WPOS.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_WPOS_Body.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_wpos_body_correct: ∀ m d env le val,
env = PTree.empty _ →
Mem.load Mint32 (m, d) bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_wpos_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_wpos_body.
esplit.
repeat vcgen.
Qed.
End CONS_BUF_WPOS_Body.
Theorem cons_buf_wpos_correct:
spec_le (cons_buf_wpos ↦ cons_buf_wpos_concrete_spec_low) (〚cons_buf_wpos ↦ f_cons_buf_wpos 〛L).
Proof.
fbigstep_pre L.
fbigstep (cons_buf_wpos_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_wpos)
(nil)
(create_undef_temps (fn_temps f_cons_buf_wpos)))) m´.
Qed.
End CONS_BUF_WPOS.
Section CONS_BUF_INIT.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_INIT_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_init_body_correct: ∀ m m0 m´ d env le,
env = PTree.empty _ →
Mem.store Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.zero)) = Some m0 →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint (Int.zero)) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_init_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_init_body.
simpl in ×.
repeat vcgen.
Opaque Z.mul.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (Int.repr 0) with Int.zero.
rewrite H0.
reflexivity.
omega.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (Int.repr 0) with Int.zero.
rewrite H1.
reflexivity.
omega.
Qed.
End CONS_BUF_INIT_Body.
Theorem cons_buf_init_correct:
spec_le (cons_buf_init ↦ cons_buf_init_concrete_spec_low) (〚cons_buf_init ↦ f_cons_buf_init 〛L).
Proof.
fbigstep_pre L. destruct H0, H1.
fbigstep (cons_buf_init_body_correct (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_init)
(nil)
(create_undef_temps (fn_temps f_cons_buf_init)))) m.
simpl.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_INIT.
Section CONS_BUF_READ.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_READ_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_read_body_correct1: ∀ m d env le rpos wpos,
env = PTree.empty _ →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
Int.unsigned rpos = Int.unsigned wpos →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_read_body E0 le´ (m, d) (Out_return (Some (Vint (Int.zero), tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold cons_buf_read_body.
esplit.
repeat vcgen.
Qed.
Lemma cons_buf_read_body_correct2: ∀ m m´ d env le rpos wpos c,
env = PTree.empty _ →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
Int.unsigned rpos ≠ Int.unsigned wpos →
Mem.load Mint32 m bcons_buf_loc ((Int.unsigned rpos) × 4) = Some (Vint c) →
Mem.store Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint (Int.repr((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE))) = Some m´ →
0 ≤ Int.unsigned rpos < CONSOLE_BUFFER_SIZE →
∃ le´,
exec_stmt ge env le ((m, d): mem) cons_buf_read_body E0 le´ (m´, d) (Out_return (Some (Vint c, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_read_body.
esplit.
repeat vcgen.
Opaque Z.mul.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite Z.mul_comm.
assumption.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
change (512 × 4) with 2048 in H4.
rewrite H4.
reflexivity.
omega.
Qed.
End CONS_BUF_READ_Body.
Theorem cons_buf_read_correct:
spec_le (cons_buf_read ↦ cons_buf_read_concrete_spec_low) (〚cons_buf_read ↦ f_cons_buf_read 〛L).
Proof.
fbigstep_pre L.
fbigstep (cons_buf_read_body_correct1 (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_read)
(nil)
(create_undef_temps (fn_temps f_cons_buf_read)))) m´.
destruct H4.
fbigstep (cons_buf_read_body_correct2 (Genv.globalenv p) b0 H (fst m) (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_cons_buf_read)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_read)))) m.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_READ.
Section CONS_BUF_WRITE.
Let L: compatlayer (cdata RData) := cons_buf_LOC ↦ cons_buf_loc_type.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONS_BUF_WRITE_Body.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variable (ge: genv).
Variable bcons_buf_loc: block.
Hypothesis hbcons_buf_loc: Genv.find_symbol ge cons_buf_LOC = Some bcons_buf_loc.
Lemma cons_buf_write_body_correct1: ∀ m m0 m´ d env le rpos wpos wpos´ c,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
Mem.store Mint32 m bcons_buf_loc (Int.unsigned wpos × 4) (Vint c) = Some m0 →
wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Int.unsigned wpos´ ≠ Int.unsigned rpos →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_write_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_write_body.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 ≤ Int.max_unsigned).
{
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
}
repeat vcgen.
Opaque Z.mul.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite Z.mul_comm.
rewrite H3.
reflexivity.
omega.
simpl.
lift_unfold.
rewrite Int.unsigned_repr.
change (513 × 4) with 2052 in H1.
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
eassumption.
right.
right.
simpl.
omega.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
lift_unfold.
rewrite Int.unsigned_repr.
discharge_cmp.
change (513 × 4) with 2052 in H7.
rewrite H7.
reflexivity.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
rewrite (Mem.load_store_other _ _ _ _ _ _ H7).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H5.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
omega.
lift_unfold.
rewrite Int.unsigned_repr.
change (513 × 4) with 2052 in H7.
rewrite (Mem.load_store_same _ _ _ _ _ _ H7).
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
rewrite Int.unsigned_repr in H6.
repeat vcgen.
assumption.
repeat vcgen.
Qed.
Lemma cons_buf_write_body_correct2: ∀ m m0 m1 m´ d env le rpos wpos wpos´ rpos´ c,
env = PTree.empty _ →
PTree.get _c le = Some (Vint c) →
Mem.load Mint32 m bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) = Some (Vint wpos) →
0 ≤ Int.unsigned wpos < CONSOLE_BUFFER_SIZE →
Mem.store Mint32 m bcons_buf_loc (Int.unsigned wpos × 4) (Vint c) = Some m0 →
wpos´ = Int.repr ((Int.unsigned wpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.store Mint32 m0 bcons_buf_loc ((CONSOLE_BUFFER_SIZE + 1) × 4) (Vint wpos´) = Some m1 →
Mem.load Mint32 m bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) = Some (Vint rpos) →
Int.unsigned wpos´ = Int.unsigned rpos →
rpos´ = Int.repr ((Int.unsigned rpos + 1) mod CONSOLE_BUFFER_SIZE) →
Mem.store Mint32 m1 bcons_buf_loc (CONSOLE_BUFFER_SIZE × 4) (Vint rpos´) = Some m´ →
exec_stmt ge env le ((m, d): mem) cons_buf_write_body E0 le (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros.
subst.
unfold cons_buf_write_body.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 ≤ Int.max_unsigned).
{
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
}
Require Import TacticsForTesting.
Opaque align.
d3 vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
change (align 0 4) with 0.
discharge_cmp.
lift_unfold.
rewrite Z.mul_comm.
rewrite H3.
reflexivity.
eassumption.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
discharge_cmp.
Opaque Z.mul Z.add.
repeat vcgen.
change (align 0 4) with 0.
change (align (0 + 4 × 512) 4) with 2048.
change (align (2048 + 4) 4) with 2052.
lift_unfold.
rewrite Int.unsigned_repr; try omega.
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
eassumption.
right.
right.
simpl.
omega.
change (align (align (align 0 4 + 4 × Z.max 0 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
lift_unfold.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
change ((512 + 1) × 4) with 2052 in H5.
rewrite H5.
reflexivity.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
rewrite (Mem.load_store_other _ _ _ _ _ _ H5).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H6.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
lift_unfold.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
change ((512 + 1) × 4) with 2052 in H5.
rewrite (Mem.load_store_same _ _ _ _ _ _ H5).
reflexivity.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
change (align (align (align 0 4 + 4 × 512) 4 + 4) 4) with 2052.
omega.
repeat vcgen.
repeat vcgen.
rewrite Int.unsigned_repr in H7; try omega.
repeat vcgen.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
rewrite (Mem.load_store_other _ _ _ _ _ _ H5).
rewrite (Mem.load_store_other _ _ _ _ _ _ H3).
change (512 × 4) with 2048 in H6.
eassumption.
right.
right.
simpl.
omega.
right.
left.
simpl.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
lift_unfold.
change (align (align 0 4 + 4 × 512) 4) with 2048.
rewrite Int.unsigned_repr; try omega.
rewrite Z.add_0_l.
discharge_cmp.
change (512 × 4) with 2048 in H9.
rewrite H9.
reflexivity.
rewrite <- H7.
rewrite Int.unsigned_repr; try omega.
assert (0 ≤ (Int.unsigned wpos + 1) mod 512 < 512).
{
apply Z.mod_pos_bound.
omega.
}
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
change (align (align 0 4 + 4 × 512) 4) with 2048.
omega.
Qed.
End CONS_BUF_WRITE_Body.
Theorem cons_buf_write_correct:
spec_le (cons_buf_write ↦ cons_buf_write_concrete_spec_low) (〚cons_buf_write ↦ f_cons_buf_write 〛L).
Proof.
fbigstep_pre L. destruct H2, H6.
fbigstep (cons_buf_write_body_correct1 (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_write)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_write)))) m.
simpl.
destruct m´.
reflexivity.
destruct H2, H4, H8.
fbigstep (cons_buf_write_body_correct2 (Genv.globalenv p) b0 H (fst m) (fst m0) (fst m1) (fst m´) (snd m) (PTree.empty _)
(bind_parameter_temps´ (fn_params f_cons_buf_write)
(Vint c :: nil)
(create_undef_temps (fn_temps f_cons_buf_write)))) m.
simpl.
destruct m´.
reflexivity.
Qed.
End CONS_BUF_WRITE.
End WithPrimitives.
End MQTICKETLOCKCODE.