🍲 Dal_attestation_repr.v
Proofs
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.
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].
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.
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.
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.
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.
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.
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.
(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.
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.
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.
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.
(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.
(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.
(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.
Lemma record_shards_availability_is_valid shard_bitset_per_slot slots shards
(H_shard_bitset_per_slot : Valid.t shard_bitset_per_slot)
(H_slots : Dal_attestation_repr.Valid.t slots)
(H_shards : List.Forall shard_index.Valid.t shards) :
Valid.t(
Dal_attestation_repr.Accountability.record_shards_availability
shard_bitset_per_slot slots shards
).
Proof.
Admitted.
(H_shard_bitset_per_slot : Valid.t shard_bitset_per_slot)
(H_slots : Dal_attestation_repr.Valid.t slots)
(H_shards : List.Forall shard_index.Valid.t shards) :
Valid.t(
Dal_attestation_repr.Accountability.record_shards_availability
shard_bitset_per_slot slots shards
).
Proof.
Admitted.
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.
(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.
(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.
(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.