Proof of cap_is_valid_bv_extract_bool and new auxiliary lemmas

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 ] 
  ].
  }