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

Clean up some Oak stuff

parent 8aa41abe
Pipeline #12076 failed with stage
in 6 minutes and 50 seconds
...@@ -24,36 +24,17 @@ Class ChainBaseTypes := ...@@ -24,36 +24,17 @@ Class ChainBaseTypes :=
Address : Type; Address : Type;
address_eqb : Address -> Address -> bool; address_eqb : Address -> Address -> bool;
address_eqb_spec : forall (a b : Address), Bool.reflect (a = b) (address_eqb a b); address_eqb_spec : forall (a b : Address), Bool.reflect (a = b) (address_eqb a b);
address_encode : Address -> positive; address_eqdec :> stdpp.base.EqDecision Address;
address_decode : positive -> option Address; address_countable :> countable.Countable Address;
address_decode_encode : forall a, address_decode (address_encode a) = Some a; address_ote :> OakTypeEquivalence Address;
address_ote : OakTypeEquivalence Address;
compute_block_reward : nat -> Amount; compute_block_reward : nat -> Amount;
}. }.
Global Opaque Address address_eqb address_eqb_spec Global Opaque Address address_eqb address_eqb_spec
address_encode address_decode address_decode_encode address_eqdec address_countable
address_ote address_ote
compute_block_reward. compute_block_reward.
Module Address.
Global Instance Address_equivalence `{ChainBaseTypes} : OakTypeEquivalence Address :=
address_ote.
(* Allow stdpp to pick up instances to allow use of Address in maps *)
Import countable.
Global Instance Address_eq_dec `{ChainBaseTypes} : EqDecision Address.
Proof.
intros a b.
apply (reflect_dec (a = b) (address_eqb a b) (address_eqb_spec a b)).
Qed.
Global Instance Address_countable `{ChainBaseTypes} : Countable Address :=
{ encode := address_encode;
decode := address_decode;
decode_encode := address_decode_encode; }.
End Address.
Delimit Scope address_scope with address. Delimit Scope address_scope with address.
Bind Scope address_scope with Address. Bind Scope address_scope with Address.
Infix "=?" := address_eqb (at level 70) : address_scope. Infix "=?" := address_eqb (at level 70) : address_scope.
...@@ -358,7 +339,6 @@ Record ContractInterface {setup_ty msg_ty state_ty : Type} := ...@@ -358,7 +339,6 @@ Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
}. }.
Arguments ContractInterface _ _ _ : clear implicits. Arguments ContractInterface _ _ _ : clear implicits.
Arguments build_contract_interface {_ _ _}.
Definition get_contract_interface Definition get_contract_interface
(chain : Chain) (chain : Chain)
...@@ -757,3 +737,4 @@ Arguments init {_ _ _ _ _ _ _}. ...@@ -757,3 +737,4 @@ Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}. Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}. Arguments build_contract {_ _ _ _ _ _ _}.
Arguments ContractInterface {_} _ _ _. Arguments ContractInterface {_} _ _ _.
Arguments build_contract_interface {_ _ _ _}.
...@@ -6,13 +6,14 @@ From SmartContracts Require Import Automation. ...@@ -6,13 +6,14 @@ From SmartContracts Require Import Automation.
From Coq Require Import Eqdep_dec. From Coq Require Import Eqdep_dec.
From Coq Require Import List. From Coq Require Import List.
From Coq Require Import Psatz. From Coq Require Import Psatz.
From Coq Require Import JMeq.
From stdpp Require countable. From stdpp Require countable.
Import ListNotations. Import ListNotations.
Local Open Scope N. Local Open Scope N.
Inductive BoundedN (bound : N) := Inductive BoundedN (bound : N) :=
| bounded (n : N) (_ : n < bound) : BoundedN bound. | bounded (n : N) (_ : (bound ?= n) = Gt).
Arguments bounded {_}. Arguments bounded {_}.
...@@ -23,32 +24,17 @@ Module BoundedN. ...@@ -23,32 +24,17 @@ Module BoundedN.
Definition eqb {bound : N} (a b : BoundedN bound) : bool := Definition eqb {bound : N} (a b : BoundedN bound) : bool :=
N.eqb (to_N a) (to_N b). N.eqb (to_N a) (to_N b).
Definition eq_dec {bound : N} (a b : BoundedN bound) : Definition of_N_compare {bound : N} (n : N) : option ((bound ?= n) = Gt) :=
{a = b} + {a <> b}. match bound ?= n as comp return (option (comp = Gt)) with
Proof. | Gt => Some eq_refl
destruct a as [a alt], b as [b blt]. | _ => None
destruct (N.eq_dec a b). end.
- left. subst. f_equal.
apply UIP_dec. Definition of_N {bound : N} (n : N) : option (BoundedN bound) :=
decide equality. match of_N_compare n with
- right. | Some prf => Some (bounded n prf)
intros H. | None => None
inversion H. end.
contradiction.
Defined.
Local Lemma N_lt_dec (a b : N) : {a < b} + {~(a < b)}.
Proof. unfold "<". decide equality. Defined.
Local Lemma Z_lt_dec (a b : Z) : ({a < b} + {~(a < b)})%Z.
Proof. unfold "<"%Z. decide equality. Defined.
Definition of_N {bound : N} (n : N) : option (BoundedN bound).
Proof.
destruct (N_lt_dec n bound).
- exact (Some (bounded n l)).
- exact None.
Defined.
Definition to_nat {bound : N} (n : BoundedN bound) : nat := Definition to_nat {bound : N} (n : BoundedN bound) : nat :=
N.to_nat (to_N n). N.to_nat (to_N n).
...@@ -122,12 +108,11 @@ Module BoundedN. ...@@ -122,12 +108,11 @@ Module BoundedN.
Lemma of_to_N {bound : N} (n : BoundedN bound) : Lemma of_to_N {bound : N} (n : BoundedN bound) :
of_N (to_N n) = Some n. of_N (to_N n) = Some n.
Proof. Proof.
destruct n as [n lt]; simpl. destruct n as [n prf]; simpl.
unfold of_N. unfold of_N.
destruct (N_lt_dec n bound). replace (of_N_compare n) with (Some prf); auto.
- f_equal. unfold of_N_compare.
now apply to_N_inj. now rewrite prf.
- tauto.
Qed. Qed.
Lemma of_to_nat {bound : N} (n : BoundedN bound) : Lemma of_to_nat {bound : N} (n : BoundedN bound) :
...@@ -161,17 +146,18 @@ Module BoundedN. ...@@ -161,17 +146,18 @@ Module BoundedN.
Proof. Proof.
intros H. intros H.
unfold of_N in H. unfold of_N in H.
destruct (N_lt_dec m bound); prove. destruct (of_N_compare m); try congruence.
now inversion H.
Qed. Qed.
Lemma of_N_none {bound : N} {m : N} : Lemma of_N_none {bound : N} {m : N} :
@of_N bound m = None -> m >= bound. @of_N bound m = None -> bound <= m.
Proof. Proof.
intros H. intros H.
unfold of_N in H. unfold of_N in H.
destruct (N_lt_dec m bound). destruct (of_N_compare m) eqn:comp; try congruence.
- inversion H. unfold of_N_compare in comp.
- assumption. destruct (bound ?= m) eqn:comp'; congruence.
Qed. Qed.
Lemma of_nat_some {bound : N} {m : nat} {n : BoundedN bound} : Lemma of_nat_some {bound : N} {m : nat} {n : BoundedN bound} :
...@@ -184,7 +170,7 @@ Module BoundedN. ...@@ -184,7 +170,7 @@ Module BoundedN.
Qed. Qed.
Lemma of_nat_none {bound : N} {m : nat} : Lemma of_nat_none {bound : N} {m : nat} :
@of_nat bound m = None -> N.of_nat m >= bound. @of_nat bound m = None -> bound <= N.of_nat m.
Proof. apply of_N_none. Qed. Proof. apply of_N_none. Qed.
Lemma in_map_of_nat (bound : N) (n : BoundedN bound) (xs : list nat) : Lemma in_map_of_nat (bound : N) (n : BoundedN bound) (xs : list nat) :
...@@ -213,22 +199,34 @@ Module BoundedN. ...@@ -213,22 +199,34 @@ Module BoundedN.
Module Stdpp. Module Stdpp.
Import countable. Import countable.
Lemma eq_dec {bound : N} : EqDecision (BoundedN bound).
Proof.
intros x y.
destruct (BoundedN.eqb_spec x y); [left|right]; assumption.
Qed.
Global Instance BoundedNEqDec {bound : N} : EqDecision (BoundedN bound) := Global Instance BoundedNEqDec {bound : N} : EqDecision (BoundedN bound) :=
eq_dec. eq_dec.
Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound). Definition encode_bounded {bound : N} (n : BoundedN bound) : positive :=
encode (to_N n).
Definition decode_bounded {bound : N} (n : positive) : option (BoundedN bound) :=
decode n >>= of_N.
Lemma decode_encode_bounded {bound : N} (n : BoundedN bound) :
decode_bounded (encode_bounded n) = Some n.
Proof. Proof.
refine {| encode n := encode (to_N n); unfold decode_bounded, encode_bounded.
decode n := of_N =<< decode n; |}.
intros [x lt].
rewrite decode_encode. rewrite decode_encode.
simpl. simpl.
unfold of_N. apply of_to_N.
destruct (BoundedN.N_lt_dec x bound). Qed.
- assert (lt = l) by (apply UIP_dec; decide equality).
congruence. Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound) :=
- tauto. {| encode := encode_bounded;
Defined. decode := decode_bounded;
decode_encode := decode_encode_bounded; |}.
End Stdpp. End Stdpp.
Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) := Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
...@@ -261,7 +259,8 @@ Module BoundedN. ...@@ -261,7 +259,8 @@ Module BoundedN.
unfold to_nat. unfold to_nat.
destruct t as [t lt]. destruct t as [t lt].
simpl. simpl.
split; auto with *. change ((bound ?= t) = Gt) with (bound > t) in lt.
lia.
Qed. Qed.
End BoundedN. End BoundedN.
......
From Coq Require Import ProofIrrelevance. From Coq Require Import List.
From Coq Require Import ZArith. From Coq Require Import ZArith.
From stdpp Require gmap. From stdpp Require gmap.
From Coq Require Import List.
From SmartContracts Require Import Monads. From SmartContracts Require Import Monads.
From SmartContracts Require Import BoundedN.
Import ListNotations. Import ListNotations.
Notation FMap := gmap.gmap. Notation FMap := gmap.gmap.
......
...@@ -23,12 +23,11 @@ Global Instance LocalChainBaseTypes : ChainBaseTypes := ...@@ -23,12 +23,11 @@ Global Instance LocalChainBaseTypes : ChainBaseTypes :=
{| Address := BoundedN AddrSize; {| Address := BoundedN AddrSize;
address_eqb := BoundedN.eqb; address_eqb := BoundedN.eqb;
address_eqb_spec := BoundedN.eqb_spec; address_eqb_spec := BoundedN.eqb_spec;
address_encode := countable.encode;
address_decode := countable.decode;
address_decode_encode := countable.decode_encode;
compute_block_reward n := 50%Z; compute_block_reward n := 50%Z;
|}. |}.
Compute LocalChainBaseTypes.
Record LocalChain := Record LocalChain :=
build_local_chain { build_local_chain {
lc_header : BlockHeader; lc_header : BlockHeader;
......
...@@ -85,13 +85,33 @@ Section LocalBlockchainTests. ...@@ -85,13 +85,33 @@ Section LocalBlockchainTests.
Compute (account_balance chain4 baker). Compute (account_balance chain4 baker).
Compute (account_balance chain4 congress_1). Compute (account_balance chain4 congress_1).
(* Definition congress_ifc
Definition congress_ifc : ContractInterface Congress.Setup Congress.Msg Congress.State := : ContractInterface Congress.Setup Congress.Msg Congress.State :=
unpack_option match get_contract_interface
(get_contract_interface chain4 congress_1 Congress.Setup Congress.Msg Congress.State). chain4 congress_1
Congress.Setup Congress.Msg Congress.State with
| Some x => x
(* Using unpack_option here is extremely slow *)
| None =>
build_contract_interface
baker
0
setup
(fun c => None)
(fun a => deploy_congress)
(fun a m => deploy_congress)
end.
Definition congress_state chain := Definition congress_state chain : Congress.State :=
unpack_option (congress_ifc.(get_state) chain). match congress_ifc.(get_state) chain with
| Some s => s
(* And also here *)
| None => {| owner := baker;
state_rules := setup_rules;
proposals := FMap.empty;
next_proposal_id := 0;
members := FMap.empty |}
end.
Compute (congress_ifc.(get_state) chain4). Compute (congress_ifc.(get_state) chain4).
Compute (FMap.elements (congress_state chain4).(members)). Compute (FMap.elements (congress_state chain4).(members)).
...@@ -107,7 +127,7 @@ Section LocalBlockchainTests. ...@@ -107,7 +127,7 @@ Section LocalBlockchainTests.
[build_act person_1 (add_person person_1); build_act person_1 (add_person person_2)] [build_act person_1 (add_person person_1); build_act person_1 (add_person person_2)]
5 0). 5 0).
Eval cbn in (FMap.elements (congress_state chain5).(members)). Compute (FMap.elements (congress_state chain5).(members)).
Compute (account_balance chain5 congress_1). Compute (account_balance chain5 congress_1).
(* person_1 creates a proposal to send 3 coins to person_3 using funds (* person_1 creates a proposal to send 3 coins to person_3 using funds
...@@ -129,8 +149,11 @@ Section LocalBlockchainTests. ...@@ -129,8 +149,11 @@ Section LocalBlockchainTests.
congress_ifc.(call) 0 (vote_for_proposal 1). congress_ifc.(call) 0 (vote_for_proposal 1).
Definition chain7 : ChainBuilder := Definition chain7 : ChainBuilder :=
unpack_option unpack_option (
(chain6.(add_block) baker [(person_1, vote_proposal); (person_2, vote_proposal)]). chain6.(builder_add_block)
baker
[build_act person_1 vote_proposal; build_act person_2 vote_proposal]
7 0).
Compute (FMap.elements (congress_state chain7).(proposals)). Compute (FMap.elements (congress_state chain7).(proposals)).
...@@ -139,7 +162,11 @@ Section LocalBlockchainTests. ...@@ -139,7 +162,11 @@ Section LocalBlockchainTests.
congress_ifc.(call) 0 (finish_proposal 1). congress_ifc.(call) 0 (finish_proposal 1).
Definition chain8 : ChainBuilder := Definition chain8 : ChainBuilder :=
unpack_option (chain7.(add_block) baker [(person_3, finish_proposal)]). unpack_option (
chain7.(builder_add_block)
baker
[build_act person_3 finish_proposal]
8 0).
Compute (FMap.elements (congress_state chain8).(proposals)). Compute (FMap.elements (congress_state chain8).(proposals)).
(* Balances before: *) (* Balances before: *)
...@@ -149,5 +176,4 @@ Section LocalBlockchainTests. ...@@ -149,5 +176,4 @@ Section LocalBlockchainTests.
Compute (account_balance chain8 congress_1). Compute (account_balance chain8 congress_1).
Compute (account_balance chain8 person_3). Compute (account_balance chain8 person_3).
Print Assumptions chain8. Print Assumptions chain8.
*)
End LocalBlockchainTests. End LocalBlockchainTests.
...@@ -4,6 +4,7 @@ From SmartContracts Require Import Containers. ...@@ -4,6 +4,7 @@ From SmartContracts Require Import Containers.
From SmartContracts Require Import Automation. From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN. From SmartContracts Require Import BoundedN.
From Coq Require Import List. From Coq Require Import List.
From Coq Require Import String.
Import ListNotations. Import ListNotations.
...@@ -18,15 +19,20 @@ Inductive OakType := ...@@ -18,15 +19,20 @@ Inductive OakType :=
| oak_set : OakType -> OakType | oak_set : OakType -> OakType
| oak_map : OakType -> OakType -> OakType. | oak_map : OakType -> OakType -> OakType.
Definition eq_oak_type_dec (t1 t2 : OakType) : {t1 = t2} + {t1 <> t2}. Module OakType.
Proof. decide equality. Defined. Scheme Equality for OakType.
Definition eqb := OakType_beq.
Definition eq_dec := OakType_eq_dec.
Proposition eq_oak_type_dec_refl (x : OakType) : Fixpoint eqb_spec (a b : OakType) :
eq_oak_type_dec x x = left eq_refl. Bool.reflect (a = b) (eqb a b).
Proof. Proof.
induction x; destruct a, b; simpl in *; try (left; congruence); try (right; congruence).
try simpl; try rewrite IHx; try rewrite IHx1; try rewrite IHx2; reflexivity. 1, 2, 5: destruct (eqb_spec a1 b1), (eqb_spec a2 b2);
Qed. try (left; congruence); try (right; congruence).
1, 2: destruct (eqb_spec a b); try (left; congruence); try (right; congruence).
Qed.
End OakType.
Set Primitive Projections. Set Primitive Projections.
Record OakInterpretation := Record OakInterpretation :=
...@@ -76,11 +82,13 @@ Record OakValue := ...@@ -76,11 +82,13 @@ Record OakValue :=
Definition extract_oak_value (t : OakType) (value : OakValue) : option (interp_type t). Definition extract_oak_value (t : OakType) (value : OakValue) : option (interp_type t).
Proof. Proof.
destruct value as [ty val]. destruct value as [ty val].
destruct (eq_oak_type_dec t ty). destruct (OakType.eq_dec t ty).
- subst. exact (Some val). - subst. exact (Some val).
- exact None. - exact None.
Defined. Defined.
Compute OakType.eq_dec.
(* Defines that a type can be serialized into OakValue and deserialized from it, (* Defines that a type can be serialized into OakValue and deserialized from it,
and that these are inverses *) and that these are inverses *)
Class OakTypeEquivalence (ty : Type) := Class OakTypeEquivalence (ty : Type) :=
...@@ -90,8 +98,6 @@ Class OakTypeEquivalence (ty : Type) := ...@@ -90,8 +98,6 @@ Class OakTypeEquivalence (ty : Type) :=
deserialize_serialize : forall (x : ty), deserialize (serialize x) = Some x; deserialize_serialize : forall (x : ty), deserialize (serialize x) = Some x;
}. }.
Global Opaque serialize deserialize deserialize_serialize. Global Opaque serialize deserialize deserialize_serialize.
Program Instance oak_empty_equivalence : OakTypeEquivalence Empty_set := Program Instance oak_empty_equivalence : OakTypeEquivalence Empty_set :=
...@@ -150,7 +156,6 @@ Next Obligation. ...@@ -150,7 +156,6 @@ Next Obligation.
now rewrite countable.decode_encode. now rewrite countable.decode_encode.
Qed. Qed.
(* Program Instance generates an insane amount of obligations for sums, (* Program Instance generates an insane amount of obligations for sums,
so we define it by ourselves. *) so we define it by ourselves. *)
Section Sum. Section Sum.
......
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