Commit 6c960f42 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Update for dev Coq

parent 81647d05
Pipeline #12542 passed with stage
in 5 minutes and 23 seconds
...@@ -495,7 +495,7 @@ Proof. ...@@ -495,7 +495,7 @@ Proof.
destruct (FMap.find (next_proposal_id state) (proposals state)) as [proposal|] eqn:find. destruct (FMap.find (next_proposal_id state) (proposals state)) as [proposal|] eqn:find.
- remember_new_proposal. - remember_new_proposal.
rewrite <- (FMap.add_remove _ (next_proposal_id state) new_proposal). rewrite <- (FMap.add_remove _ (next_proposal_id state) new_proposal).
Hint Resolve FMap.find_remove. Hint Resolve FMap.find_remove : core.
rewrite <- (FMap.add_id _ _ _ find) at 2. rewrite <- (FMap.add_id _ _ _ find) at 2.
rewrite <- (FMap.add_remove _ (next_proposal_id state) proposal). rewrite <- (FMap.add_remove _ (next_proposal_id state) proposal).
repeat rewrite FMap.elements_add; auto. repeat rewrite FMap.elements_add; auto.
...@@ -540,7 +540,7 @@ Proof. ...@@ -540,7 +540,7 @@ Proof.
rewrite <- (FMap.add_id (proposals state) pid p) at 2; auto. rewrite <- (FMap.add_id (proposals state) pid p) at 2; auto.
rewrite <- (FMap.add_remove _ pid p). rewrite <- (FMap.add_remove _ pid p).
rewrite <- (FMap.add_remove _ pid new_proposal). rewrite <- (FMap.add_remove _ pid new_proposal).
Hint Resolve FMap.find_remove. Hint Resolve FMap.find_remove : core.
repeat rewrite FMap.elements_add; auto. repeat rewrite FMap.elements_add; auto.
subst; reflexivity. subst; reflexivity.
Qed. Qed.
...@@ -793,7 +793,7 @@ Theorem congress_txs_well_behaved to contract : ...@@ -793,7 +793,7 @@ Theorem congress_txs_well_behaved to contract :
num_acts_created_in_proposals to contract. num_acts_created_in_proposals to contract.
Proof. Proof.
intros [trace] congress_deployed. intros [trace] congress_deployed.
Hint Resolve contract_addr_format. Hint Resolve contract_addr_format : core.
assert (address_is_contract contract = true) as addr_format by eauto. assert (address_is_contract contract = true) as addr_format by eauto.
remember empty_state eqn:eq. remember empty_state eqn:eq.
(* Contract cannot have been deployed in empty trace so we solve that immediately. *) (* Contract cannot have been deployed in empty trace so we solve that immediately. *)
......
...@@ -437,7 +437,7 @@ Section Theories. ...@@ -437,7 +437,7 @@ Section Theories.
let count tx := let count tx :=
match tx_body tx with match tx_body tx with
| tx_call msg => | tx_call msg =>
match deserialize msg with match deserialize msg : option Msg with
| Some (create_proposal acts) => length acts | Some (create_proposal acts) => length acts
| _ => 0 | _ => 0
end end
......
...@@ -348,7 +348,7 @@ Section ExecuteActions. ...@@ -348,7 +348,7 @@ Section ExecuteActions.
destruct trace as [trace]. destruct trace as [trace].
Hint Constructors ChainEvent : core. Hint Constructors ChainEvent : core.
Hint Constructors ChainedList : core. Hint Constructors ChainedList : core.
Hint Unfold ChainTrace. Hint Unfold ChainTrace : core.
destruct df. destruct df.
+ (* depth-first case *) + (* depth-first case *)
eapply IH; try eassumption; eauto. eapply IH; try eassumption; eauto.
...@@ -504,7 +504,7 @@ Proof. ...@@ -504,7 +504,7 @@ Proof.
refine (execute_actions_reachable _ _ _ _ _ _ exec). refine (execute_actions_reachable _ _ _ _ _ _ exec).
constructor. constructor.
refine (snoc prev_lcb_trace _). refine (snoc prev_lcb_trace _).
Hint Resolve validate_header_valid validate_actions_valid. Hint Resolve validate_header_valid validate_actions_valid : core.
eapply evt_block; eauto. eapply evt_block; eauto.
apply add_new_block_header_equiv. apply add_new_block_header_equiv.
reflexivity. reflexivity.
......
...@@ -178,7 +178,7 @@ Section LocalBlockchainTests. ...@@ -178,7 +178,7 @@ Section LocalBlockchainTests.
Print Assumptions chain8. Print Assumptions chain8.
End LocalBlockchainTests. End LocalBlockchainTests.
Hint Resolve congress_txs_after_block. Hint Resolve congress_txs_after_block : core.
(* The congress satisfies a property specialized to the local blockchain DFS: *) (* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block Lemma congress_txs_after_local_chain_block
(prev new : LocalChainBuilderDepthFirst) baker acts slot finalization_height : (prev new : LocalChainBuilderDepthFirst) baker acts slot finalization_height :
......
Supports Markdown
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