From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- kvx/Stacklayout.v | 51 ++++++++++++++++++++++++++------------------------- 1 file changed, 26 insertions(+), 25 deletions(-) (limited to 'kvx/Stacklayout.v') diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 81ffcebb..05cfa1d7 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -18,6 +18,7 @@ Require Import Coqlib. Require Import AST Memory Separation. Require Import Bounds. +Require Import Lia. Local Open Scope sep_scope. @@ -71,15 +72,15 @@ Local Opaque Z.add Z.mul sepconj range. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -92,11 +93,11 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + apply range_split_2. fold olink; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -112,16 +113,16 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -140,11 +141,11 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). split. apply Z.divide_0_r. - split. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl. Qed. -- cgit