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

Some preliminary work on proving LocalBlockchain is a chain

parent ed136fc6
From Coq Require Import ZArith.
From Coq Require Import Arith ZArith.
From Coq Require Import List.
From Coq Require Import PeanoNat.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
From SmartContracts Require Import Oak.
......@@ -309,7 +308,7 @@ Section Transfer.
outgoing_txs post from = tx :: outgoing_txs pre from.
Record TransferBase : Prop :=
build_transfer {
build_transfer_base {
amount_nonnegative : amount >= 0;
head_block_post : head_block post = head_block pre;
account_balance_pre_from_enough : account_balance pre from >= amount;
......
......@@ -217,18 +217,15 @@ Module BoundedN.
Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound).
Proof.
refine {| encode n := encode (proj1_sig n);
decode n := do n' <- (decode n : option N); _; |}.
Unshelve. all: cycle 1.
- destruct (N_lt_dec n' bound).
+ exact (Some (exist _ n' l)).
+ exact None.
- intros [x lt].
rewrite decode_encode.
simpl.
destruct (N_lt_dec x bound).
+ assert (lt = l) by (apply UIP_dec; decide equality).
now subst.
+ tauto.
decode n := of_N =<< decode n; |}.
intros [x lt].
rewrite decode_encode.
simpl.
unfold of_N.
destruct (BoundedN.N_lt_dec x bound).
- assert (lt = l) by (apply UIP_dec; decide equality).
congruence.
- tauto.
Qed.
End Stdpp.
......
......@@ -22,17 +22,44 @@ Module FMap.
Notation elements := fin_maps.map_to_list.
Notation size := stdpp.base.size.
Notation of_list := fin_maps.list_to_map.
Notation union := stdpp.base.union.
Proposition of_elements_eq
{A B : Type}
`{countable.Countable A}
(m : FMap A B)
: of_list (elements m) = m.
Proof.
apply fin_maps.list_to_map_to_list.
Qed.
Section Theories.
Context {K V : Type} `{countable.Countable K}.
Proposition of_elements_eq (m : FMap K V) :
of_list (elements m) = m.
Proof. apply fin_maps.list_to_map_to_list. Qed.
Lemma find_union_None (m1 m2 : FMap K V) (k : K) :
find k m1 = None ->
find k m2 = None ->
find k (union m1 m2) = None.
Proof.
intros find1 find2.
apply fin_maps.lookup_union_None; auto.
Qed.
Lemma find_union_Some_l (m1 m2 : FMap K V) (k : K) (v : V) :
find k m1 = Some v ->
find k (union m1 m2) = Some v.
Proof. apply fin_maps.lookup_union_Some_l. Qed.
Lemma find_add (m : FMap K V) (k : K) (v : V) :
find k (add k v m) = Some v.
Proof. apply fin_maps.lookup_insert. Qed.
Lemma find_add_ne (m : FMap K V) (k k' : K) (v : V) :
k <> k' -> find k' (add k v m) = find k' m.
Proof. apply fin_maps.lookup_insert_ne. Qed.
End Theories.
End FMap.
Hint Resolve FMap.find_union_None.
Hint Resolve FMap.find_union_Some_l.
Hint Resolve FMap.find_add.
Hint Resolve FMap.find_add_ne.
Instance empty_set_eq_dec : stdpp.base.EqDecision Empty_set.
Proof. decidable.solve_decision. Defined.
Program Instance empty_set_countable : countable.Countable Empty_set :=
......
From Coq Require Import ZArith.
From Coq Require Import Arith ZArith.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
......@@ -8,6 +8,7 @@ From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
From Coq Require Import Psatz.
From stdpp Require countable.
Import RecordSetNotations.
......@@ -86,12 +87,12 @@ Definition lc_head_block (lc : LocalChain) : Block :=
end.
Definition lc_incoming_txs (lc : LocalChain) (addr : Address) : list Tx :=
let all_txs := flat_map (fun u => u.(upd_txs)) lc.(lc_updates) in
let all_txs := flat_map upd_txs lc.(lc_updates) in
let is_inc tx := (tx.(tx_to) =? addr)%address in
filter is_inc all_txs.
Definition lc_outgoing_txs (lc : LocalChain) (addr : Address) : list Tx :=
let all_txs := flat_map (fun u => u.(upd_txs)) lc.(lc_updates) in
let all_txs := flat_map upd_txs lc.(lc_updates) in
let is_out tx := (tx.(tx_from) =? addr)%address in
filter is_out all_txs.
......@@ -118,11 +119,6 @@ Record LocalChainBuilder :=
build_local_chain_builder {
lcb_lc : LocalChain;
lcb_contracts : FMap Address WeakContract;
(*
lcb_trace : ChainTrace
(build_env lc_initial_chain (fun a => None))
(build_env lcb_lc lcb_contracts);
*)
}.
Instance eta_local_chain_builder : Settable _ :=
......@@ -134,75 +130,56 @@ Definition initial_chain_builder : LocalChainBuilder :=
{| lcb_lc := lc_initial_chain;
lcb_contracts := FMap.empty |}.
Definition lcb_env (lcb : LocalChainBuilder) : Environment :=
build_env lcb.(lcb_lc) (fun a => FMap.find a lcb.(lcb_contracts)).
Section ExecuteActions.
Context (initial_lcb : LocalChainBuilder)
(initial_acts : list ExternalAction).
Definition lcb_env (lcb : LocalChainBuilder) : Environment :=
build_env lcb.(lcb_lc) (fun a => FMap.find a lcb.(lcb_contracts)).
Local Coercion lcb_env : LocalChainBuilder >-> Environment.
Record ExecutionContext :=
build_execution_context {
block_txs : list Tx;
new_update : ChainUpdate;
cur_env : Environment;
new_contracts : FMap Address WeakContract;
acts_stack : list ExternalAction;
trace : BlockTrace initial_lcb cur_env initial_acts acts_stack;
}.
Instance eta_execution_context : Settable _ :=
mkSettable
((constructor build_execution_context) <*> block_txs
<*> new_update
<*> cur_env
<*> acts_stack
<*> trace)%settable.
(*
Definition merge_contracts (m : FMap Address WeakContract) (l : list InternalAction)
: FMap Address WeakContract :=
let go (iact : InternalAction)
(m : FMap Address WeakContract) : FMap Address WeakContract :=
match iact.(iact_body) with
| iact_deploy wc _ => FMap.add iact.(iact_to) wc m
| _ => m
end in
fold_right go m l.
*)
<*> new_contracts
<*> acts_stack)%settable.
Definition verify_amount (c : LocalChain) (addr : Address) (amt : Amount)
: option unit :=
if ((amt >=? 0) && (amt <=? account_balance c addr))%Z
then Some tt
else None.
Definition make_lcb (ec : ExecutionContext) : LocalChainBuilder :=
let lc := initial_lcb.(lcb_lc)[[lc_updates ::= cons ec.(new_update)]] in
initial_lcb[[lcb_lc := lc]][[lcb_contracts ::= FMap.union ec.(new_contracts)]].
Definition count_contract_deployments (lcb : LocalChainBuilder) : nat :=
FMap.size lcb.(lcb_contracts).
Definition verify_no_txs (addr : Address) (c : LocalChain) : option unit :=
match incoming_txs c addr with
| _ :: _ => None
| [] => Some tt
end.
Local Open Scope Z.
Definition add_step
(from to : Address)
(amount : Amount)
(body : InternalActionBody)
(body : TxBody)
(record : bool)
(ec : ExecutionContext)
: ExecutionContext :=
let iact := {| iact_from := from;
iact_to := to;
iact_amount := amount;
iact_body := body; |} in
let new_cu := ec.(new_update)[[upd_txs ::= cons (iact : Tx)]] in
: option ExecutionContext :=
let lcb := make_lcb ec in
do if amount <? 0 then None else Some tt;
do if amount >? account_balance lcb from then None else Some tt;
let tx := build_tx from to amount body in
let new_cu := ec.(new_update)[[upd_txs ::= cons tx]] in
let new_ec := ec[[new_update := new_cu]]
[[new_iacts ::= cons iact]]
[[recorded_iacts ::= if record then cons iact else id]] in
new_ec.
[[block_txs ::= if record then cons tx else id]] in
(* todo: invariant *)
do if account_balance (make_lcb new_ec) to <? amount then None else Some tt;
Some new_ec.
Definition update_contract_state
(addr : Address)
......@@ -212,21 +189,32 @@ Section ExecuteActions.
let new_ec := ec[[new_update := new_cu]] in
new_ec.
Definition add_new_contract
(addr : Address)
(wc : WeakContract)
(ec : ExecutionContext) : ExecutionContext :=
ec[[new_contracts ::= FMap.add addr wc]].
Definition deploy_contract
(from : Address)
(amount : Amount)
(wc : WeakContract)
(setup : OakValue)
(ec : ExecutionContext)
(record : bool)
(ec : ExecutionContext)
: option ExecutionContext :=
let lcb := make_acc ec in
do verify_amount lcb from amount;
let num := 1 + count_contract_deployments lcb in
let lcb := make_lcb ec in
let num := (1 + count_contract_deployments lcb)%nat in
do contract_addr <- BoundedN.of_nat num;
do verify_no_txs contract_addr lcb;
let ec := add_step from contract_addr amount (iact_deploy wc setup) record ec in
let lcb := make_acc ec in
do if (length (incoming_txs lcb contract_addr) =? 0)%nat then Some tt else None;
(* todo: invariant from above line *)
do match env_contracts lcb contract_addr with
| Some _ => None
| None => Some tt
end;
let body := tx_deploy (build_contract_deployment (wc_version wc) setup) in
do ec <- add_step from contract_addr amount body record ec;
let lcb := make_lcb ec in
let ctx := {| ctx_chain := lcb;
ctx_from := from;
ctx_contract_address := contract_addr;
......@@ -234,8 +222,203 @@ Section ExecuteActions.
let (ver, init, recv) := wc in
do state <- init ctx setup;
let ec := update_contract_state contract_addr state ec in
let ec := add_new_contract contract_addr wc ec in
Some ec.
Ltac mini_solver :=
repeat
(match goal with
| [H: context[Z.ltb ?a ?b] |- _] => destruct (Z.ltb_spec a b)
| [H: context[Z.gtb ?a ?b] |- _] => destruct (Z.gtb_spec a b)
| [H: context[BoundedN.eqb ?a ?b] |- _] => destruct (BoundedN.eqb_spec a b)
| [H: context[Nat.eqb ?a ?b] |- _] => destruct (Nat.eqb_spec a b)
| [H: context[do _ <- ?b; _] |- _] => destruct b eqn:?
| [H: Some ?a = Some ?b |- _] => inversion H; subst; clear H
| [H: context[match ?a with | Some _ => _ | None => _ end] |- _] =>
destruct a eqn:?
| [H: FMap.find _ (FMap.union _ _) = None |- _] =>
apply fin_maps.lookup_union_None in H
| [H: _ /\ _ |- _] => destruct H
| [|- context[?a <? ?b] ] => destruct (Z.ltb_spec a b)
| [|- context[?a >? ?b] ] => destruct (Z.gtb_spec a b)
| [|- context[BoundedN.eqb ?a ?b] ] => destruct (BoundedN.eqb_spec a b)
| [|- context[do _ <- ?b; _] ] => destruct b eqn:?
| _ => idtac
end;
intros;
simpl in *;
eauto;
try congruence;
try lia).
Lemma add_step_sound from to amount body record ec new_ec :
add_step from to amount body record ec = Some new_ec ->
TransferBase (make_lcb ec) (make_lcb new_ec) from to amount.
Proof.
unfold add_step.
repeat
match goal with
| [|- TransferBase _ _ _ _ _] => apply build_transfer_base
| _ =>
unfold constructor, lc_head_block, lc_incoming_txs, lc_outgoing_txs in *;
mini_solver
end.
Qed.
Hint Resolve add_step_sound.
Lemma add_step_incoming_txs from to amount body record ec new_ec lc new_lc :
add_step from to amount body record ec = Some new_ec ->
lc = (make_lcb ec).(lcb_lc) ->
new_lc = (make_lcb new_ec).(lcb_lc) ->
lc_incoming_txs new_lc to = build_tx from to amount body :: lc_incoming_txs lc to.
Proof.
unfold add_step.
repeat
(unfold lc_incoming_txs, lc_outgoing_txs in *;
mini_solver).
Qed.
Lemma add_step_outgoing_txs from to amount body record ec new_ec :
add_step from to amount body record ec = Some new_ec ->
outgoing_txs (make_lcb new_ec) from =
build_tx from to amount body :: outgoing_txs (make_lcb ec) from.
Proof.
unfold add_step.
repeat
(unfold lc_incoming_txs, lc_outgoing_txs in *;
mini_solver).
Qed.
Lemma add_step_new_contracts {from to amount body record ec new_ec} :
add_step from to amount body record ec = Some new_ec ->
new_contracts new_ec = new_contracts ec.
Proof.
unfold add_step.
mini_solver.
Qed.
Hint Resolve add_step_incoming_txs.
Hint Resolve add_step_outgoing_txs.
Hint Resolve add_step_new_contracts.
Lemma update_contract_state_respects_transfer
addr state lcb ec from to amount :
TransferBase lcb (make_lcb ec) from to amount ->
TransferBase
lcb
(make_lcb (update_contract_state addr state ec))
from to amount.
Proof.
intros [].
apply build_transfer_base; auto.
Qed.
Hint Resolve update_contract_state_respects_transfer.
Lemma add_new_contract_respects_transfer
addr wc lcb ec from to amount :
TransferBase lcb (make_lcb ec) from to amount ->
TransferBase
lcb
(make_lcb (add_new_contract addr wc ec))
from to amount.
Proof.
intros [].
apply build_transfer_base; auto.
Qed.
Hint Resolve add_new_contract_respects_transfer.
Lemma update_contract_state_respects_incoming_txs
caddr state ec addr :
incoming_txs (make_lcb (update_contract_state caddr state ec)) addr =
incoming_txs (make_lcb ec) addr.
Proof. reflexivity. Qed.
Lemma update_contract_state_respects_outgoing_txs
caddr state ec addr :
outgoing_txs (make_lcb (update_contract_state caddr state ec)) addr =
outgoing_txs (make_lcb ec) addr.
Proof. reflexivity. Qed.
Lemma add_new_contract_respects_incoming_txs
caddr wc ec addr :
incoming_txs (make_lcb (add_new_contract caddr wc ec)) addr =
incoming_txs (make_lcb ec) addr.
Proof. reflexivity. Qed.
Lemma add_new_contract_respects_outgoing_txs
caddr wc ec addr :
outgoing_txs (make_lcb (add_new_contract caddr wc ec)) addr =
outgoing_txs (make_lcb ec) addr.
Proof. reflexivity. Qed.
Lemma list_nil_if_length_0 {A : Type} (xs : list A) :
length xs = 0%nat ->
xs = [].
Proof.
intros length_xs.
destruct xs; prove.
Qed.
Hint Resolve list_nil_if_length_0.
Lemma find_union_diff_l
(m1 m2 m3 : FMap Address WeakContract)
(k : Address) :
FMap.find k m1 = FMap.find k m2 ->
FMap.find k (FMap.union m1 m3) = FMap.find k (FMap.union m2 m3).
Proof.
intros H.
now rewrite fin_maps.lookup_union, H, <- fin_maps.lookup_union.
Qed.
Hint Resolve find_union_diff_l.
Lemma deploy_contract_sound from amount wc setup record ec new_ec :
deploy_contract from amount wc setup record ec = Some new_ec ->
exists to, DeployTransfer
(make_lcb ec) (make_lcb new_ec)
from to amount wc setup.
Proof.
unfold deploy_contract.
destruct wc.
repeat
match goal with
| [contract_addr: BoundedN AddrSize |- exists _, _] => exists contract_addr
| [|- DeployTransfer _ _ _ _ _ _ _] => apply build_deploy_transfer
| [|- IncomingTxRecorded _ _ _ _] =>
unfold IncomingTxRecorded;
rewrite add_new_contract_respects_incoming_txs;
rewrite update_contract_state_respects_incoming_txs;
eauto
| [|- OutgoingTxRecorded _ _ _ _] =>
unfold OutgoingTxRecorded;
rewrite add_new_contract_respects_outgoing_txs;
rewrite update_contract_state_respects_outgoing_txs;
eauto
| [H: add_step _ _ _ _ _ _ = Some ?new_ec |- context[new_contracts ?new_ec] ] =>
rewrite (add_step_new_contracts H)
| _ =>
mini_solver
end.
- unfold lc_contract_state.
simpl.
rewrite FMap.find_add.
replace (new_contracts e0) with (new_contracts ec).
apply find_union_diff_l.
rewrite FMap.find_add_ne by auto.
rewrite fin_maps.lookup_insert_ne.
debug auto.
apply FMap.find_union_Some_l.
apply fin_maps.lookup_union_Some_l.
apply fin_maps.lookup_insert.
Definition send_or_call
(from to : Address)
(amount : Amount)
......@@ -370,7 +553,7 @@ Section ExecuteActions.
match goal with
| [|- context[@cons InternalAction ?x] ] => exists x
end.
apply build_transfer; simpl; auto.
apply build_transfer_base; simpl; auto.
* unfold account_balance; simpl.
unfold lc_incoming_txs, lc_outgoing_txs; simpl.
simplify.
......
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