Skip to main content

Fixing reused proofs

· 5 min read

After each new release of the protocol there comes a need to validate it. One of the options would be to start from scratch, but fortunately there is no need for that since many parts of the protocol are only slightly changed or stay the same. That allows us to reuse old proofs in consequent versions and speed up the validation.

Of course there is a small number of proofs which stop working due to the changes and that has to be repaired. This process can sometimes be tricky since it requires an understanding of how different functions and proofs depend on each other, but that makes it very interesting. In this post, we will show examples of broken proofs, discuss reasons for their failure, and show techniques we used to fix issues.

Missing code

The easiest case is when a source file no longer contains the function or module that the proof validates. Then it suffices to remove the proofs or, if the corresponding code is now in another file, move them accordingly.

Compare and equality

Often a proof fails because validated data structure has been modified. Most often it breaks validation of equality or compare function because they depend directly on the structure of a particular type. In that case failure is caused by incomplete definition of projection to the type where the equality or compare function can be expressed from already proven-correct combinators (see Verifying the compare functions of OCaml for more information). To fix the proof we have to add projections for new constructors and accordingly modify comparison used after projection.

For example Destination_repr initially contained the following type:

Inductive t : Set :=
| Contract : Contract_repr.t -> t
| Tx_rollup : Tx_rollup_repr.t -> t.

and the proof of the validity of its compare function in the corresponding proofs file:

Lemma compare_is_valid :
Compare.Valid.t (fun _ => True) id Destination_repr.compare.
Proof.
apply (Compare.equality (
let proj_tx_rollup x :=
match x with
| Destination_repr.Tx_rollup x => Some x
| _ => None
end in
let proj_contract x :=
match x with
| Destination_repr.Contract x => Some x
| _ => None
end in
let proj x :=
(proj_tx_rollup x, proj_contract x) in
Compare.projection proj (
Compare.lexicographic
(Compare.Option.compare Tx_rollup_repr.compare)
(Compare.Option.compare Contract_repr.compare)
)
)); [intros [] []; cbn; hauto lq: on |].
Compare.valid_auto.
unfold id; sauto lq: on.
Qed.

but now we receive a message from the prover informing that hauto failed. If we temporarily remove hauto tactic we will see that some of the goals are now false, like this one:

True -> True -> -1 = 1

That indicates the projection and comparison used in tactic apply are invalid.

Indeed, in newer version new constructor of type t have been added:

Inductive t : Set :=
| Contract : Contract_repr.t -> t
| Tx_rollup : Tx_rollup_repr.t -> t
| Sc_rollup : Sc_rollup_repr.t -> t.

so we modify the projection getting:

Lemma compare_is_valid :
Compare.Valid.t (fun _ => True) id Destination_repr.compare.
Proof.
apply (Compare.equality (
let proj_sc_rollup x :=
match x with
| Destination_repr.Sc_rollup x => Some x
| _ => None
end in
let proj_tx_rollup x :=
match x with
| Destination_repr.Tx_rollup x => Some x
| _ => None
end in
let proj_contract x :=
match x with
| Destination_repr.Contract x => Some x
| _ => None
end in
let proj x :=
(proj_sc_rollup x, (proj_tx_rollup x, proj_contract x)) in
Compare.projection proj (
Compare.lexicographic
(Compare.Option.compare Sc_rollup_repr.Address.compare)
(
Compare.lexicographic
(Compare.Option.compare Tx_rollup_repr.compare)
(Compare.Option.compare Contract_repr.compare)
))
)); [intros [] []; cbn; hauto lq: on |].
Compare.valid_auto.
unfold id; sauto lq: on.
Qed.

so now the proof is fixed.

Encoding

Sometimes extending a data type affects more functions. One of these functions that is also often validated is encoding. Adding new constructors to a type returned by encoding causes tactic Data_encoding.Valid.data_encoding_auto we use in proofs of its validity to fail to solve some intermediate goals causing the proof to break.

The reason why Data_encoding.Valid.data_encoding_auto does not work properly is that it requires proofs of validity of other encoding functions our encoding depends on. These should be included in the hint database Data_encoding_db. To fix the proof of encoding validity, we define and add relevant lemmas to the database.

Let us consider the following example:

Sc_rollup_inbox contains a type t : Set that initially was:

  Record record : Set := Build {
rollup : Sc_rollup_repr.t;
level : Raw_level_repr.t;
nb_available_messages : int64;
message_counter : Z.t;
current_messages_hash : unit -> Context.Proof.hash;
old_levels_messages : history_proof;
}.

but it have been extended with two new constructors:

    nb_messages_in_commitment_period : int64;
starting_level_of_current_commitment_period : Raw_level_repr.t;

so the proof of encoding validity:

Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
repeat (split; try dtauto).
destruct_all Sc_rollup_inbox_repr.t; f_equal.
now apply functional_extentionality_unit.
Qed.

no longer works because it is missing a lemma in Data_encoding_db database stating that Sc_rollup_inbox_repr.Hash.encoding is valid:

  Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ => True)
Sc_rollup_inbox_repr.Hash.encoding.

In order to fix the proof we add that lemma and also add:

    starting_level_of_current_commitment_period : Raw_level_repr.Valid.t x.(starting_level_of_current_commitment_period);
nb_available_messages : Int64.Valid.t x.(nb_available_messages);

to the record Valid.t:

  Record t (x : Sc_rollup_inbox_repr.t) : Prop := {
level : Raw_level_repr.Valid.t x.(level);
nb_available_messages : Int64.Valid.t x.(nb_available_messages);
message_counter : 0 <= x.(message_counter);
}.

because that particular proof also depends on it.

More complicated functions

Sometimes it happens that in a new release simple function gets very complicated with many local functions defined using let, which cannot be eliminated by applying lemmas (because you cannot create a lemma describing a local function). In that situation we create a new equivalent definition of the same function, but with its local functions defined externally. It lets us to create lemmas about these local functions, what allows us to make only little changes to the structure of the reused proof.