Commit 4f766233 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Rename OakValue -> SerializedValue

parent f4bc2be8
......@@ -12,7 +12,7 @@ theories/Finite.v
theories/LocalBlockchain.v
theories/LocalBlockchainTests.v
theories/Monads.v
theories/Oak.v
theories/Serializable.v
-R vendor/record-update RecordUpdate
vendor/record-update/RecordSet.v
vendor/record-update/RecordUpdate.v
......@@ -4,7 +4,7 @@ From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Serializable.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
......@@ -25,12 +25,12 @@ Class ChainBase :=
forall (a b : Address), Bool.reflect (a = b) (address_eqb a b);
address_eqdec :> stdpp.base.EqDecision Address;
address_countable :> countable.Countable Address;
address_ote :> OakTypeEquivalence Address;
address_serializable :> Serializable Address;
address_is_contract : Address -> bool;
}.
Global Opaque Address address_eqb address_eqb_spec
address_eqdec address_countable address_ote.
address_eqdec address_countable address_serializable.
Delimit Scope address_scope with address.
Bind Scope address_scope with Address.
......@@ -73,7 +73,7 @@ Record Chain :=
current_slot : nat;
finalized_height : nat;
account_balance : Address -> Amount;
contract_state : Address -> option OakValue;
contract_state : Address -> option SerializedValue;
}.
(* Two chains are said to be equivalent if they are extensionally equal.
......@@ -123,24 +123,24 @@ Record ContractCallContext :=
to interact with a chain. *)
Inductive ActionBody :=
| act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
| act_call (to : Address) (amount : Amount) (msg : SerializedValue)
| act_deploy (amount : Amount) (c : WeakContract) (setup : SerializedValue)
with WeakContract :=
| build_weak_contract
(init :
Chain ->
ContractCallContext ->
OakValue (* setup *) ->
option OakValue)
SerializedValue (* setup *) ->
option SerializedValue)
(* Init respects chain equivalence *)
(init_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq) init)
(receive :
Chain ->
ContractCallContext ->
OakValue (* state *) ->
option OakValue (* message *) ->
option (OakValue * list ActionBody))
SerializedValue (* state *) ->
option SerializedValue (* message *) ->
option (SerializedValue * list ActionBody))
(* And so does receive *)
(receive_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive).
......@@ -185,9 +185,9 @@ only "internally" for blockchains, while any strongly-typed contract can
be converted to and from *)
Record Contract
(Setup Msg State : Type)
`{OakTypeEquivalence Setup}
`{OakTypeEquivalence Msg}
`{OakTypeEquivalence State} :=
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State} :=
build_contract {
init :
Chain ->
......@@ -212,19 +212,19 @@ Arguments build_contract {_ _ _ _ _ _}.
Program Definition contract_to_weak_contract
{Setup Msg State : Type}
`{OakTypeEquivalence Setup}
`{OakTypeEquivalence Msg}
`{OakTypeEquivalence State}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
(c : Contract Setup Msg State) : WeakContract :=
let weak_init chain ctx oak_setup :=
do setup <- deserialize oak_setup;
let weak_init chain ctx ser_setup :=
do setup <- deserialize ser_setup;
do state <- c.(init) chain ctx setup;
Some (serialize state) in
let weak_recv chain ctx oak_state oak_msg_opt :=
do state <- deserialize oak_state;
match oak_msg_opt with
| Some oak_msg =>
do msg <- deserialize oak_msg;
let weak_recv chain ctx ser_state ser_msg_opt :=
do state <- deserialize ser_state;
match ser_msg_opt with
| Some ser_msg =>
do msg <- deserialize ser_msg;
do '(new_state, acts) <- c.(receive) chain ctx state (Some msg);
Some (serialize new_state, acts)
| None =>
......@@ -249,7 +249,7 @@ Next Obligation.
simpl.
destruct (deserialize state1); auto; simpl.
destruct msg1.
+ destruct (deserialize o); auto; simpl.
+ destruct (deserialize _); auto; simpl.
now rewrite receive_proper.
+ now rewrite receive_proper.
Qed.
......@@ -259,9 +259,9 @@ Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* Deploy a strongly typed contract with some amount and setup *)
Definition create_deployment
{Setup Msg State : Type}
`{OakTypeEquivalence Setup}
`{OakTypeEquivalence Msg}
`{OakTypeEquivalence State}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
(amount : Amount)
(contract : Contract Setup Msg State)
(setup : Setup) : ActionBody :=
......@@ -269,7 +269,7 @@ Definition create_deployment
(* The contract interface is the main mechanism allowing a deployed
contract to interact with another deployed contract. This hides
the ugly details of everything being OakValue away from contracts. *)
the ugly details of everything being SerializedValue away from contracts. *)
Record ContractInterface {Msg State : Type} :=
build_contract_interface {
(* The address of the contract being interfaced with *)
......@@ -286,8 +286,8 @@ Definition get_contract_interface
(chain : Chain)
(addr : Address)
(Msg State : Type)
`{OakTypeEquivalence Msg}
`{OakTypeEquivalence State}
`{Serializable Msg}
`{Serializable State}
: option (ContractInterface Msg State) :=
let ifc_get_state chain := contract_state chain addr >>= deserialize in
let ifc_send amount msg :=
......@@ -309,8 +309,9 @@ Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amou
else map a.
Definition set_chain_contract_state
(addr : Address) (state : OakValue) (map : Address -> option OakValue)
: Address -> option OakValue :=
(addr : Address) (state : SerializedValue)
(map : Address -> option SerializedValue)
: Address -> option SerializedValue :=
fun a => if (a =? addr)%address
then Some state
else map a.
......@@ -363,7 +364,8 @@ Definition add_contract (addr : Address) (contract : WeakContract) (env : Enviro
then Some contract
else f a|>.
Definition set_contract_state (addr : Address) (state : OakValue) (env : Environment) :=
Definition set_contract_state
(addr : Address) (state : SerializedValue) (env : Environment) :=
env<|env_chain; contract_state ::= set_chain_contract_state addr state|>.
Ltac rewrite_environment_equiv :=
......@@ -432,8 +434,8 @@ Inductive ActionEvaluation :
(from to : Address)
(amount : Amount)
(wc : WeakContract)
(setup : OakValue)
(state : OakValue),
(setup : SerializedValue)
(state : SerializedValue),
amount <= account_balance pre from ->
address_is_contract to = true ->
env_contracts pre to = None ->
......@@ -455,9 +457,9 @@ Inductive ActionEvaluation :
(from to : Address)
(amount : Amount)
(wc : WeakContract)
(msg : option OakValue)
(prev_state : OakValue)
(new_state : OakValue)
(msg : option SerializedValue)
(prev_state : SerializedValue)
(new_state : SerializedValue)
(resp_acts : list ActionBody),
amount <= account_balance pre from ->
env_contracts pre to = Some wc ->
......@@ -671,8 +673,8 @@ a normal blockchain is. Each evaluation of an action in the blockchain correspon
a transaction, so we can go from a trace to a list of transactions. *)
Inductive TxBody :=
| tx_empty
| tx_deploy (wc : WeakContract) (setup : OakValue)
| tx_call (msg : option OakValue).
| tx_deploy (wc : WeakContract) (setup : SerializedValue)
| tx_call (msg : option SerializedValue).
Record Tx :=
build_tx {
......
......@@ -3,7 +3,7 @@ From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Serializable.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Automation.
......@@ -25,7 +25,7 @@ Definition ProposalId := nat.
Inductive CongressAction :=
| cact_transfer (to : Address) (amount : Amount)
| cact_call (to : Address) (amount : Amount) (msg : OakValue).
| cact_call (to : Address) (amount : Amount) (msg : SerializedValue).
Record Proposal :=
build_proposal {
......@@ -73,13 +73,13 @@ Record State :=
Instance state_settable : Settable _ :=
settable! build_state <owner; state_rules; proposals; next_proposal_id; members>.
Section Equivalences.
Section Serialization.
Definition deserialize_rules (v : OakValue) : option Rules :=
Definition deserialize_rules (v : SerializedValue) : option Rules :=
do '(a, b, c) <- deserialize v;
Some (build_rules a b c).
Global Program Instance rules_equivalence : OakTypeEquivalence Rules :=
Global Program Instance rules_serializable : Serializable Rules :=
{| serialize r := let (a, b, c) := r in serialize (a, b, c);
(* Why does
deserialize v :=
......@@ -93,7 +93,7 @@ Next Obligation.
reflexivity.
Qed.
Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
Global Program Instance setup_serializable : Serializable Setup :=
{| serialize s := serialize s.(setup_rules);
deserialize or :=
do rules <- deserialize or;
......@@ -105,14 +105,14 @@ Next Obligation.
reflexivity.
Qed.
Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
Definition deserialize_congress_action (v : SerializedValue) : option CongressAction :=
do val <- deserialize v;
Some (match val with
| inl (to, amount) => cact_transfer to amount
| inr (to, amount, msg) => cact_call to amount msg
end).
Global Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
Global Program Instance congress_action_serializable : Serializable CongressAction :=
{| serialize ca :=
serialize
match ca with
......@@ -127,11 +127,11 @@ Next Obligation.
destruct ca; reflexivity.
Qed.
Definition deserialize_proposal (v : OakValue) : option Proposal :=
Definition deserialize_proposal (v : SerializedValue) : option Proposal :=
do '(a, b, c, d) <- deserialize v;
Some (build_proposal a b c d).
Global Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
Global Program Instance proposal_serializable : Serializable Proposal :=
{| serialize p :=
let (a, b, c, d) := p in
serialize (a, b, c, d);
......@@ -144,7 +144,7 @@ Next Obligation.
destruct p; reflexivity.
Qed.
Definition serialize_msg (m : Msg) : OakValue :=
Definition serialize_msg (m : Msg) : SerializedValue :=
serialize
match m with
| transfer_ownership a => (0, serialize a)
......@@ -158,7 +158,7 @@ Definition serialize_msg (m : Msg) : OakValue :=
| finish_proposal pid => (8, serialize pid)
end.
Definition deserialize_msg (v : OakValue) : option Msg :=
Definition deserialize_msg (v : SerializedValue) : option Msg :=
do '(tag, v) <- deserialize v;
match tag with
| 0 => option_map transfer_ownership (deserialize v)
......@@ -173,7 +173,7 @@ Definition deserialize_msg (v : OakValue) : option Msg :=
| _ => None
end.
Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
Global Program Instance msg_serializable : Serializable Msg :=
{| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
intros msg.
......@@ -181,22 +181,22 @@ Next Obligation.
destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
Definition serialize_state (s : State) : OakValue :=
Definition serialize_state (s : State) : SerializedValue :=
let (a, b, c, d, e) := s in
serialize (a, b, c, d, e).
Definition deserialize_state (v : OakValue) : option State :=
Definition deserialize_state (v : SerializedValue) : option State :=
do '(a, b, c, d, e) <- deserialize v;
Some (build_state a b c d e).
Global Program Instance state_equivalence : OakTypeEquivalence State :=
Global Program Instance state_serializable : Serializable State :=
{| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
unfold serialize_state, deserialize_state.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
End Equivalences.
End Serialization.
Definition validate_rules (rules : Rules) : bool :=
(rules.(min_vote_count_permille) >=? 0)
......
......@@ -3,7 +3,7 @@ From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Serializable.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Automation.
......@@ -25,7 +25,7 @@ Definition ProposalId := nat.
Inductive CongressAction :=
| cact_transfer (to : Address) (amount : Amount)
| cact_call (to : Address) (amount : Amount) (msg : OakValue).
| cact_call (to : Address) (amount : Amount) (msg : SerializedValue).
Record Proposal :=
build_proposal {
......@@ -74,13 +74,13 @@ Record State :=
Instance state_settable : Settable _ :=
settable! build_state <owner; state_rules; proposals; next_proposal_id; members>.
Section Equivalences.
Section Serialization.
Definition deserialize_rules (v : OakValue) : option Rules :=
Definition deserialize_rules (v : SerializedValue) : option Rules :=
do '((a, b), c) <- deserialize v;
Some (build_rules a b c).
Global Program Instance rules_equivalence : OakTypeEquivalence Rules :=
Global Program Instance rules_serializable : Serializable Rules :=
{| serialize r := let (a, b, c) := r in serialize (a, b, c);
(* Why does
deserialize v :=
......@@ -94,7 +94,7 @@ Next Obligation.
reflexivity.
Qed.
Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
Global Program Instance setup_serializable : Serializable Setup :=
{| serialize s := serialize s.(setup_rules);
deserialize or :=
do rules <- deserialize or;
......@@ -106,14 +106,14 @@ Next Obligation.
reflexivity.
Qed.
Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
Definition deserialize_congress_action (v : SerializedValue) : option CongressAction :=
do val <- deserialize v;
Some (match val with
| inl (to, amount) => cact_transfer to amount
| inr (to, amount, msg) => cact_call to amount msg
end).
Global Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
Global Program Instance congress_action_serializable : Serializable CongressAction :=
{| serialize ca :=
serialize
match ca with
......@@ -128,11 +128,11 @@ Next Obligation.
destruct ca; reflexivity.
Qed.
Definition deserialize_proposal (v : OakValue) : option Proposal :=
Definition deserialize_proposal (v : SerializedValue) : option Proposal :=
do '(a, b, c, d) <- deserialize v;
Some (build_proposal a b c d).
Global Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
Global Program Instance proposal_serializable : Serializable Proposal :=
{| serialize p :=
let (a, b, c, d) := p in
serialize (a, b, c, d);
......@@ -145,7 +145,7 @@ Next Obligation.
destruct p; reflexivity.
Qed.
Definition serialize_msg (m : Msg) : OakValue :=
Definition serialize_msg (m : Msg) : SerializedValue :=
serialize
match m with
| transfer_ownership a => (0, serialize a)
......@@ -160,7 +160,7 @@ Definition serialize_msg (m : Msg) : OakValue :=
| finish_proposal_remove pid => (9, serialize pid)
end.
Definition deserialize_msg (v : OakValue) : option Msg :=
Definition deserialize_msg (v : SerializedValue) : option Msg :=
do '(tag, v) <- deserialize v;
match tag with
| 0 => option_map transfer_ownership (deserialize v)
......@@ -176,7 +176,7 @@ Definition deserialize_msg (v : OakValue) : option Msg :=
| _ => None
end.
Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
Global Program Instance msg_serializable : Serializable Msg :=
{| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
intros msg.
......@@ -184,22 +184,22 @@ Next Obligation.
destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
Definition serialize_state (s : State) : OakValue :=
Definition serialize_state (s : State) : SerializedValue :=
let (a, b, c, d, e) := s in
serialize (a, b, c, d, e).
Definition deserialize_state (v : OakValue) : option State :=
Definition deserialize_state (v : SerializedValue) : option State :=
do '(a, b, c, d, e) <- deserialize v;
Some (build_state a b c d e).
Global Program Instance state_equivalence : OakTypeEquivalence State :=
Global Program Instance state_serializable : Serializable State :=
{| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
unfold serialize_state, deserialize_state.
destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
Qed.
End Equivalences.
End Serialization.
Definition validate_rules (rules : Rules) : bool :=
(rules.(min_vote_count_permille) >=? 0)
......
......@@ -2,7 +2,7 @@ From Coq Require Import ZArith.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Serializable.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
......@@ -37,7 +37,7 @@ Record LocalChain :=
lc_slot : nat;
lc_fin_height : nat;
lc_account_balances : FMap Address Amount;
lc_contract_state : FMap Address OakValue;
lc_contract_state : FMap Address SerializedValue;
lc_contracts : FMap Address WeakContract;
}.
......@@ -79,14 +79,14 @@ Section ExecuteActions.
Definition set_contract_state
(addr : Address)
(state : OakValue)
(state : SerializedValue)
(lc : LocalChain) : LocalChain :=
lc<|lc_contract_state ::= FMap.add addr state|>.
Definition send_or_call
(from to : Address)
(amount : Amount)
(msg : option OakValue)
(msg : option SerializedValue)
(lc : LocalChain) : option (list Action * LocalChain) :=
do if amount >? account_balance lc from then None else Some tt;
match FMap.find to lc.(lc_contracts) with
......@@ -110,7 +110,7 @@ Section ExecuteActions.
(from : Address)
(amount : Amount)
(wc : WeakContract)
(setup : OakValue)
(setup : SerializedValue)
(lc : LocalChain)
: option (list Action * LocalChain) :=
do if amount >? account_balance lc from then None else Some tt;
......@@ -240,7 +240,7 @@ Section ExecuteActions.
destruct (wc_receive wc _ _ _ _) eqn:receive;
[|cbn in *; congruence].
match goal with
| [p: OakValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
| [p: SerializedValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
end.
Hint Resolve gtb_le : core.
apply (eval_call from to amount wc msg prev_state new_state resp_acts);
......
......@@ -2,7 +2,6 @@ From SmartContracts Require Import Monads.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import LocalBlockchain.
From SmartContracts Require Import Congress.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Containers.
From SmartContracts Require Import BoundedN.
From SmartContracts Require Import Extras.
......
This diff is collapsed.
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