Commit f4bc2be8 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Fix for Coq 8.8

parent e7245511
Pipeline #12837 passed with stage
in 5 minutes and 23 seconds
......@@ -362,7 +362,7 @@ Definition validate_header (header : BlockHeader) (chain : Chain) : option unit
&& (current_slot chain <? block_slot header)
&& (finalized_height chain <=? block_finalized_height header)
&& (block_finalized_height header <? block_height header)
&& (Bool.eqb (address_is_contract (block_creator header)) false)
&& negb (address_is_contract (block_creator header))
&& (block_reward header >=? 0)%Z
then Some tt
else None.
......@@ -378,9 +378,11 @@ Proof.
| [H: context[Nat.eqb ?a ?b] |- _] => destruct (Nat.eqb_spec a b)
| [H: context[Nat.ltb ?a ?b] |- _] => destruct (Nat.ltb_spec a b)
| [H: context[Nat.leb ?a ?b] |- _] => destruct (Nat.leb_spec a b)
| [H: context[Bool.eqb ?a ?b] |- _] => destruct (Bool.eqb_spec a b)
| [H: context[Z.geb ?a ?b] |- _] => destruct (Z.geb_spec a b)
end; [|repeat rewrite Bool.andb_false_r in valid; cbn in valid; congruence]).
destruct (negb (address_is_contract (block_creator header))) eqn:to_acc;
[|cbn in valid; congruence].
apply Bool.negb_true_iff in to_acc.
apply build_is_valid_next_block; cbn; auto.
lia.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment