From da69ac4aa288cc3551583e46d869c1ed25683b5f Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Wed, 25 Sep 2024 11:49:48 +0100 Subject: [PATCH] Proof of cap_is_valid_bv_extract_bool and new auxiliary lemmas --- theories/Morello/Capabilities.v | 53 ++++++++++++++++++++++++++++----- 1 file changed, 45 insertions(+), 8 deletions(-) diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index fb96123..a370b3e 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -1479,12 +1479,41 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true. Admitted. - Lemma cap_is_valid_bv c : - cap_is_valid c = ((@bv_extract 129 128 1 c) =? 1)%bv. - Admitted. + Lemma cap_is_valid_bv_extract c : + cap_is_valid c ↔ bv_extract 128 1 c = (BV 1 1). + Proof. + split. + + intro H. apply cap_is_valid_bv_and in H. + unfold t, len in *. bv_simplify. bv_simplify H. + bitblast as n. replace n with 0%Z; [| lia ]. + assert (P: Z.testbit (bv_unsigned c) 128 = Z.testbit (Z.land (bv_unsigned c) (2 ^ 128)) 128); [ bitblast |]. + rewrite P. rewrite H. bitblast. + + intro H. unfold cap_is_valid, CapIsTagClear, CapGetTag. + unfold_cap. unfold t, len in *. unfold MachineWord.N_to_word, CAP_TAG_BIT. unfold_cap. + case_decide as P; try done. simpl. + assert (Q: vec_of_bits [@access_vec_dec 64 (bv_zero_extend 64 (vec_of_bits [@access_vec_dec 129 c 128])) 0] = Z_to_bv 1 1). + { unfold access_vec_dec, access_mword_dec, MachineWord.get_bit, bitU_of_bool, vec_of_bits, get_word, of_bools, bools_to_mword, MachineWord.bools_to_word, MachineWord.N_to_word; case_match; try done; case_match eqn:H1; try done; simpl. + bv_simplify H. change (autocast _) with (Z_to_bv 1 0). + apply bv_eq. rewrite !Z_to_bv_unsigned. simpl. + bitblast as n. bitblast H with n as H2. + rewrite <- H1, <- H2. replace n with 0%Z; [| lia ]. done. } + by rewrite P in Q. + Qed. + Lemma cap_is_valid_bv_extract_bool c : + cap_is_valid c = (bv_extract 128 1 c =? 1)%bv. + Proof. + destruct (cap_is_valid c) eqn:E. + + apply Is_true_true_2 in E. + apply cap_is_valid_bv_extract in E. rewrite E. done. + + assert (bv_extract 128 1 c ≠ (BV 1 1)). + { intro H. apply cap_is_valid_bv_extract in H. rewrite E in H. contradiction. } + symmetry. apply Z.eqb_neq. by apply bv_neq. + Qed. + Lemma bits_of_vec_hd h l : bits_of (vec_of_bits (h::l)) = bits_of ((concat_vec (vec_of_bits [h]) (vec_of_bits l))). + Proof. Admitted. Lemma hd_bits_of_vec h l : @@ -1519,11 +1548,19 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou byte_chunks l = Some l' → try_map memory_byte_to_ascii (rev l') = Some l'' → map bitU_of_bool (bool_bits_of_bytes (rev l'')) = l. + Proof. Admitted. - Lemma mword_to_bools_split (c: bv 129) : - @mword_to_bools 129 c = (((@bv_extract 129 128 1 c =? 1)) :: (@mword_to_bools 128 (@bv_extract 129 0 128 c)))%list. + Lemma bv_to_bits_app_last (c : bv 129) : + bv_to_bits c = (bv_to_bits (bv_extract 0 128 c) ++ [bv_extract 128 1 c =? 1])%list. Admitted. + + Lemma mword_to_bools_cons_last (c: bv 129) : + @mword_to_bools 129 c = (((bv_extract 128 1 c =? 1)) :: (@mword_to_bools 128 (bv_extract 0 128 c)))%list. + Proof. + unfold mword_to_bools, MachineWord.word_to_bools; simpl. + rewrite <- rev_unit. apply f_equal. by rewrite bv_to_bits_app_last. + Qed. Lemma cap_encode_decode: ∀ cap bytes t, @@ -1547,18 +1584,18 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou { unfold bv_to_bv, bv_to_Z_unsigned. by rewrite Z_to_bv_bv_unsigned. } { rewrite Z_to_bv_checked_bv_unsigned. apply f_equal. unfold vec, bv_to_bv, bv_to_Z_unsigned. - rewrite cap_is_valid_bv. + rewrite cap_is_valid_bv_extract_bool. destruct (bv_extract 128 1 c =? 1) eqn:H_c_valid; simpl; [ replace B1 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| by rewrite H_c_valid ] | replace B0 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| by rewrite H_c_valid ]]. all: unfold bits_of; - have -> : @mword_to_bools 129 c = (bv_extract 128 1 c =? 1) :: @mword_to_bools 128 (bv_extract 0 128 c); [ by rewrite mword_to_bools_split |]; + have -> : @mword_to_bools 129 c = (bv_extract 128 1 c =? 1) :: @mword_to_bools 128 (bv_extract 0 128 c); [ by rewrite mword_to_bools_cons_last |]; rewrite map_cons; simpl; have -> : vec_of_bits (bitU_of_bool (bv_extract 128 1 c =? 1) :: map bitU_of_bool (@mword_to_bools 128 (bv_extract 0 128 c))) = (vec_of_bits (map bitU_of_bool ((bv_extract 128 1 c =? 1) :: @mword_to_bools 128 (bv_extract 0 128 c)))); [ unfold vec_of_bits; apply f_equal; by rewrite map_cons | have -> : bv_unsigned (vec_of_bits (map bitU_of_bool ((@bv_extract 129 128 1 c =? 1) :: @mword_to_bools 128 (@bv_extract 129 0 128 c)))) = bv_unsigned (vec_of_bits (map bitU_of_bool (@mword_to_bools 129 c))); [ change (N.of_nat (Pos.to_nat (Pos.of_succ_nat _ ))) with 129%N; - apply f_equal; unfold vec_of_bits; apply f_equal; by rewrite <- mword_to_bools_split + apply f_equal; unfold vec_of_bits; apply f_equal; by rewrite <- mword_to_bools_cons_last | fold (@bits_of 129 c); rewrite cap_to_bits_to_cap; by rewrite Z_to_bv_bv_unsigned ] ]. }