Commit aea281d5 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Get rid of versions and a comment

Versions are not used for anything and the comment is outdated.
parent 8962fbb6
...@@ -14,8 +14,6 @@ From stdpp Require countable. ...@@ -14,8 +14,6 @@ From stdpp Require countable.
Import ListNotations. Import ListNotations.
Definition Version := nat.
Definition Amount := Z. Definition Amount := Z.
Bind Scope Z_scope with Amount. Bind Scope Z_scope with Amount.
...@@ -126,23 +124,8 @@ Inductive ActionBody := ...@@ -126,23 +124,8 @@ Inductive ActionBody :=
| act_transfer (to : Address) (amount : Amount) | act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue) | act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue) | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
(* Since one operation is the possibility to deploy a new contract,
this represents an instance of a contract. Note that the act of deploying
a contract has to be a separate thing to the contract deployment a contract
can access during its execution due to positivity constraints. That is,
we would like to allow contracts to obtain information about what another
contract was deployed with (its setup, version and amount transferred). An obvious
way to model this would be to simply store a WeakContract in the chain.
But this is already a non-strict positive occurence, since we dumbed down then
end up with
Record WeakContract := { receive : (Address -> WeakContract) -> State -> State }.
where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments.
*)
with WeakContract := with WeakContract :=
| build_weak_contract | build_weak_contract
(version : Version)
(init : (init :
Chain -> Chain ->
ContractCallContext -> ContractCallContext ->
...@@ -161,11 +144,8 @@ with WeakContract := ...@@ -161,11 +144,8 @@ with WeakContract :=
(receive_proper : (receive_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive). Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive).
Definition wc_version (wc : WeakContract) : Version :=
let (v, _, _, _, _) := wc in v.
Definition wc_init (wc : WeakContract) := Definition wc_init (wc : WeakContract) :=
let (_, i, _, _, _) := wc in i. let (i, _, _, _) := wc in i.
Global Instance wc_init_proper : Global Instance wc_init_proper :
Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq) wc_init. Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq) wc_init.
...@@ -174,12 +154,12 @@ Proof. ...@@ -174,12 +154,12 @@ Proof.
exact ( exact (
match wc return match wc return
Proper (ChainEquiv ==> eq ==> eq ==> eq) (wc_init wc) with Proper (ChainEquiv ==> eq ==> eq ==> eq) (wc_init wc) with
| build_weak_contract _ _ ip _ _ => ip | build_weak_contract _ ip _ _ => ip
end). end).
Qed. Qed.
Definition wc_receive (wc : WeakContract) := Definition wc_receive (wc : WeakContract) :=
let (_, _, _, r, _) := wc in r. let (_, _, r, _) := wc in r.
Global Instance wc_receive_proper : Global Instance wc_receive_proper :
Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq ==> eq) wc_receive. Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq ==> eq) wc_receive.
...@@ -188,7 +168,7 @@ Proof. ...@@ -188,7 +168,7 @@ Proof.
exact ( exact (
match wc return match wc return
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) (wc_receive wc) with Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) (wc_receive wc) with
| build_weak_contract _ _ _ _ rp => rp | build_weak_contract _ _ _ rp => rp
end). end).
Qed. Qed.
...@@ -208,7 +188,6 @@ Record Contract ...@@ -208,7 +188,6 @@ Record Contract
`{OakTypeEquivalence Msg} `{OakTypeEquivalence Msg}
`{OakTypeEquivalence State} := `{OakTypeEquivalence State} :=
build_contract { build_contract {
version : Version;
init : init :
Chain -> Chain ->
ContractCallContext -> ContractCallContext ->
...@@ -226,7 +205,6 @@ Record Contract ...@@ -226,7 +205,6 @@ Record Contract
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive; Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
}. }.
Arguments version {_ _ _ _ _ _}.
Arguments init {_ _ _ _ _ _}. Arguments init {_ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _}. Arguments receive {_ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _}. Arguments build_contract {_ _ _ _ _ _}.
...@@ -252,7 +230,7 @@ Program Definition contract_to_weak_contract ...@@ -252,7 +230,7 @@ Program Definition contract_to_weak_contract
do '(new_state, acts) <- c.(receive) chain ctx state None; do '(new_state, acts) <- c.(receive) chain ctx state None;
Some (serialize new_state, acts) Some (serialize new_state, acts)
end in end in
build_weak_contract c.(version) weak_init _ weak_recv _. build_weak_contract weak_init _ weak_recv _.
Next Obligation. Next Obligation.
intros. intros.
intros c1 c2 eq_chains ctx1 ctx2 eq_ctx setup1 setup2 eq_setups. intros c1 c2 eq_chains ctx1 ctx2 eq_ctx setup1 setup2 eq_setups.
...@@ -935,7 +913,6 @@ Global Coercion builder_type : ChainBuilderType >-> Sortclass. ...@@ -935,7 +913,6 @@ Global Coercion builder_type : ChainBuilderType >-> Sortclass.
Global Coercion builder_env : builder_type >-> Environment. Global Coercion builder_env : builder_type >-> Environment.
End Blockchain. End Blockchain.
Arguments version {_ _ _ _ _ _ _}.
Arguments init {_ _ _ _ _ _ _}. Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}. Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}. Arguments build_contract {_ _ _ _ _ _ _}.
......
...@@ -198,8 +198,6 @@ Qed. ...@@ -198,8 +198,6 @@ Qed.
End Equivalences. End Equivalences.
Definition version : Version := 1%nat.
Definition validate_rules (rules : Rules) : bool := Definition validate_rules (rules : Rules) : bool :=
(rules.(min_vote_count_permille) >=? 0) (rules.(min_vote_count_permille) >=? 0)
&& (rules.(min_vote_count_permille) <=? 1000) && (rules.(min_vote_count_permille) <=? 1000)
...@@ -369,7 +367,7 @@ Lemma receive_proper : ...@@ -369,7 +367,7 @@ Lemma receive_proper :
Proof. repeat intro; solve_contract_proper. Qed. Proof. repeat intro; solve_contract_proper. Qed.
Definition contract : Contract Setup Msg State := Definition contract : Contract Setup Msg State :=
build_contract version init init_proper receive receive_proper. build_contract init init_proper receive receive_proper.
Section Theories. Section Theories.
Local Open Scope nat. Local Open Scope nat.
......
...@@ -202,8 +202,6 @@ Qed. ...@@ -202,8 +202,6 @@ Qed.
End Equivalences. End Equivalences.
Definition version : Version := 1%nat.
Definition validate_rules (rules : Rules) : bool := Definition validate_rules (rules : Rules) : bool :=
(rules.(min_vote_count_permille) >=? 0) (rules.(min_vote_count_permille) >=? 0)
&& (rules.(min_vote_count_permille) <=? 1000) && (rules.(min_vote_count_permille) <=? 1000)
...@@ -381,7 +379,7 @@ Lemma receive_proper : ...@@ -381,7 +379,7 @@ Lemma receive_proper :
Proof. repeat intro; solve_contract_proper. Qed. Proof. repeat intro; solve_contract_proper. Qed.
Definition contract : Contract Setup Msg State := Definition contract : Contract Setup Msg State :=
build_contract version init init_proper receive receive_proper. build_contract init init_proper receive receive_proper.
End CongressBuggy. End CongressBuggy.
(* We will show that this contract is buggy and does not satisfy the (* We will show that this contract is buggy and does not satisfy the
...@@ -421,7 +419,7 @@ Instance exploit_receive_proper : ...@@ -421,7 +419,7 @@ Instance exploit_receive_proper :
Proof. now subst. Qed. Proof. now subst. Qed.
Definition exploit_contract : Contract ExploitSetup ExploitMsg ExploitState := Definition exploit_contract : Contract ExploitSetup ExploitMsg ExploitState :=
build_contract 0 exploit_init exploit_init_proper exploit_receive exploit_receive_proper. build_contract exploit_init exploit_init_proper exploit_receive exploit_receive_proper.
End ExploitContract. End ExploitContract.
......
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