Skip to content

Commit

Permalink
Proof of to_ubytes_fin_inf.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Chobbes
Chobbes committed Jun 5, 2023
1 parent deb13f1 commit cf2b6e7
Showing 1 changed file with 207 additions and 12 deletions.
219 changes: 207 additions & 12 deletions src/coq/Semantics/InfiniteToFinite.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10371,6 +10371,11 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF

exists (lift_MemState ms_fin_final).

assert (Heap_in_bounds ms_fin_final) as HIB_FINAL.
{
admit. (* TODO: Heap_in_bounds *)
}

split.
2: apply lift_MemState_refine_prop.

Expand Down Expand Up @@ -10405,7 +10410,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
eapply ptr_in_memstate_heap_inf_fin in H; eauto.
apply free_bytes_freed in H.
eapply fin_inf_byte_not_allocated in H; eauto.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
}

{ (* Big pointer, shouldn't be allocated. *)
Expand All @@ -10425,7 +10430,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
{ (* ptr in finite range *)
split; intros ALLOC.
- eapply fin_inf_byte_allocated; eauto.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
apply free_non_block_bytes_preserved.
+ intros CONTRA.
eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto.
Expand All @@ -10435,7 +10440,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
+ intros CONTRA.
eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto.
+ eapply inf_fin_byte_allocated; eauto.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
}

{ (* Big pointer, shouldn't be allocated. *)
Expand All @@ -10446,7 +10451,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
- eapply inf_fin_byte_allocated_exists in ALLOC; eauto.
destruct ALLOC as (?&?&?).
rewrite CONV in H0; discriminate.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
}
}
- intros ptr byte H.
Expand All @@ -10460,8 +10465,8 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
eapply ptr_in_memstate_heap_fin_inf in CONTRA; eauto.
}
eapply fin_inf_read_byte_spec; eauto.
apply lift_MemState_refine_prop.
- pose proof (lift_MemState_refine_prop ms_fin_final) as MSR'.
apply lift_MemState_refine_prop; auto.
- pose proof (lift_MemState_refine_prop ms_fin_final HIB_FINAL) as MSR'.
epose proof inf_fin_read_byte_spec MSR' CONV RBS as (byte_fin&RBS_FIN&BYTE_REF).
eapply free_non_frame_bytes_read in RBS_FIN.
2: {
Expand All @@ -10481,7 +10486,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
destruct ALLOC as (?&?&?&?&?).
red in H2.
rewrite CONV in H2; discriminate.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
}
}
- clear - PTR_REF MSR free_block.
Expand Down Expand Up @@ -10517,14 +10522,14 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
auto.
}
- (* Free operation invariants *)
clear - MSR free_invariants.
clear - HIB_FINAL MSR free_invariants.
destruct free_invariants.
split.
+ eapply fin_inf_preserve_allocation_ids; eauto.
apply lift_MemState_refine_prop.
apply lift_MemState_refine_prop; auto.
+ eapply fin_inf_frame_stack_preserved; eauto.
apply lift_MemState_refine_prop.
Qed.
apply lift_MemState_refine_prop; auto.
Admitted.

Lemma handle_free_fin_inf :
forall {ms_fin_start ms_fin_final ms_inf_start res_fin args_fin args_inf},
Expand Down Expand Up @@ -10586,6 +10591,7 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
{ (* MA *)
intros a_fin ms_fin_ma MEMCPY.
eapply handle_memcpy_fin_inf; eauto.
admit. (* TODO: Heap_in_bounds *)
}

intros ms_inf0 ms_fin0 ms_fin'0 a_fin a_inf b_fin _ MSR' EQV.
Expand Down Expand Up @@ -10648,6 +10654,107 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
(* Unknown intrinsic *)
cbn in *; auto.
contradiction.
Admitted.

Lemma to_ubytes_fin_inf_helper :
forall {uv_fin uv_inf t sid bytes_fin start},
DVC1.uvalue_refine_strict uv_inf uv_fin ->
map_monad
(fun n : N =>
n' <- LLVMParams64BitIntptr.IP.from_Z (Z.of_N n);;
ret
(Memory64BitIntptr.MP.BYTE_IMPL.uvalue_sbyte uv_fin t
(LLVMParams64BitIntptr.Events.DV.UVALUE_IPTR n') sid))
(Nseq start (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t))) =
NoOom bytes_fin ->
map_monad
(fun n : N =>
n' <- LLVMParamsBigIntptr.IP.from_Z (Z.of_N n);;
ret
(MemoryBigIntptr.MP.BYTE_IMPL.uvalue_sbyte uv_inf t
(LLVMParamsBigIntptr.Events.DV.UVALUE_IPTR n') sid))
(Nseq start (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t))) = NoOom (map lift_SByte bytes_fin).
Proof.
intros uv_fin uv_inf t sid bytes_fin start UV_REF UBYTES.
generalize dependent bytes_fin.
generalize dependent start.
induction (N.to_nat (FiniteSizeof.FinSizeof.sizeof_dtyp t));
intros start bytes_fin UBYTES.
- cbn in *.
inv UBYTES.
cbn.
reflexivity.
- rewrite <- cons_Nseq.
rewrite <- cons_Nseq in UBYTES.

rewrite map_monad_unfold.
rewrite map_monad_unfold in UBYTES.

cbn.
cbn in UBYTES.

break_match_hyp; inv UBYTES.
break_match_hyp; inv H0.
break_match_hyp; inv Heqo.

apply IHn in Heqo0.
cbn in Heqo0.
rewrite Heqo0.
cbn.
unfold MemoryBigIntptr.MP.BYTE_IMPL.uvalue_sbyte.
erewrite <- fin_to_inf_uvalue_refine_strict'; eauto.
erewrite <- fin_to_inf_uvalue_refine_strict'; eauto.

rewrite DVC1.uvalue_refine_strict_equation.
rewrite DVC1.uvalue_convert_strict_equation.
cbn.

erewrite FinToInfIntptrConvertSafe.intptr_convert_safe; eauto.
cbn.
erewrite IP64Bit.from_Z_to_Z; eauto.
Qed.

(* TODO: move this *)
Definition lift_SBytes := map lift_SByte.

Lemma lift_SBytes_refine :
forall {bytes_fin},
sbytes_refine (lift_SBytes bytes_fin) bytes_fin.
Proof.
induction bytes_fin; cbn.
- constructor.
- constructor.
apply sbyte_refine_lifted.
apply IHbytes_fin.
Qed.

(* TODO: should we know that uv_inf / uv_fin has type t?

I think this would have to be an assumption, in theory the front
end would guarantee this for stores with a syntactic check.
*)
Lemma to_ubytes_fin_inf :
forall {uv_fin uv_inf t sid bytes_fin},
DVC1.uvalue_refine_strict uv_inf uv_fin ->
Memory64BitIntptr.MMEP.MMSP.MemByte.to_ubytes uv_fin t sid = NoOom bytes_fin ->
exists bytes_inf,
MemoryBigIntptr.MMEP.MMSP.MemByte.to_ubytes uv_inf t sid = NoOom bytes_inf /\
sbytes_refine bytes_inf bytes_fin.
Proof.
intros uv_fin uv_inf t sid bytes_fin UV_REF UBYTES.
exists (map lift_SByte bytes_fin).
split.
2: {
apply lift_SBytes_refine.
}

unfold MemoryBigIntptr.MMEP.MMSP.MemByte.to_ubytes,
Memory64BitIntptr.MMEP.MMSP.MemByte.to_ubytes in *.

unfold LLVMParams64BitIntptr.SIZEOF.sizeof_dtyp,
LLVMParamsBigIntptr.SIZEOF.sizeof_dtyp in *.

eapply to_ubytes_fin_inf_helper; eauto.
Qed.

(* TODO: Prove this *)
Expand All @@ -10665,7 +10772,95 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
MemState_refine_prop ms_inf_final ms_fin_final.
Proof.
intros ms_fin_start ms_fin_final ms_inf_start uv_fin uv_inf t bytes_fin MSR UV_REF SERIALIZE.
Admitted.

rewrite Memory64BitIntptr.MMEP.MemSpec.MemHelpers.serialize_sbytes_equation in SERIALIZE.
rewrite MemoryBigIntptr.MMEP.MemSpec.MemHelpers.serialize_sbytes_equation.

induction uv_inf.
- pose proof UV_REF as UV_REF'.
rewrite DVC1.uvalue_refine_strict_equation in UV_REF.
rewrite DVC1.uvalue_convert_strict_equation in UV_REF.
cbn in UV_REF.
move UV_REF after SERIALIZE.
break_match_hyp; inv UV_REF.

eapply MemPropT_fin_inf_bind.
4: apply SERIALIZE.
all: eauto.

{ (* MA: fresh_sid *)
intros a_fin ms_fin_ma FRESH.
eapply fresh_sid_fin_inf; eauto.
}

intros ms_inf ms_fin ms_fin' a_fin a_inf b_fin SID MSR_SID UBYTES.
cbn in SID, UBYTES; subst.

red in UBYTES.
break_match_hyp; inv UBYTES.


eapply to_ubytes_fin_inf in Heqo0; eauto.
destruct Heqo0 as (?&?&?).
exists x. exists ms_inf.
split; auto.
red.
rewrite H.
cbn. auto.


try
solve
[ rewrite DVC1.dvalue_refine_strict_equation in UV_REF;
first
[ apply dvalue_convert_strict_i1_inv in UV_REF
| apply dvalue_convert_strict_i8_inv in UV_REF
| apply dvalue_convert_strict_i32_inv in UV_REF
| apply dvalue_convert_strict_i64_inv in UV_REF
| apply dvalue_convert_strict_iptr_inv in UV_REF
| apply dvalue_convert_strict_addr_inv in UV_REF
| apply dvalue_convert_strict_double_inv in UV_REF
| apply dvalue_convert_strict_float_inv in UV_REF
| apply dvalue_convert_strict_poison_inv in UV_REF
| apply dvalue_convert_strict_oom_inv in UV_REF
| apply dvalue_convert_strict_none_inv in UV_REF
| apply dvalue_convert_strict_struct_inv in UV_REF
| apply dvalue_convert_strict_packed_struct_inv in UV_REF
| apply dvalue_convert_strict_array_inv in UV_REF
| apply dvalue_convert_strict_vector_inv in UV_REF
];
first
[ destruct ADDR_REF as (?&?&?); subst
| inv ADDR_REF
]
].

rewrite DVC1.uvalue_refine_strict_equation in UV_REF.
apply uvalue_convert_strict_addr_inv in UV_REF.
first
[ apply uvalue_convert_strict_i1_inv in UV_REF
| apply uvalue_convert_strict_i8_inv in UV_REF
| apply uvalue_convert_strict_i32_inv in UV_REF
| apply uvalue_convert_strict_i64_inv in UV_REF
| apply uvalue_convert_strict_iptr_inv in UV_REF
| apply uvalue_convert_strict_addr_inv in UV_REF
| apply uvalue_convert_strict_double_inv in UV_REF
| apply uvalue_convert_strict_float_inv in UV_REF
| apply uvalue_convert_strict_poison_inv in UV_REF
| apply uvalue_convert_strict_oom_inv in UV_REF
| apply uvalue_convert_strict_none_inv in UV_REF
| apply uvalue_convert_strict_struct_inv in UV_REF
| apply uvalue_convert_strict_packed_struct_inv in UV_REF
| apply uvalue_convert_strict_array_inv in UV_REF
| apply uvalue_convert_strict_vector_inv in UV_REF
];
first
[ destruct ADDR_REF as (?&?&?); subst
| inv ADDR_REF
].


Qed.

Lemma handle_store_fin_inf :
forall {t addr_fin addr_inf uv_fin uv_inf ms_fin_start ms_fin_final ms_inf_start res_fin},
Expand Down

0 comments on commit cf2b6e7

Please sign in to comment.