Skip to main content

🚥 Bitset.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Bitset.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.

We require a bitset to be a non-negative number.
Module Valid.
  Definition t (x : Bitset.t) : Prop :=
    0 x.
End Valid.

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.

The empty bitset is valid (non-negative).
Lemma empty_is_valid : Valid.t Bitset.empty.
Proof.
  easy.
Qed.

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 yValid.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.

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.