From b3358e4a85b9741b291cae4bf12e5e6dd072b28b Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Tue, 6 Aug 2024 15:22:57 -0700 Subject: [PATCH] ADDR_LIMIT alignment axiom --- coq/Proofs/Revocation.v | 115 +++++++++++++++++++++++++--------------- 1 file changed, 71 insertions(+), 44 deletions(-) diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v index 6a2ab84ea..cf26611ce 100644 --- a/coq/Proofs/Revocation.v +++ b/coq/Proofs/Revocation.v @@ -67,6 +67,10 @@ End AbstTagDefs. (* This is a Morello-specific requirement. *) Axiom pointer_sizeof_alignof: sizeof_pointer MorelloImpl.get = alignof_pointer MorelloImpl.get. +(* TODO: this should be moved to [AddressValue] module *) +Axiom ADDR_LIMIT_aligned: + AddressValue.ADDR_LIMIT mod (Z.of_nat (alignof_pointer MorelloImpl.get)) = 0. + (* TODO: move *) Section AddressValue_Lemmas. @@ -5457,7 +5461,7 @@ Module CheriMemoryImplWithProofs (* prove bytes unchanged *) subst bs. - clear - SP RSZ OUT Balign. + clear - RSZ SP OUT Balign. (* prep *) pose proof MorelloImpl.alignof_pointer_pos as AP. @@ -5477,7 +5481,7 @@ Module CheriMemoryImplWithProofs intros a IN. apply In_nth_error in IN. destruct IN as [off IN]. - assert(off < psize)%nat. + assert(off < psize)%nat as POFF. { cut(nth_error (list_init psize (fun i : nat => AddressValue.with_offset addr (Z.of_nat i))) off <> None). intros H0. @@ -5496,12 +5500,13 @@ Module CheriMemoryImplWithProofs clear s. unfold addr_ptr_aligned in Balign. - rewrite pointer_sizeof_alignof in H0. + rewrite pointer_sizeof_alignof in POFF. rewrite repeat_length in *. apply not_and in OUT;[|apply Z.le_decidable]. + pose proof ADDR_LIMIT_aligned as ALA. remember (alignof_pointer MorelloImpl.get) as palign; clear Heqpalign. pose proof (AddressValue.to_Z_in_bounds addr) as AB. pose proof (AddressValue.to_Z_in_bounds start) as SB. @@ -5520,44 +5525,56 @@ Module CheriMemoryImplWithProofs unfold AddressValue.with_offset. unfold align_down in *. rewrite AddressValue.of_Z_roundtrip. - remember (AddressValue.to_Z addr) as zaddr;clear Heqzaddr addr. - remember (AddressValue.to_Z start) as zstart; clear Heqzstart. - - (* Do not need size in this branch *) - clear RSZ szn SP. - - pose proof (Z.mod_pos_bound zstart (Z.of_nat palign)). - autospecialize H1. lia. - unfold AddressValue.ADDR_MIN in *. - zify. - clear cstr. (* overlaps with AP *) - remember (Z.of_nat palign) as zalign; clear palign Heqzalign. - remember (Z.of_nat off) as zoff; clear off Heqzoff. - - remember (zstart - (zstart mod zalign)) as lzstart. - assert(lzstart mod zalign = 0). - { - subst. - apply align_bottom_correct, AP. - } + ++ + remember (AddressValue.to_Z addr) as zaddr;clear Heqzaddr addr. + remember (AddressValue.to_Z start) as zstart; clear Heqzstart. + + pose proof (Z.mod_pos_bound zstart (Z.of_nat palign)). + autospecialize H0. lia. + unfold AddressValue.ADDR_MIN in *. + zify. + clear cstr. (* overlaps with AP *) + remember (Z.of_nat palign) as zalign; clear palign Heqzalign. + remember (Z.of_nat off) as zoff; clear off Heqzoff. + + remember (zstart - (zstart mod zalign)) as lzstart. + assert(lzstart mod zalign = 0). + { + subst. + apply align_bottom_correct, AP. + } - (* zaddr - aligned. + (* zaddr - aligned. lzstart - aligned zaddr < lzstart - *) - assert(lzstart - zaddr >= zalign). - { + *) + assert(lzstart - zaddr >= zalign). + { + apply Zdiv.Zmod_divides in Balign; [|lia]. + destruct Balign as [naddr Balign]. + apply Zdiv.Zmod_divides in H1; [|lia]. + destruct H1 as [nstart H1]. + clear Heqlzstart. + subst. + apply Z.mul_lt_mono_pos_l in H;[|lia]. + nia. + } + nia. + ++ + split;[lia|]. apply Zdiv.Zmod_divides in Balign; [|lia]. destruct Balign as [naddr Balign]. - apply Zdiv.Zmod_divides in H2; [|lia]. - destruct H2 as [nstart H2]. - clear Heqlzstart. - subst. - apply Z.mul_lt_mono_pos_l in H;[|lia]. + apply Zdiv.Zmod_divides in ALA; [|lia]. + destruct ALA as [nmax ALA]. + rewrite Balign,ALA. + + cut(naddr