Skip to main content

🍲 Dal_attestation_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Proto_alpha.Dal_attestation_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Proofs.Bitset.

Validity predicate for [Dal_attestation_repr.t].
Module Valid.
  Definition t (s : Dal_attestation_repr.t) : Prop :=
    Bitset.Valid.t s.
End Valid.

The encoding [encoding] is valid.
Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True)
  Dal_attestation_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[commit] produces a valid bitset from a valid bitset.
Lemma commit_is_valid (bitset : Dal_attestation_repr.t) (i : int) :
  0 i Valid.t bitset
  Valid.t (Dal_attestation_repr.commit bitset i).
Proof.
  intros i_nneg Hvalid.
  unfold Valid.t in ×.
  unfold Dal_attestation_repr.commit, Dal_slot_repr.Index.to_int.
  destruct Bitset.add eqn:Hadd; auto.
  pose proof (Bitset.add_is_valid bitset i Hvalid i_nneg) as pf.
  rewrite Hadd in pf; auto.
Qed.

Positive indices are not attested in the empty bitset.
Lemma is_attested_empty_false (i : int) : 0 i
  Dal_attestation_repr.is_attested Dal_attestation_repr.empty i = false.
Proof.
  intro i_nneg.
  unfold Dal_attestation_repr.is_attested.
  rewrite Bitset.mem_empty_eq; auto.
Qed.

A bit which was just committed is attested.
Lemma is_attested_commit_eq (bitset : Dal_attestation_repr.t) (i : int) :
  Valid.t bitset 0 i
  Dal_attestation_repr.is_attested
    (Dal_attestation_repr.commit bitset i) i = true.
Proof.
  intros Hvalid i_nneg.
  unfold
    Dal_attestation_repr.is_attested,
    Dal_attestation_repr.commit,
    Dal_slot_repr.Index.to_int.
  destruct Bitset.add eqn:Hadd.
  { pose proof (Bitset.mem_add_eq bitset i i Hvalid i_nneg i_nneg) as pf.
    rewrite Hadd in pf; simpl in pf.
    rewrite pf.
    rewrite Z.eqb_refl; reflexivity.
  }
  { unfold Bitset.add in Hadd.
    unfold error_when in Hadd.
    unfold Int.op_lt in Hadd; simpl in Hadd.
    rewrite <- Z.ltb_ge in i_nneg.
    rewrite i_nneg in Hadd; inversion Hadd.
  }
Qed.

The availability of indices other than the commit index remains unchanged.
Lemma is_attested_commit_neq (bitset : Dal_attestation_repr.t) (i j : int) :
  Valid.t bitset 0 i 0 j j i
  Dal_attestation_repr.is_attested (Dal_attestation_repr.commit bitset i) j =
  Dal_attestation_repr.is_attested bitset j.
Proof.
  intros Hvalid i_nneg j_nneg ji_neq.
  unfold
    Dal_attestation_repr.is_attested,
    Dal_attestation_repr.commit,
    Dal_slot_repr.Index.to_int.
  destruct Bitset.add eqn:Hadd.
  { pose proof (Bitset.mem_add_eq bitset i j Hvalid i_nneg j_nneg) as pf.
    rewrite Hadd in pf; simpl in pf.
    rewrite pf.
    rewrite <- Z.eqb_neq in ji_neq.
    rewrite ji_neq.
    reflexivity.
  }
  { unfold Bitset.add in Hadd.
    unfold error_when in Hadd.
    unfold Int.op_lt in Hadd; simpl in Hadd.
    rewrite <- Z.ltb_ge in i_nneg.
    rewrite i_nneg in Hadd; inversion Hadd.
  }
Qed.

If an index is available after commit, then either it was just committed or was previously available.
Lemma is_available_commit_inversion
  (bitset : Dal_attestation_repr.t) (i j : int)
  : Valid.t bitset Dal_attestation_repr.is_attested
      (Dal_attestation_repr.commit bitset i) j = true
    i = j Dal_attestation_repr.is_attested bitset j = true.
Proof.
  unfold
    Dal_attestation_repr.is_attested,
    Dal_attestation_repr.commit,
    Dal_slot_repr.Index.to_int.
  destruct (Bitset.add bitset i) eqn:Hadd; auto.
  intros Hvalid Hij.
  destruct (Bitset.mem t j) eqn:Hmem; auto.
  rewrite Hij in Hmem.
  assert (0 i) as i_nneg.
  { unfold Bitset.add in Hadd.
    destruct (i <i 0) eqn:?; [sauto|lia].
  }
  assert (0 j) as j_nneg.
  { unfold Bitset.mem in Hmem.
    destruct (j <i 0) eqn:?; [sauto|lia].
  }
  pose proof
    (Bitset.mem_add_eq bitset i j Hvalid i_nneg j_nneg) as pf.
  rewrite Hadd in pf; simpl in pf.
  destruct (j =? i) eqn:?; [lia|sauto].
Qed.

Module shard_index.
  Module Valid.
Validity predicate for the type [shard_index].
    Definition t (x : Dal_attestation_repr.shard_index) : Prop :=
      Pervasives.Int.Valid.non_negative x.
  End Valid.
End shard_index.

Module Accountability.
  Module Valid.
Validity predicate for the type [t].
    Definition t (x : Dal_attestation_repr.Accountability.t) : Prop :=
      List.Forall Bitset.Valid.t x.
  End Valid.

init_value len = [0;...;0].
  Lemma init_value_repeat_empty (len : int) (bitset : Dal_attestation_repr.t) :
    0 len Dal_attestation_repr.Accountability.init_value len =
    List.repeat Dal_attestation_repr.empty (Z.to_nat len).
  Proof.
    intros len_nneg.
    destruct len; [reflexivity | | lia].
    unfold Dal_attestation_repr.Accountability.init_value; simpl.
    generalize (Pos.to_nat p).
    induction n; sauto.
  Qed.

  Lemma rssa_commit (bitset : Dal_attestation_repr.t) (shards : list int) :
    Dal_attestation_repr.Accountability.record_slot_shard_availability
      bitset shards =
    List.fold_left Dal_attestation_repr.commit bitset shards.
  Proof.
    induction shards; lia.
  Qed.

An index remains available after applying [record_slot_shard_availability].
  Lemma rssa_is_available_still_available (bitset : Dal_attestation_repr.t)
    (shards : list int) (i : int) :
    Bitset.Valid.t bitset Forall (Z.le 0) shards
    Dal_attestation_repr.is_attested bitset i = true
    Dal_attestation_repr.is_attested
      (Dal_attestation_repr.Accountability.record_slot_shard_availability
      bitset shards) i = true.
  Proof.
    rewrite rssa_commit.
    generalize i; clear i.
    generalize bitset; clear bitset.
    induction shards as [|j shards IH]; [sauto|].
    intros bitset i Hvalid shards_nneg Hi.
    assert (0 i).
    { unfold
        Dal_attestation_repr.is_attested,
        Bitset.mem,
        Dal_slot_repr.Index.to_int
        in Hi.
      cbn in ×.
      destruct (i <? 0) eqn:?.
      { cbn in ×. discriminate. }
      { lia. }
    }
    simpl.
    inversion shards_nneg.
    apply IH; auto.
    { apply commit_is_valid; auto. }
    destruct (BinInt.Z.eq_dec j i) as [ji_eq|ji_neq].
    { rewrite ji_eq.
      apply is_attested_commit_eq; auto.
    }
    { rewrite is_attested_commit_neq; auto. }
  Qed.

If all shards are non-negative, then each shard is available after applying [record_slot_shard_availability].
  Lemma rssa_In_shards_is_available (bitset : Dal_attestation_repr.t)
    (shards : list int) (i : int) :
    Bitset.Valid.t bitset Forall (Z.le 0) shards
    In i shards
    Dal_attestation_repr.is_attested
      (Dal_attestation_repr.Accountability.record_slot_shard_availability
      bitset shards) i = true.
  Proof.
    rewrite rssa_commit.
    generalize i; clear i.
    generalize bitset; clear bitset.
    induction shards as [|j shards IH]; [sauto|].
    intros bitset i Hvalid shards_nneg Hin; simpl.
    inversion shards_nneg.
    destruct Hin as [ji_eq|Hin].
    { apply rssa_is_available_still_available; auto.
      { apply commit_is_valid; auto. }
      { rewrite <- ji_eq.
        apply is_attested_commit_eq; auto.
      }
    }
    { apply IH; auto.
      apply commit_is_valid; auto.
    }
  Qed.

If an index is available after applying [record_slot_shard_availability], then it either was already available or belongs to the shards.
  Lemma rssa_is_available_inversion (bitset : Dal_attestation_repr.t)
    (shards : list int) (i : int) :
    Forall (Z.le 0) shards
    Bitset.Valid.t bitset 0 i
    Dal_attestation_repr.is_attested
      (Dal_attestation_repr.Accountability.record_slot_shard_availability
      bitset shards) i = true
    Dal_attestation_repr.is_attested bitset i = true In i shards.
  Proof.
    rewrite rssa_commit.
    generalize i; clear i.
    generalize bitset; clear bitset.
    induction shards as [|j shards IH]; [sauto|].
    intros bitset i shards_nneg Hvalid i_nneg Hi.
    simpl in Hi.
    inversion shards_nneg as [|? ? j_nneg shards_nneg'].
    destruct (IH _ _ shards_nneg'
      (commit_is_valid _ _ j_nneg Hvalid) i_nneg Hi) as [Hji|]; [|sauto].
    destruct (is_available_commit_inversion _ _ _ Hvalid Hji); sauto.
  Qed.

The function [record_shards_availability] is valid.
If the [i]th bitset of [shard_bitset_per_slot] is [bitset] but there is no [i]th bit in [slots], then the [i]th bitset after applying [record_shards_availability] is [bitset].
  Lemma rsa_In_error (shard_bitset_per_slot : list Dal_attestation_repr.t)
    (slots : Dal_attestation_repr.t) (shards : list int)
    (bitset : Dal_attestation_repr.t)
    (i : int) (e : trace _error) :
    List.nth shard_bitset_per_slot i = Some bitset
    Bitset.mem slots i = Pervasives.Error e
    List.nth (Dal_attestation_repr.Accountability.record_shards_availability
      shard_bitset_per_slot slots shards) i = Some bitset.
  Proof.
    intros Hnth Hmem.
    unfold Dal_attestation_repr.Accountability.record_shards_availability.
    rewrite (List.nth_mapi_Some _ _ _ _ Hnth).
    rewrite Hmem; reflexivity.
  Qed.

If the [i]th bitset of [shard_bitset_per_slot] is [bitset] and the [i]th bit in [slots] is [b], the [i]th bitset after applying [record_shards_availability] is the application of [record_slot_shard_availability] or the original [bitset], depending on [b].
  Lemma rsa_In_ok (shard_bitset_per_slot : list Dal_attestation_repr.t)
    (slots : Dal_attestation_repr.t) (shards : list int)
    (bitset : Dal_attestation_repr.t) (i : int) (b : bool) :
    List.nth shard_bitset_per_slot i = Some bitset
    Bitset.mem slots i = Pervasives.Ok b
    List.nth (Dal_attestation_repr.Accountability.record_shards_availability
      shard_bitset_per_slot slots shards) i =
      Some (if b
      then Dal_attestation_repr.Accountability.record_slot_shard_availability
        bitset shards
      else bitset).
  Proof.
    intros Hnth Hmem.
    unfold Dal_attestation_repr.Accountability.record_shards_availability.
    rewrite (List.nth_mapi_Some _ _ _ _ Hnth).
    rewrite Hmem; reflexivity.
  Qed.

If the [i]th bitset after applying [record_shards_availability] is [bitset], then either: a) [i] is out of bounds in [slots], in which case the [i]th bitset was already [bitset]. b) the [i]th bit of [slots] is false, in which case the [i]th bitset was already [bitset]. c) the [i]th bit of [slots] is true, in which case the [i]th bitset was some [bitset'] such that [record_slot_shard_availability bitset' shards = bitset].
  Lemma rsa_In_invert (shard_bitset_per_slot : list Dal_attestation_repr.t)
    (slots : Dal_attestation_repr.t)
    (shards : list int) (bitset : Dal_attestation_repr.t) (i : int) :
    List.nth (Dal_attestation_repr.Accountability.record_shards_availability
      shard_bitset_per_slot slots shards) i = Some bitset
    match Bitset.mem slots i with
    | Pervasives.Error e
        List.nth shard_bitset_per_slot i = Some bitset
    | Pervasives.Ok false
        List.nth shard_bitset_per_slot i = Some bitset
    | Pervasives.Ok true bitset',
           Dal_attestation_repr.Accountability.record_slot_shard_availability
             bitset' shards = bitset
         List.nth shard_bitset_per_slot i = Some bitset'
    end.
  Proof.
    intro Hnth.
    destruct (List.nth_mapi_Some_invert _ _ _ _ Hnth) as [bitset' Hbitset'].
    destruct (Bitset.mem slots i); sauto.
  Qed.
End Accountability.