🚥 Bitset.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bitset.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bitset.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
We require a bitset to be a non-negative number.
The encoding for bitset values is valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Bitset.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
The empty bitset is valid (non-negative).
A bitset value is still valid after adding a bit.
Lemma add_is_valid (x : Bitset.t) (position : int) :
Valid.t x →
0 ≤ position →
match Bitset.add x position with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ False
end.
Proof.
intros x_valid pos_nneg.
unfold Valid.t in ×.
unfold Bitset.add.
unfold "<i"; simpl.
rewrite <- Z.ltb_ge in pos_nneg.
rewrite pos_nneg; simpl.
unfold logor, shift_left, one.
rewrite Z.lor_nonneg; split; auto.
rewrite Z.shiftl_nonneg; lia.
Qed.
Valid.t x →
0 ≤ position →
match Bitset.add x position with
| Pervasives.Ok y ⇒ Valid.t y
| Pervasives.Error _ ⇒ False
end.
Proof.
intros x_valid pos_nneg.
unfold Valid.t in ×.
unfold Bitset.add.
unfold "<i"; simpl.
rewrite <- Z.ltb_ge in pos_nneg.
rewrite pos_nneg; simpl.
unfold logor, shift_left, one.
rewrite Z.lor_nonneg; split; auto.
rewrite Z.shiftl_nonneg; lia.
Qed.
The membership in an empty bitset is always [false].
Lemma mem_empty_eq (position : int) :
0 ≤ position →
Bitset.mem Bitset.empty position = return? false.
Proof.
intros.
unfold Bitset.mem, Error_monad.error_when.
step; simpl; [lia|].
now destruct position.
Qed.
0 ≤ position →
Bitset.mem Bitset.empty position = return? false.
Proof.
intros.
unfold Bitset.mem, Error_monad.error_when.
step; simpl; [lia|].
now destruct position.
Qed.
The membership in a bitset with an added bit.
Lemma mem_add_eq (x : Bitset.t) (position_add position_mem : int) :
Valid.t x →
0 ≤ position_add → 0 ≤ position_mem →
(let? y := Bitset.add x position_add in
Bitset.mem y position_mem) =
(if position_mem =? position_add then
return? true
else
Bitset.mem x position_mem).
Proof.
intros x_valid pos_add_nneg pos_mem_nneg.
unfold Bitset.add, Bitset.mem.
unfold "<i"; simpl.
assert (position_add <? 0 = false) as Hadd by (apply Z.ltb_ge; auto).
assert (position_mem <? 0 = false) as Hmem by (apply Z.ltb_ge; auto).
rewrite Hadd, Hmem; simpl.
unfold testbit.
unfold logor, shift_left, one.
destruct Z.eqb eqn:mem_add_eq; f_equal; rewrite Z.lor_spec.
{ rewrite Z.eqb_eq in mem_add_eq.
rewrite mem_add_eq.
rewrite Z.shiftl_spec; auto.
rewrite Z.sub_diag; simpl.
apply Bool.orb_true_r.
}
{ rewrite Z.eqb_neq in mem_add_eq.
rewrite Z.shiftl_spec; auto.
destruct (Ztrichotomy position_mem position_add)
as [Hlt|[Heq|Hgt]]; try contradiction.
{ rewrite (Z.testbit_neg_r _ (position_mem - position_add)); try lia.
apply Bool.orb_false_r.
}
{ destruct (position_mem - position_add) eqn:?; try lia.
simpl; apply Bool.orb_false_r.
}
}
Qed.
Valid.t x →
0 ≤ position_add → 0 ≤ position_mem →
(let? y := Bitset.add x position_add in
Bitset.mem y position_mem) =
(if position_mem =? position_add then
return? true
else
Bitset.mem x position_mem).
Proof.
intros x_valid pos_add_nneg pos_mem_nneg.
unfold Bitset.add, Bitset.mem.
unfold "<i"; simpl.
assert (position_add <? 0 = false) as Hadd by (apply Z.ltb_ge; auto).
assert (position_mem <? 0 = false) as Hmem by (apply Z.ltb_ge; auto).
rewrite Hadd, Hmem; simpl.
unfold testbit.
unfold logor, shift_left, one.
destruct Z.eqb eqn:mem_add_eq; f_equal; rewrite Z.lor_spec.
{ rewrite Z.eqb_eq in mem_add_eq.
rewrite mem_add_eq.
rewrite Z.shiftl_spec; auto.
rewrite Z.sub_diag; simpl.
apply Bool.orb_true_r.
}
{ rewrite Z.eqb_neq in mem_add_eq.
rewrite Z.shiftl_spec; auto.
destruct (Ztrichotomy position_mem position_add)
as [Hlt|[Heq|Hgt]]; try contradiction.
{ rewrite (Z.testbit_neg_r _ (position_mem - position_add)); try lia.
apply Bool.orb_false_r.
}
{ destruct (position_mem - position_add) eqn:?; try lia.
simpl; apply Bool.orb_false_r.
}
}
Qed.
The function [occupied_size_in_bits] is valid.
Lemma occupied_size_in_bits_is_valid (x : Bitset.t) :
Pervasives.Int.Valid.non_negative (Bitset.occupied_size_in_bits x).
Proof.
apply Z.numbits_is_valid.
Qed.
Pervasives.Int.Valid.non_negative (Bitset.occupied_size_in_bits x).
Proof.
apply Z.numbits_is_valid.
Qed.