Commit 1f7a5567 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Some small cleanups

parent bd58cff0
......@@ -55,10 +55,11 @@ Lemma step_circulation_unchanged
{pre : Environment}
{act : Action}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act post new_acts) :
{new_acts : list Action} :
ChainStep pre act post new_acts ->
circulation post = circulation pre.
Proof.
intros step.
destruct (address_eqb_spec (step_from step) (step_to step))
as [from_eq_to | from_neq_to]; eauto.
destruct (address_reorganize from_neq_to) as [suf perm].
......
......@@ -366,7 +366,7 @@ Section Theories.
Local Open Scope nat.
Definition num_acts_created_in_proposals chain address :=
let extract tx :=
let count tx :=
match tx_body tx with
| tx_call msg =>
match deserialize msg with
......@@ -375,7 +375,7 @@ Definition num_acts_created_in_proposals chain address :=
end
| _ => 0
end in
sumnat extract (incoming_txs chain address).
sumnat count (incoming_txs chain address).
Definition num_cacts_in_raw_state state :=
sumnat (fun '(k, v) => length (actions v)) (FMap.elements (proposals state)).
......@@ -886,7 +886,7 @@ Corollary congress_txs_after_block
prev baker acts slot finalization_height new :
builder_add_block prev baker acts slot finalization_height = Some new ->
forall addr,
env_contracts (builder_env new) addr = Some (Congress.contract : WeakContract) ->
env_contracts new addr = Some (Congress.contract : WeakContract) ->
length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof.
intros add_block contract congress_at_addr.
......
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