...
 
Commits (24)
......@@ -11,6 +11,8 @@
*~
CoqMakefile
CoqMakefile.conf
CoqMakefile.plugin
CoqMakefile.plugin.conf
Makefile.coq
Makefile.coq.conf
execution/CoqMakefile
......@@ -31,3 +33,7 @@ execution/CoqMakefile.conf
doc/
docs/
_opam/
## extraction output
*.liq
*.out
\ No newline at end of file
SED = `which gsed || which sed`
EXTRA_DIR:=extra
DOCS_DIR:=docs
COQDOCFLAGS:= \
......@@ -6,14 +7,24 @@ COQDOCFLAGS:= \
--with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
export COQDOCFLAGS
COQMAKEFILE:=CoqMakefile
PLUGINMAKEFILE:=CoqMakefile.plugin
COQ_PROJ:=_CoqProject
PLUGIN_PROJ:=_PluginProject
default: code
default: code # plugin
all: code html
all: code html # plugin
plugin: $(PLUGINMAKEFILE)
$(MAKE) -f $(PLUGINMAKEFILE)
cleanplugin: $(PLUGINMAKEFILE)
@$(MAKE) -f $(PLUGINMAKEFILE) clean
rm -f $(PLUGINMAKEFILE)
code: $(COQMAKEFILE)
$(MAKE) -f $(COQMAKEFILE)
# ./clean_extraction.sh
clean: $(COQMAKEFILE)
@$(MAKE) -f $(COQMAKEFILE) $@
......@@ -28,6 +39,10 @@ html: $(COQMAKEFILE)
$(COQMAKEFILE): $(COQ_PROJ)
coq_makefile -f $(COQ_PROJ) -o $@
$(PLUGINMAKEFILE): $(PLUGIN_PROJ)
coq_makefile -f $(PLUGIN_PROJ) -o $@ $(DEPS)
$(SED) -i -e s/coqdeps/coqdeps.plugin/g $(PLUGINMAKEFILE)
%: $(COQMAKEFILE) force
@$(MAKE) -f $(COQMAKEFILE) $@
force $(COQ_PROJ): ;
......
......@@ -19,7 +19,6 @@ Then MetaCoq and bignums:
```bash
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-metacoq.1.0~alpha+8.11
opam install coq-bignums
```
And std++:
......@@ -29,6 +28,8 @@ opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-stdpp
```
Install MetaCoq from this [MetaCoq's fork](https://github.com/annenkov/template-coq/tree/coq-8.11-erase-annotated). Follow the instructions from the [official MetaCoq repo](https://github.com/MetaCoq/metacoq#installing-from-github-repository-for-developers).
After completing the procedures above, run `make` to build the development, and
`make html` to build the documentation. The documentation will be located in the
docs folder after `make html`.
......@@ -40,7 +41,7 @@ The [embedding](embedding/) folder contains the development of the embedding.
The [execution](execution/) folder contains the formalization of the smart
contract execution layer, which allows reasoning about interacting contracts.
The [extraction](extraction/) folder contains a printing procedure for the deep embedding into the Liquidity syntax. For extraction using MetaCoq's **certified erasure** see the [extract-cert](https://github.com/AU-COBRA/ConCert/tree/extract-cert) branch (requires [MetaCoq's fork](https://github.com/annenkov/template-coq) to compile).
The [extraction](extraction/) folder contains two versions of extraction. The first one is a printing procedure from the deep embedding into the Liquidity syntax. The second one is based on MetaCoq's **certified erasure**.
## Notes for developers
......
......@@ -26,6 +26,7 @@ execution/theories/Extras.v
execution/theories/Finite.v
execution/theories/LocalBlockchain.v
execution/theories/Monads.v
execution/theories/ResultMonad.v
execution/theories/Serializable.v
-Q embedding/theories ConCert.Embedding
......@@ -56,6 +57,11 @@ embedding/examples/SimpleBlockchain.v
-Q extraction/theories ConCert.Extraction
extraction/theories/Liquidity.v
extraction/theories/LPretty.v
extraction/theories/Certified.v
extraction/theories/Extra.v
# extraction/theories/Extraction.v
-Q extraction/examples ConCert.Extraction.Examples
extraction/examples/Prelude.v
......@@ -63,8 +69,13 @@ extraction/examples/Counter.v
extraction/examples/SimpleBlockchain.v
extraction/examples/crowdfunding_extract/CrowdfundingData.v
extraction/examples/crowdfunding_extract/Crowdfunding.v
extraction/examples/CounterCertifiedExtraction.v
extraction/examples/CrowdfundingCertifiedExtraction.v
extraction/examples/CounterDepCertifiedExtraction.v
extraction/examples/CounterRefinementTypes.v
extraction/examples/StackInterpreter.v
embedding/theories/pcuic/PCUICCorrectness.v
embedding/theories/pcuic/PCUICCorrectnessAux.v
embedding/theories/pcuic/PCUICFacts.v
embedding/theories/pcuic/PCUICFacts.v
\ No newline at end of file
-R extraction/theories/ ConCert.Extraction
-I extraction/src
extraction/src/all_Forall.ml
extraction/src/all_Forall.mli
extraction/src/ascii.ml
extraction/src/ascii.mli
extraction/src/ast0.ml
extraction/src/ast0.mli
extraction/src/astUtils.ml
extraction/src/astUtils.mli
extraction/src/basicAst.ml
extraction/src/basicAst.mli
extraction/src/basics.ml
extraction/src/basics.mli
extraction/src/binInt.ml
extraction/src/binInt.mli
extraction/src/binNat.ml
extraction/src/binNat.mli
extraction/src/binNums.ml
extraction/src/binNums.mli
extraction/src/binPos.ml
extraction/src/binPos.mli
extraction/src/bool.ml
extraction/src/bool.mli
extraction/src/byte.ml
extraction/src/byte.mli
extraction/src/classes0.ml
extraction/src/classes0.mli
extraction/src/compare_dec.ml
extraction/src/compare_dec.mli
extraction/src/config0.ml
extraction/src/config0.mli
extraction/src/datatypes.ml
extraction/src/datatypes.mli
extraction/src/eAst.ml
extraction/src/eAst.mli
extraction/src/eAstUtils.ml
extraction/src/eAstUtils.mli
extraction/src/eLiftSubst.ml
extraction/src/eLiftSubst.mli
extraction/src/environment.ml
extraction/src/environment.mli
extraction/src/ePretty.ml
extraction/src/ePretty.mli
extraction/src/eqDecInstances.ml
extraction/src/eqDecInstances.mli
extraction/src/eqdepFacts.ml
extraction/src/eqdepFacts.mli
extraction/src/equalities.ml
extraction/src/equalities.mli
extraction/src/erasureFunction.ml
extraction/src/erasureFunction.mli
extraction/src/eTyping.ml
extraction/src/eTyping.mli
extraction/src/extract.ml
extraction/src/extract.mli
extraction/src/init.ml
extraction/src/init.mli
extraction/src/liftSubst.ml
extraction/src/liftSubst.mli
extraction/src/list0.ml
extraction/src/list0.mli
extraction/src/mCCompare.ml
extraction/src/mCCompare.mli
extraction/src/mCList.ml
extraction/src/mCList.mli
extraction/src/mCOption.ml
extraction/src/mCOption.mli
extraction/src/mCProd.ml
extraction/src/mCProd.mli
extraction/src/mCString.ml
extraction/src/mCString.mli
extraction/src/monad_utils.ml
extraction/src/monad_utils.mli
extraction/src/mSetDecide.ml
extraction/src/mSetDecide.mli
extraction/src/mSetFacts.ml
extraction/src/mSetFacts.mli
extraction/src/mSetInterface.ml
extraction/src/mSetInterface.mli
extraction/src/mSetList.ml
extraction/src/mSetList.mli
extraction/src/mSetProperties.ml
extraction/src/mSetProperties.mli
extraction/src/mSetWeakList.ml
extraction/src/mSetWeakList.mli
extraction/src/nat0.ml
extraction/src/nat0.mli
extraction/src/ordersFacts.ml
extraction/src/ordersFacts.mli
extraction/src/ordersLists.ml
extraction/src/ordersLists.mli
extraction/src/orders.ml
extraction/src/orders.mli
extraction/src/ordersTac.ml
extraction/src/ordersTac.mli
extraction/src/pCUICAst.ml
extraction/src/pCUICAst.mli
extraction/src/pCUICAstUtils.ml
extraction/src/pCUICAstUtils.mli
extraction/src/pCUICChecker.ml
extraction/src/pCUICChecker.mli
extraction/src/pCUICCumulativity.ml
extraction/src/pCUICCumulativity.mli
extraction/src/pCUICEquality.ml
extraction/src/pCUICEquality.mli
extraction/src/pCUICLiftSubst.ml
extraction/src/pCUICLiftSubst.mli
extraction/src/pCUICNormal.ml
extraction/src/pCUICNormal.mli
extraction/src/pCUICPosition.ml
extraction/src/pCUICPosition.mli
extraction/src/pCUICPretty.ml
extraction/src/pCUICPretty.mli
extraction/src/pCUICReflect.ml
extraction/src/pCUICReflect.mli
extraction/src/pCUICSafeChecker.ml
extraction/src/pCUICSafeChecker.mli
extraction/src/pCUICSafeConversion.ml
extraction/src/pCUICSafeConversion.mli
extraction/src/pCUICSafeLemmata.ml
extraction/src/pCUICSafeLemmata.mli
extraction/src/pCUICSafeReduce.ml
extraction/src/pCUICSafeReduce.mli
extraction/src/pCUICSafeRetyping.ml
extraction/src/pCUICSafeRetyping.mli
extraction/src/pCUICTyping.ml
extraction/src/pCUICTyping.mli
extraction/src/pCUICUnivSubst.ml
extraction/src/pCUICUnivSubst.mli
extraction/src/peanoNat.ml
extraction/src/peanoNat.mli
extraction/src/pretty.ml
extraction/src/pretty.mli
extraction/src/safeErasureFunction.ml
extraction/src/safeErasureFunction.mli
extraction/src/safeTemplateChecker.ml
extraction/src/safeTemplateChecker.mli
extraction/src/safeTemplateErasure.ml
extraction/src/safeTemplateErasure.mli
extraction/src/specif.ml
extraction/src/specif.mli
extraction/src/ssrbool.ml
extraction/src/ssrbool.mli
extraction/src/string0.ml
extraction/src/string0.mli
extraction/src/templateToPCUIC.ml
extraction/src/templateToPCUIC.mli
extraction/src/typing0.ml
extraction/src/typing0.mli
extraction/src/uGraph0.ml
extraction/src/uGraph0.mli
extraction/src/universes0.ml
extraction/src/universes0.mli
extraction/src/univSubst0.ml
extraction/src/univSubst0.mli
extraction/src/utils.ml
extraction/src/utils.mli
extraction/src/wGraph.ml
extraction/src/wGraph.mli
extraction/src/main.ml
extraction/src/main.mli
extraction/src/g_concert_extract.mlg
extraction/src/concert_extract_plugin.mlpack
# extraction/theories/Loader.v
\ No newline at end of file
#!/bin/bash
SED=`which gsed || which sed`
echo "Cleaning result of extraction"
cd extraction
if [ ! -d "src" ]
then
mkdir src
fi
shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
# files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | $SED -e s/gen-src/src/`
if [[ ! -f "src/concert_extract_plugin.cmxs" ||
"src/concert_extract_plugin.cmxs" -ot "theories/Extraction.vo" ]]
then
cd src
# Move extracted modules to build the plugin
# Uncapitalize modules to circumvent a bug of coqdep with mllib files
for i in *.ml*
do
newi=`echo $i | cut -b 1 | tr '[:upper:]' '[:lower:]'``echo $i | cut -b 2-`;
echo "Moving " $i "to" $newi;
mv $i $newi;
done
cd ..
# Remove extracted modules already linked in template_coq_plugin, checker and pcuic.
# echo "Removing:" $files
# rm -f $files
else
echo "Extraction up-to date"
fi
......@@ -12,7 +12,7 @@ Require Import Morphisms.
Require Import Permutation.
Require Import Program.Tactics.
From ConCert.Execution Require Import Blockchain Congress Automation Extras.
From ConCert.Execution Require Import Blockchain Congress Automation Extras ResultMonad.
Import ListNotations.
......@@ -519,7 +519,7 @@ Qed.
Corollary cf_backed_after_block {ChainBuilder : ChainBuilderType}
prev hd acts new cf_addr lstate :
builder_add_block prev hd acts = Some new ->
builder_add_block prev hd acts = Ok new ->
env_contracts new cf_addr = Some (cf_contract : WeakContract) ->
cf_state new cf_addr = Some lstate ->
(account_balance (env_chain new) cf_addr >= balance_coq lstate)%Z.
......@@ -537,7 +537,7 @@ Qed.
(** ** The actual contract balance is consistent with the sum of individual contributions *)
Corollary cf_donations_backed_after_block {ChainBuilder : ChainBuilderType}
prev hd acts new cf_addr lstate :
builder_add_block prev hd acts = Some new ->
builder_add_block prev hd acts = Ok new ->
env_contracts new cf_addr = Some (cf_contract : WeakContract) ->
cf_state new cf_addr = Some lstate ->
~~ lstate.(done_coq) ->
......
......@@ -27,7 +27,7 @@ Fixpoint mkNames (ns : list string) (suffix : string) :=
match ns with
| [] => tmPrint "Done."
| n :: ns' => n' <- tmEval all (n ++ suffix)%string ;;
str <- tmQuote n';;
str <- tmQuote n' ;;
tmMkDefinition n str;;
mkNames ns' suffix
end.
......@@ -206,4 +206,4 @@ Section MapEval.
Ok (vConstr Maybe "JustAcorn" [vTy (tyInd Nat); vConstr Nat "Z" []]).
Proof. compute. reflexivity. Qed.
End MapEval.
\ No newline at end of file
End MapEval.
......@@ -67,7 +67,7 @@ Section WcbvEvalProp.
Lemma mkApps_unfold t1 ts t2 :
mkApps t1 (ts ++ [t2]) = tApp (mkApps t1 ts) t2.
Proof.
now rewrite <- PCUICAstUtils.mkApps_nested.
now rewrite <- mkApps_nested.
Qed.
Lemma mkApps_eq_false t1 t2 args :
......@@ -744,7 +744,7 @@ Proof.
specialize (Forall_In _ _ _ Hin'' H) as Hfa'. simpl in Hfa'. easy.
* trivial.
+ simpl in *.
rewrite Bool.andb_true_r in *. unfold PCUICAstUtils.test_def. simpl.
rewrite Bool.andb_true_r in *. unfold test_def. simpl.
repeat rewrite Bool.andb_true_iff in *.
repeat split;eauto with hints;
try apply type_to_term_closed;intuition.
......@@ -963,7 +963,7 @@ Proof.
* reflexivity.
+ (* eFix *)
cbn in *. unfold is_true in *;repeat rewrite Bool.andb_true_iff in *.
unfold PCUICAstUtils.map_def. simpl. repeat f_equal;intuition.
unfold map_def. simpl. repeat f_equal;intuition.
rewrite commut_lift_subst. intuition. rewrite commut_lift_subst. intuition.
+ (* eTy *) simpl in *. eauto with hints.
Qed.
......
......@@ -26,4 +26,5 @@ theories/Extras.v
theories/Finite.v
theories/LocalBlockchain.v
theories/Monads.v
theories/ResultMonad.v
theories/Serializable.v
......@@ -64,11 +64,12 @@ From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
Require Import Serializable.
Require Import Monads.
Require Import Extras.
Require Import Automation.
Require Import ChainedList.
Require Import Extras.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.
......@@ -1860,6 +1861,23 @@ End Theories.
End Trace.
End Semantics.
Inductive ActionEvaluationError :=
| amount_negative (* amount is negative *)
| amount_too_high (* sender does not have enough money *)
| no_such_contract (* there is not contract at that address *)
| too_many_contracts (* cannot generate fresh address for new contract *)
| init_failed (* contract init function failed *)
| receive_failed (* contract receive function failed *)
| internal_error. (* unexpected internal error *)
Inductive AddBlockError :=
| invalid_header (* header for next block is invalid *)
| invalid_root_action (act : Action) (* a specified root action is invalid *)
| action_evaluation_depth_exceeded (* out of fuel while evaluating actions recursively *)
| action_evaluation_error (* error when evaluating single action *)
(act : Action)
(err : ActionEvaluationError).
Class ChainBuilderType :=
build_builder {
builder_type : Type;
......@@ -1872,7 +1890,7 @@ Class ChainBuilderType :=
(builder : builder_type)
(header : BlockHeader)
(actions : list Action) :
option builder_type;
result builder_type AddBlockError;
builder_trace (builder : builder_type) :
ChainTrace empty_state (build_chain_state (builder_env builder) []);
......
......@@ -40,6 +40,11 @@ Module FMap.
Section Theories.
Context {K V : Type} `{countable.Countable K}.
Lemma ext_eq (m1 m2 : FMap K V) :
(forall k, FMap.find k m1 = FMap.find k m2) ->
m1 = m2.
Proof. apply fin_maps.map_eq. Qed.
Lemma of_elements_eq (m : FMap K V) :
of_list (elements m) = m.
Proof. apply fin_maps.list_to_map_to_list. Qed.
......
......@@ -9,6 +9,7 @@ Require Import Containers.
Require Import Extras.
Require Import LocalBlockchain.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
Import ListNotations.
......@@ -112,7 +113,7 @@ Definition deploy_setup :=
registration_deposit := 0; |}.
Local Open Scope list.
Definition boardroom_example :=
Definition boardroom_example : option nat :=
let chain : ChainBuilder := builder_initial in
let creator : Address := A 10 in
let add_block (chain : ChainBuilder) (acts : list Action) :=
......@@ -122,11 +123,11 @@ Definition boardroom_example :=
block_finalized_height := finalized_height chain;
block_creator := creator;
block_reward := 50; |} in
builder_add_block chain next_header acts in
option_of_result (builder_add_block chain next_header acts) in
do chain <- add_block chain [];
let dep := build_act creator (create_deployment 0 (boardroom_voting hash_func) deploy_setup) in
do chain <- add_block chain [dep];
do caddr <- hd None (map Some (FMap.keys (lc_contracts (lcb_lc chain))));
do caddr <- hd_error (FMap.keys (lc_contracts (lcb_lc chain)));
let send addr m := build_act addr (act_call caddr 0 (serialize m)) in
let calls := map (fun '(addr, m) => send addr m) (zip addrs signups) in
do chain <- add_block chain calls;
......@@ -135,6 +136,6 @@ Definition boardroom_example :=
let tally := build_act creator (act_call caddr 0 (serialize tally_votes)) in
do chain <- add_block chain [tally];
do state <- @contract_state _ (@State _ Z) _ (lcb_lc chain) caddr;
result state.
BoardroomVoting.result state.
Check (@eq_refl (option nat) (Some votes_for)) <<: boardroom_example = Some votes_for.
......@@ -8,13 +8,14 @@ From Coq Require Import ZArith.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
Require Import Automation.
Require Import Blockchain.
Require Import Serializable.
Require Import Monads.
Require Import ChainedList.
Require Import Containers.
Require Import Automation.
Require Import Extras.
Require Import ChainedList.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -528,7 +529,7 @@ Qed.
Corollary congress_txs_after_block
{ChainBuilder : ChainBuilderType}
prev new header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......
......@@ -9,13 +9,15 @@ From Coq Require Import ZArith.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Permutation.
Require Import Automation.
Require Import Blockchain.
Require Import Serializable.
Require Import Monads.
Require Import BoundedN.
Require Import ChainedList.
Require Import Containers.
Require Import Automation.
Require Import Extras.
Require Import BoundedN.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -353,7 +355,7 @@ Section Theories.
block_creator := creator;
block_reward := 50; |} in
let acts := map (build_act creator) act_bodies in
builder_add_block chain next_header acts in
option_of_result (builder_add_block chain next_header acts) in
(* Get some money on the creator *)
do chain <- add_block chain [];
(* Deploy congress and exploit contracts *)
......
......@@ -23,6 +23,7 @@ Require Import Automation.
Require Import Blockchain.
Require Import Extras.
Require Import Monads.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
......@@ -583,7 +584,7 @@ Section Theories.
Corollary escrow_correct
{ChainBuilder : ChainBuilderType}
prev new header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
let trace := builder_trace new in
forall caddr,
env_contracts new caddr = Some (Escrow.contract : WeakContract) ->
......
......@@ -10,6 +10,7 @@ Require Import Congress.
Require Import Containers.
Require Import BoundedN.
Require Import Extras.
Require Import ResultMonad.
Require Import Serializable.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -36,7 +37,7 @@ Section LocalBlockchainTests.
Definition chain1 : ChainBuilder := builder_initial.
Definition add_block (chain : ChainBuilder) acts : option ChainBuilder :=
Definition add_block (chain : ChainBuilder) acts : result ChainBuilder AddBlockError :=
let header :=
{| block_height := S (chain_height chain);
block_slot := S (current_slot chain);
......@@ -45,16 +46,25 @@ Section LocalBlockchainTests.
block_reward := 50; |} in
builder_add_block chain header acts.
Definition unpack_result {T E} (r : result T E) :=
match r return match r with
| Ok _ => T
| Err _ => E
end with
| Ok t => t
| Err e => e
end.
(* Creator created an empty block (and gets some coins) *)
Definition chain2 : ChainBuilder :=
unpack_option (add_block chain1 []).
unpack_result (add_block chain1 []).
Compute (account_balance chain2 person_1).
Compute (account_balance chain2 creator).
(* Creator transfers 10 coins to person_1 *)
Definition chain3 : ChainBuilder :=
unpack_option (add_block chain2 [build_act creator (act_transfer person_1 10)]).
unpack_result (add_block chain2 [build_act creator (act_transfer person_1 10)]).
Compute (account_balance chain3 person_1).
Compute (account_balance chain3 creator).
......@@ -71,7 +81,7 @@ Section LocalBlockchainTests.
create_deployment 5 Congress.contract setup.
Definition chain4 : ChainBuilder :=
unpack_option (add_block chain3 [build_act person_1 deploy_congress]).
unpack_result (add_block chain3 [build_act person_1 deploy_congress]).
Definition congress_1 : Address :=
match outgoing_txs (builder_trace chain4) person_1 with
......@@ -115,7 +125,7 @@ Section LocalBlockchainTests.
Definition chain5 : ChainBuilder :=
let acts := [build_act person_1 (add_person person_1);
build_act person_1 (add_person person_2)] in
unpack_option (add_block chain4 acts).
unpack_result (add_block chain4 acts).
Compute (FMap.elements (congress_state chain5).(members)).
Compute (account_balance chain5 congress_1).
......@@ -126,7 +136,7 @@ Section LocalBlockchainTests.
congress_ifc.(send) 0 (Some (create_proposal [cact_transfer person_3 3])).
Definition chain6 : ChainBuilder :=
unpack_option (add_block chain5 [build_act person_1 create_proposal_call]).
unpack_result (add_block chain5 [build_act person_1 create_proposal_call]).
Compute (FMap.elements (congress_state chain6).(proposals)).
......@@ -136,7 +146,7 @@ Section LocalBlockchainTests.
Definition chain7 : ChainBuilder :=
let acts := [build_act person_1 vote_proposal; build_act person_2 vote_proposal] in
unpack_option (add_block chain6 acts).
unpack_result (add_block chain6 acts).
Compute (FMap.elements (congress_state chain7).(proposals)).
......@@ -145,7 +155,7 @@ Section LocalBlockchainTests.
congress_ifc.(send) 0 (Some (finish_proposal 1)).
Definition chain8 : ChainBuilder :=
unpack_option (add_block chain7 [build_act person_3 finish_proposal]).
unpack_result (add_block chain7 [build_act person_3 finish_proposal]).
Compute (FMap.elements (congress_state chain8).(proposals)).
(* Balances before: *)
......@@ -161,7 +171,7 @@ Section LocalBlockchainTests.
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
(prev new : BuilderDF) header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......@@ -173,7 +183,7 @@ Section LocalBlockchainTests.
Definition BuilderBF := LocalChainBuilderBreadthFirst AddrSize.
Lemma congress_txs_after_local_chain_bf_block
(prev new : BuilderBF) header acts :
builder_add_block prev header acts = Some new ->
builder_add_block prev header acts = Ok new ->
forall caddr,
env_contracts new caddr = Some (Congress.contract : WeakContract) ->
exists inc_calls,
......
This diff is collapsed.
......@@ -36,14 +36,14 @@ build_monad_laws {
Class MonadTrans (m : Type -> Type) (mt : Type -> Type) : Type :=
{ lift : forall {t}, mt t -> m t }.
Global Instance option_monad : Monad option :=
Global Instance Monad_option : Monad option :=
{| ret _ t := Some t;
bind _ _ v f := match v with
| Some val => f val
| None => None
end |}.
Global Instance option_monad_laws : MonadLaws option_monad.
Global Instance MonadLaws_Monad_option : MonadLaws Monad_option.
Proof.
constructor.
- auto.
......
From ConCert.Execution Require Import Monads.
Inductive result T E :=
| Ok (t : T)
| Err (e : E).
Arguments Ok {_ _}.
Arguments Err {_ _}.
Global Instance Monad_result {E} : Monad (fun T => result T E) :=
{| ret _ t := Ok t;
bind _ _ mt f :=
match mt with
| Ok t => f t
| Err e => Err e
end |}.
Definition result_of_option {T E} (o : option T) (err : E) : result T E :=
match o with
| Some a => Ok a
| None => Err err
end.
Definition option_of_result {T E} (r : result T E) : option T :=
match r with
| Ok t => Some t
| Err e => None
end.
# Extraction prototype
# Extraction
A prototype implementation of the extraction procedure from the deep embedding (essentially, just by printing). Currently, implements simplistic extraction to Liquidity. We also try to set use the standard Coq extraction to OCaml as a substitute for the Liquidity extraction, since the two languages are very close syntactically.
Contains two implementations:
* pretty-printing procedure from the deep embedding into the Liquidity syntax. Smart contracts have to be written in ``λsmart`` using the notations.
* extraction using MetaCoq's certified erasure. Extracts smart contracts impelemted in Gallina. Can handle some form of dependent types. Currently supports Liquidity as a target language.
From Coq Require Import PeanoNat ZArith Notations.
From MetaCoq.Template Require Import Loader.
From ConCert.Embedding Require Import MyEnv CustomTactics.
From ConCert.Embedding Require Import Notations.
From ConCert.Embedding Require Import SimpleBlockchain.
From ConCert.Extraction Require Import LPretty Certified.
From ConCert.Extraction Require Import Counter.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import AcornBlockchain.
Import MonadNotation.
Open Scope Z.
Definition PREFIX := "".
Module Counter.
Notation address := nat.
Definition storage := Z × address.
Inductive msg :=
| Inc (_ : Z)
| Dec (_ : Z).
Definition inc_balance (st : storage) (new_balance : Z) :=
(st.1 + new_balance, st.2).
Definition dec_balance (st : storage) (new_balance : Z) :=
(st.1 - new_balance, st.2).
Definition counter (msg : msg) (st : storage)
: option (list SimpleActionBody * storage) :=
match msg with
| Inc i =>
if (0 <=? i) then
Some ([], inc_balance st i)
else None
| Dec i =>
if (0 <=? i) then
Some ([], dec_balance st i)
else None
end.
End Counter.
Import Counter.
Import Lia.
Lemma inc_correct state n m :
0 <= m ->
state.1 = n ->
exists new_state, counter (Inc m) state = Some ([],new_state)
/\ new_state.1 = (n + m)%Z.
Proof.
intros Hm Hn.
eexists. split.
- simpl. destruct ?; Zleb_ltb_to_prop;auto;lia.
- simpl. congruence.
Qed.
Lemma dec_correct state n m :
0 <= m ->
state.1 = n ->
exists new_state, counter (Dec m) state = Some ([],new_state)
/\ new_state.1 = (n - m)%Z.
Proof.
intros Hm Hn.
eexists. split.
- simpl. destruct ?; Zleb_ltb_to_prop;auto;lia.
- simpl. congruence.
Qed.
Import Counter.
Definition local_def := local PREFIX.
(** A translation table for various constants we want to rename *)
Definition TT : env string :=
[ remap <% Z.add %> "addInt"
; remap <% Z.sub %> "subInt"
; remap <% Z.leb %> "leInt"
; remap <% Z %> "int"
; remap <% nat %> "address"
; ("Some", "Some")
; ("None", "None")
; ("Z0" ,"0")
; ("nil", "[]")
; remap <% @fst %> "fst"
; remap <% @snd %> "snd"
; remap <% storage %> "storage"
; local_def <% storage %>
; local_def <% option %>
; local_def <% msg %>
; local_def <% inc_balance %>
; local_def <% dec_balance %>
].
Quote Recursively Definition counter_syn := (unfolded counter).
(** We run the extraction procedure inside the [TemplateMonad]. It uses the certified erasure from [MetaCoq] and (so far uncertified) de-boxing procedure that removes application of boxes to constants and constructors. Even though the de-boxing is not certified yet, before removing boxes we check if constant is applied to all logical argument (i.e. proofs or types) and constructors are fully applied. In this case, it is safe to remove these applications. *)
Time Run TemplateProgram
(storage_def <- tmQuoteConstant "storage" false ;;
storage_body <- opt_to_template storage_def.(cst_body) ;;
ind <- tmQuoteInductive "msg" ;;
ind_liq <- print_one_ind_body PREFIX TT ind.(ind_bodies);;
t1 <- toLiquidity PREFIX TT inc_balance ;;
t2 <- toLiquidity PREFIX TT dec_balance ;;
t3 <- toLiquidity PREFIX TT counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops
++ nl ++ nl
++ "type storage = " ++ print_liq_type PREFIX TT storage_body
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted" res).
Print counter_extracted.
Redirect "counter.liq" Print counter_extracted.
From Coq Require Import PeanoNat ZArith Notations Bool.
From MetaCoq.Template Require Import Loader.
From MetaCoq.Erasure Require Import Loader.
From ConCert Require Import MyEnv.
From ConCert.Embedding Require Import Notations.
From ConCert.Embedding Require Import SimpleBlockchain.
From ConCert.Extraction Require Import LPretty Certified.
From ConCert.Extraction Require Import Counter.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import AcornBlockchain.
Import MonadNotation.
Open Scope Z.
Import Lia.
Definition PREFIX := "coq_".
Module Counter.
Definition storage := Z × nat.
Inductive msg :=
| Inc (_ : Z)
| Dec (_ : Z).
Definition inc_balance (st : Z × nat) (new_balance : Z)
(p : (0 <=? new_balance) = true) :=
(st.1 + new_balance, st.2).
Definition dec_balance (st : storage) (new_balance : Z)
(p : (0 <=? new_balance) = true) :=
(st.1 - new_balance, st.2).
Definition my_bool_dec := Eval compute in bool_dec.
Definition counter (msg : msg) (st : storage)
: option (list SimpleActionBody * storage) :=
match msg with
| Inc i =>
match (my_bool_dec (0 <=? i) true) with
| left h =>
Some ([], inc_balance st i h)
| right _ => None
end
| Dec i =>
match (my_bool_dec (0 <=? i) true) with
| left h => Some ([], dec_balance st i h)
| right _ => None
end
end.
End Counter.
Import Counter.
Definition local_def := local PREFIX.
(** A translation table for various constants we want to rename *)
Definition TT : env string :=
[ remap <% Z.add %> "addInt"
; remap <% Z.sub %> "subInt"
; remap <% Z.leb %> "leInt"
; remap <% Z %> "int"
; remap <% bool %> "bool"
; remap <% nat %> "address"
; remap <% option %> "option"
; ("Some", "Some")
; ("None", "None")
; ("true", "true")
; ("false", "false")
; ("Z0" ,"0")
; ("nil", "[]")
; remap <% @fst %> "fst"
; remap <% @snd %> "snd"
; remap <% storage %> "storage"
; local_def <% storage %>
; local_def <% msg %>
; local_def <% my_bool_dec %>
; local_def <% inc_balance %>
; local_def <% dec_balance %>
].
Quote Recursively Definition ex_partially_applied_syn :=
((fun msg : msg => fun st => match msg with
| Inc i =>
match (my_bool_dec (0 <=? i) true) with
| left h =>
let f := inc_balance st i in
Some ([], f h)
| right _ => None
end
| Dec i =>
match (my_bool_dec (0 <=? i) true) with
| left h => Some ([], dec_balance st i h)
| right _ => None
end
end) : msg -> storage -> option (list SimpleActionBody * storage)).
Compute (check_applied ex_partially_applied_syn).
(* returns [false], as expected *)
(** We run the extraction procedure inside the [TemplateMonad]. It uses the certified erasure from [MetaCoq] and (so far uncertified) de-boxing procedure that removes application of boxes to constants and constructors. Even though the de-boxing is not certified yet, before removing boxes we check if constant is applied to all logical argument (i.e. proofs or types) and constructors are fully applied. In this case, it is safe to remove these applications. *)
Run TemplateProgram
(storage_def <- tmQuoteConstant "storage" false ;;
storage_body <- opt_to_template storage_def.(cst_body) ;;
sumbool_t <- tmQuoteInductive "sumbool" ;;
sumbool_liq <- print_one_ind_body PREFIX TT sumbool_t.(ind_bodies);;
ind <- tmQuoteInductive "msg" ;;
ind_liq <- print_one_ind_body PREFIX TT ind.(ind_bodies);;
t1 <- toLiquidity PREFIX TT inc_balance ;;
t2 <- toLiquidity PREFIX TT dec_balance ;;
t3 <- toLiquidity PREFIX TT my_bool_dec ;;
t4 <- toLiquidity PREFIX TT counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops
++ nl ++ nl
++ "type storage = " ++ print_liq_type PREFIX TT storage_body
++ nl ++ nl
++ sumbool_liq
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ t4
++ nl ++ nl
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted" res).
Print counter_extracted.
From Coq Require Import PeanoNat ZArith Notations Bool.
From MetaCoq.Template Require Import Loader.
From MetaCoq.Erasure Require Import Loader.
From ConCert Require Import MyEnv.
From ConCert.Embedding Require Import Notations CustomTactics.
From ConCert.Embedding Require Import SimpleBlockchain.
From ConCert.Extraction Require Import LPretty Certified.
From ConCert.Extraction Require Import Counter.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import AcornBlockchain.
Import MonadNotation.
Open Scope Z.
Import Lia.
Definition PREFIX := "coq_".
Module Type ZTheorems.
Axiom lt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
End ZTheorems.
(** We use parameterised modules (functors) to isolate proof terms from the extracted parts. Otherwise type cheking and erasing is taking too long *)
Module CounterRefinmentTypes (ZT : ZTheorems).
Definition storage := Z.
Definition positive := {z : Z | 0 <? z}.
Inductive msg :=
| Inc (_ : Z)
| Dec (_ : Z).
Program Definition inc_counter (st : storage) (new_balance : positive) :
{new_st : storage | st <? new_st} :=
exist (st + proj1_sig new_balance) _.
Next Obligation.
destruct new_balance.
unfold is_true in *. simpl.
Zleb_ltb_to_prop. apply ZT.lt_add_pos_r. exact i.
Qed.
Definition dec_counter (st : storage) (new_balance : positive) :=
st - proj1_sig new_balance.
Definition my_bool_dec := Eval compute in bool_dec.
Definition counter (msg : msg) (st : storage)
: option (list SimpleActionBody * storage) :=
match msg with
| Inc i =>
match (my_bool_dec (0 <? i) true) with
| left h => Some ([], proj1_sig (inc_counter st (exist i h)))
| right _ => None
end
| Dec i =>
match (my_bool_dec (0 <? i) true) with
| left h => Some ([], dec_counter st (exist i h))
| right _ => None
end
end.
End CounterRefinmentTypes.
Module ZT : ZTheorems.
Lemma lt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
Proof. apply Z.lt_add_pos_r. Qed.
End ZT.
Module CRT := (CounterRefinmentTypes ZT).
Import CRT.
Definition local_def := local PREFIX.
(** A translation table for various constants we want to rename *)
Definition TT_rt : env string :=
[ remap <% Z.add %> "addInt"
; remap <% Z.sub %> "subInt"
; remap <% Z.leb %> "leInt"
; remap <% Z.ltb %> "ltInt"
; remap <% Z %> "int"
; remap <% bool %> "bool"
; remap <% nat %> "address"
; remap <% option %> "option"
; remap <% proj1_sig %> "(fun x -> x)" (* this is a safe, but ad-hoc optimisation*)
; remap <% positive %> "int" (* this is again an ad-hoc optimisation *)
; ("Some", "Some")
; ("None", "None")
; ("true", "true")
; ("false", "false")
; ("exist", "exist")
; ("Z0" ,"0")
; ("nil", "[]")
; remap <% @fst %> "fst"
; remap <% @snd %> "snd"
; remap <% storage %> "storage"
; local_def <% storage %>
; local_def <% msg %>
; local_def <% my_bool_dec %>
; local_def <% inc_counter %>
; local_def <% dec_counter %>
].
(** exists becomes just a wrapper *)
Definition exists_def := "let exist a = a".
Quote Recursively Definition Counter := (counter).
(** We run the extraction procedure inside the [TemplateMonad]. It uses the certified erasure from [MetaCoq] and (so far uncertified) de-boxing procedure that remove redundant type abstractions and application of boxes *)
Time Run TemplateProgram
(storage_def <- tmQuoteConstant "storage" false ;;
storage_body <- opt_to_template storage_def.(cst_body) ;;
sumbool_t <- tmQuoteInductive "sumbool" ;;
sumbool_liq <- print_one_ind_body PREFIX TT sumbool_t.(ind_bodies);;
ind <- tmQuoteInductive "msg" ;;
ind_liq <- print_one_ind_body PREFIX TT_rt ind.(ind_bodies);;
t1 <- toLiquidityEnv PREFIX TT_rt (Counter.1) inc_counter ;;
t2 <- toLiquidityEnv PREFIX TT_rt (Counter.1) dec_counter ;;
t3 <- toLiquidityEnv PREFIX TT_rt (Counter.1) my_bool_dec ;;
t4 <- toLiquidityEnv PREFIX TT_rt (Counter.1) counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops ++ nl ++ exists_def
++ nl ++ nl
++ "type storage = " ++ print_liq_type PREFIX TT_rt storage_body
++ nl ++ nl
++ sumbool_liq
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ t4
++ nl ++ nl
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted_refinment_types" res).
Print counter_extracted_refinment_types.
Require Import String ZArith Basics.
From ConCert.Embedding Require Import Ast Notations CustomTactics
PCUICTranslate PCUICtoTemplate Utils MyEnv.
From ConCert.Extraction Require Import Certified LPretty.
From ConCert.Extraction.Examples Require Import Prelude CrowdfundingData Crowdfunding SimpleBlockchain.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import AcornBlockchain.
Import MonadNotation.
Open Scope Z.
Import CrowdfundingContract.
Import Validate.
Import Receive.
Definition PREFIX := "".
Definition local_def := local PREFIX.
(** A translation table for various constants we want to rename *)
Definition TT : env string :=
[ (* types *)
remap <% Z %> "tez"
; remap <% address_coq %> "address"
; remap <% time_coq %> "timestamp"
; remap <% nat %> "nat"
; remap <% bool %> "bool"
; remap <% unit %> "unit"
; remap <% list %> "list"
; remap <% @fst %> "fst"
; remap <% @snd %> "snd"
; remap <% option %> "option"
; remap <% addr_map %> "(address,tez) map"
; remap <% SimpleActionBody %> "operation"
; remap <% Z.add %> "addTez"
; remap <% Z.eqb %> "eqTez"
; remap <% Z.leb %> "leTez"
; remap <% Z.ltb %> "ltTez"
; remap <% ltb_time %> "ltb_time"
; remap <% leb_time %> "leb_time"
; remap <% eqb_addr %> "eq_addr"
; remap <% andb %> "andb"
; remap <% negb %> "not"
; remap <% add_map %> "Map.add"
; remap <% lookup %> "Map.find"
; ("Z0" ,"0DUN")
; ("nil", "[]")
; ("tt", "()")
; local_def <% msg_coq %>
; local_def <% update_contribs %>
; local_def <% maybe_bind_unit %>
; local_def <% set_done %>
; local_def <% validate %>
].
Definition printWrapperAndMain :=
"let wrapper (msg : msg_coq)(st : ((timestamp * (tez * address)) * ((address,tez) map * bool))) = match receive msg st (Current.time (), (Current.sender (), (Current.amount (), Current.balance ()))) with
| Some v -> v| None -> failwith ()
let%entry main (msg : msg_coq)(st : ((timestamp * (tez * address)) * ((address,tez) map * bool))) = wrapper msg st".
Time Run TemplateProgram
(ind <- tmQuoteInductive "msg_coq" ;;
ind_liq <- print_one_ind_body PREFIX TT ind.(ind_bodies);;
t1 <- toLiquidity PREFIX TT update_contribs ;;
t2 <- toLiquidity PREFIX TT maybe_bind_unit ;;
t3 <- toLiquidity PREFIX TT set_done ;;
t4 <- toLiquidity PREFIX TT validate ;;
t5 <- toLiquidity PREFIX TT receive ;;
res <- tmEval lazy
(LiquidityPrelude
++ nl ++ nl
++ "type storage = ((timestamp * (tez * address)) * ((address,tez) map * bool))"
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ t4
++ nl ++ nl
++ t5
++ nl ++ nl
++ printWrapperAndMain ) ;;
tmDefinition "crowdfunding_extracted" res).
Print crowdfunding_extracted.
From Coq Require Import PeanoNat ZArith Notations Bool.
From MetaCoq.SafeChecker Require Import PCUICSafeChecker SafeTemplateChecker.
From MetaCoq.Template Require Import Loader.
From MetaCoq.Erasure Require Import Loader.
From ConCert Require Import MyEnv.
From ConCert.Embedding Require Import Notations.
From ConCert.Embedding Require Import SimpleBlockchain.
From ConCert.Extraction Require Import LPretty Certified Extra.
From ConCert.Execution Require Import Containers.
From Coq Require Import List Ascii String.
Local Open Scope string_scope.
From MetaCoq.Template Require Import All.
Import ListNotations.
Import MonadNotation.
Definition PREFIX := "".
(** Quoting this runs forever, because of many dependencies *)
Definition lookup (m : FMap string Z) (k : string) := FMap.find k m.
(* Quote Recursively Definition lookup_quoted :=lookup. *)
Definition map_key_type := (string * Z).
Module Interpreter.
Inductive op : Set := Add | And | Equal.
Inductive instruction :=
| IPushZ : Z -> instruction
| IPushB : bool -> instruction
| IObs : string -> Z -> instruction
| IOp : op -> instruction.
Inductive value : Set := BVal : bool -> value | ZVal : Z -> value.
Definition ext_map := FMap (string * Z) value.
Definition lookup (k : string * Z) (m : ext_map) := FMap.find k m.
Definition storage := list value.
Definition params := list instruction * ext_map.
Definition obs0 s := IObs s 0.
Fixpoint interp (ext : ext_map) (insts : list instruction) (s : list value) :=
match insts with
| [] => Some s
| hd :: inst' =>
match hd with
| IPushZ i => interp ext inst' (ZVal i :: s)
| IPushB b => interp ext inst' (BVal b :: s)
| IObs l i => match lookup (l,i) ext with
| Some v => Some (v :: s)
| None => None
end
| IOp op => match op with
| Add => match s with
| ZVal i :: ZVal j :: s' => interp ext inst' (ZVal (i+j) :: s')%Z
| _ => None
end
| And => match s with
| BVal i :: BVal j :: s' => interp ext inst' (BVal (i && j) :: s')%Z
| _ => None
end
| Equal => match s with
| ZVal i :: ZVal j :: s' => interp ext inst' (BVal (i =? j) :: s')%Z
| _ => None
end
end
end
end.
Definition receive (p : params) (s : list value) := interp p.2 p.1 s.
End Interpreter.
Import Interpreter.
Definition local_def := local PREFIX.
Definition print_finmap_type (prefix ty_key ty_val : string) :=
parens false (ty_key ++ "," ++ prefix ++ ty_val) ++ " map".
(** A translation table for various constants we want to rename *)
Definition TT : env string :=
[ (* remapping types *)
remap <% Z %> "int"
; remap <% bool %> "bool"
; remap <% nat %> "address"
; remap <% list %> "list"
; remap <% string %> "string"
; remap <% ext_map %> (print_finmap_type PREFIX "string * int" "value")
(* remapping operations *)
; remap <% Z.add %> "addInt"
; remap <% Z.eqb %> "eqInt"
; remap <% @lookup %> "Map.find"
; remap <% @fst %> "fst"
; remap <% @snd %> "snd"
; remap <% andb %> "andb"
(* remapping constructors *)
; ("Some", "Some")
; ("None", "None")
; ("true", "true")
; ("false", "false")
; ("Z0" ,"0")
; ("nil", "[]")
(* local types *)
; local_def <% storage %>
; local_def <% params %>
; local_def <% interp %>
; local_def <% instruction %>
; local_def <% value %>
; local_def <% op %>
].
(** A wrapper for calling the main functionality [func_name]. It is important to be explicit about types for all the parameters of entry points *)
Definition print_main (func_name : string): string :=
let func_name := PREFIX ++ func_name in
let params_name := PREFIX ++ "params" in
"let%entry main (p : " ++ params_name ++ ")" ++ " s ="
++ nl
++ "match " ++ func_name ++ " p s" ++ " with"
++ nl
++ "| Some res -> ( [], res ) "
++ nl
++ "| _ -> Current.failwith s".
Fixpoint combine_global_envs (Σ Σ' : global_env) : global_env :=
match Σ' with
| [] => Σ
| (nm,d) :: Σ'' => match (lookup_env Σ nm) with
| Some _ => (combine_global_envs Σ Σ'')%list
| None => ((nm,d) :: combine_global_envs Σ Σ'')%list
end
end.
Definition INTERP_MODULE : LiquidityModule :=
{| (* a name for the definition with the extracted code *)
lm_module_name := "liquidity_interp" ;
(* definitions of operations on ints, bools, pairs, ect. *)
lm_prelude := prod_ops ++ nl ++ int_ops ++ nl ++ bool_ops;
(* inductives *)
lm_adts := ["op";"instruction";"value"];
(* definitions: type abbreviations and functions *)
lm_defs := ["params"; "storage";"obs0";"interp";"receive"];