...
 
Commits (26)
......@@ -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): ;
......
......@@ -36,9 +36,13 @@ docs folder after `make html`.
## Structure of the project
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).
## Notes for developers
The [execution](execution/) subproject can be built independently via running `make` in the `execution` folder. This also means that the `_CoqProject` file inside the `execution` folder musdt be manually kept in sync with the main `_CoqProject` in the root.
......@@ -12,7 +12,6 @@ execution/theories/ChainedList.v
execution/theories/Circulation.v
execution/theories/Containers.v
execution/theories/ContractMonads.v
execution/theories/Examples/BignumsSerializable.v
execution/theories/Examples/BoardroomMath.v
execution/theories/Examples/BoardroomVoting.v
execution/theories/Examples/BoardroomVotingTest.v
......@@ -57,6 +56,10 @@ embedding/examples/SimpleBlockchain.v
-Q extraction/theories ConCert.Extraction
extraction/theories/Liquidity.v
extraction/theories/LPretty.v
extraction/theories/Certified.v
# extraction/theories/Extraction.v
-Q extraction/examples ConCert.Extraction.Examples
extraction/examples/Prelude.v
......@@ -64,8 +67,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
......@@ -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.
......
......@@ -12,7 +12,6 @@ theories/ChainedList.v
theories/Circulation.v
theories/Containers.v
theories/ContractMonads.v
theories/Examples/BignumsSerializable.v
theories/Examples/BoardroomMath.v
theories/Examples/BoardroomVoting.v
theories/Examples/BoardroomVotingTest.v
......
......@@ -40,10 +40,22 @@ Module FMap.
Section Theories.
Context {K V : Type} `{countable.Countable K}.
Proposition of_elements_eq (m : FMap K V) :
Lemma of_elements_eq (m : FMap K V) :
of_list (elements m) = m.
Proof. apply fin_maps.list_to_map_to_list. Qed.
Lemma of_list_elements (m : FMap K V) :
of_list (elements m) = m.
Proof. apply fin_maps.list_to_map_to_list. Qed.
Lemma elements_of_list (l : list (K * V)) :
NoDup (map fst l) ->
Permutation (elements (of_list l)) l.
Proof.
rewrite <- base.NoDup_ListNoDup.
apply fin_maps.map_to_list_to_map.
Qed.
Lemma find_add (k : K) (v : V) (m : FMap K V) :
find k (add k v m) = Some v.
Proof. apply fin_maps.lookup_insert. Qed.
......@@ -208,6 +220,33 @@ Module FMap.
rewrite elements_add; auto.
apply find_remove.
Qed.
Lemma not_In_elements k (m : FMap K V) :
(forall v, ~ In (k, v) (elements m)) <-> find k m = None.
Proof.
split.
- intros all.
destruct (find k m) eqn:find; [|easy].
pose proof (proj2 (In_elements _ _ _) find).
specialize (all v); congruence.
- intros find v is_in.
pose proof (proj1 (In_elements _ _ _) is_in).
congruence.
Qed.
Lemma NoDup_elements (m : FMap K V) :
NoDup (elements m).
Proof.
apply base.NoDup_ListNoDup.
apply fin_maps.NoDup_map_to_list.
Qed.
Lemma NoDup_keys (m : FMap K V) :
NoDup (keys m).
Proof.
apply base.NoDup_ListNoDup.
apply fin_maps.NoDup_fst_map_to_list.
Qed.
End Theories.
End FMap.
......
From Bignums Require Import BigN.
From Bignums Require Import BigZ.
From Coq Require Import ZArith.
From Coq Require Import DoubleType.
Require Import Monads.
Require Import Serializable.
Section IntSer.
Definition int_serializable
(T := BigN.dom_t 0)
(to_Z : T -> Z)
(of_Z : Z -> T)
(of_to_Z : forall t, of_Z (to_Z t) = t) : Serializable T.
Proof.
refine
{| serialize t := serialize (to_Z t);
deserialize p := do z <- deserialize p; ret (of_Z z); |}.
intros x.
rewrite deserialize_serialize.
cbn.
now rewrite of_to_Z.
Defined.
(* Massive hack: ltac inside notation is only checked at expansion time.
This allows the proof below to work for Coq 8.10 where Bignums uses int63
and Coq 8.9 where Bignums uses int31 and int63 does not even exist. *)
Local Set Warnings "-non-reversible-notation".
Notation "'lazyexp' x" := ltac:(exact x) (at level 70).
Global Instance int_serializable_inst : Serializable (BigN.dom_t 0).
Proof.
first
[exact
(int_serializable
(lazyexp Int31.phi)
(lazyexp Int31.phi_inv)
(lazyexp Cyclic31.phi_inv_phi))|
exact
(int_serializable
(lazyexp Int63.to_Z)
(lazyexp Int63.of_Z)
(lazyexp Int63.of_to_Z))].
Defined.
End IntSer.
Global Instance zn2z_serializable {A} `{Serializable A} : Serializable (zn2z A).
Proof.
refine
{| serialize w1 :=
serialize
match w1 with
| W0 => (0%nat, serialize tt)
| WW a b => (1%nat, serialize (a, b))
end;
deserialize p :=
do '(tag, p) <- deserialize p;
match tag with
| 0%nat => ret W0
| _ => do '(a, b) <- deserialize p;
ret (WW a b)
end |}.
intros.
rewrite deserialize_serialize.
cbn.
destruct x; auto.
now rewrite deserialize_serialize.
Defined.
Global Instance word_serializable {A} `{Serializable A} (n : nat) : Serializable (word A n) :=
(fix f (n : nat) :=
match n return (Serializable (word A n)) with
| 0%nat => _ : Serializable A
| S n => zn2z_serializable
end) n.
Global Instance BigNw1_serializable : Serializable BigN.w1 := ltac:(apply zn2z_serializable).
Global Instance BigNw2_serializable : Serializable BigN.w2 := ltac:(apply zn2z_serializable).
Global Instance BigNw3_serializable : Serializable BigN.w3 := ltac:(apply zn2z_serializable).
Global Instance BigNw4_serializable : Serializable BigN.w4 := ltac:(apply zn2z_serializable).
Global Instance BigNw5_serializable : Serializable BigN.w5 := ltac:(apply zn2z_serializable).
Global Instance BigNw6_serializable : Serializable BigN.w6 := ltac:(apply zn2z_serializable).
Global Instance BigN_serializable : Serializable bigN.
Proof.
refine
{| serialize n :=
match n with
| BigN.N0 i => serialize (0, serialize i)
| BigN.N1 w => serialize (1, serialize w)
| BigN.N2 w => serialize (2, serialize w)
| BigN.N3 w => serialize (3, serialize w)
| BigN.N4 w => serialize (4, serialize w)
| BigN.N5 w => serialize (5, serialize w)
| BigN.N6 w => serialize (6, serialize w)
| BigN.Nn n w => serialize (7, serialize (n, serialize w))
end%nat;
deserialize p :=
do '(tag, p) <- deserialize p;
match tag with
| 0 => option_map BigN.N0 (deserialize p)
| 1 => option_map BigN.N1 (deserialize p)
| 2 => option_map BigN.N2 (deserialize p)
| 3 => option_map BigN.N3 (deserialize p)
| 4 => option_map BigN.N4 (deserialize p)
| 5 => option_map BigN.N5 (deserialize p)
| 6 => option_map BigN.N6 (deserialize p)
| 7 => do '(n, p) <- deserialize p;
do w <- deserialize p;
ret (BigN.Nn n w)
| _ => None
end%nat |}.
intros [].
all: rewrite ?deserialize_serialize; cbn.
all: rewrite ?deserialize_serialize; easy.
Defined.
Global Instance BigZ_serializable : Serializable bigZ :=
Derive Serializable BigZ.t__rect<BigZ.Pos, BigZ.Neg>.
......@@ -42,6 +42,7 @@ Class BoardroomAxioms {A : Type} :=
mul_proper :> Proper (elmeq ==> elmeq ==> elmeq) mul;
opp_proper :> Proper (elmeq ==> elmeq) opp;
inv_proper :> Proper (elmeq ==> elmeq) inv;
pow_base_proper :> Proper (elmeq ==> eq ==> elmeq) pow;
pow_exp_proper a :
~(elmeq a zero) -> Proper (expeq ==> elmeq) (pow a);
......@@ -76,6 +77,11 @@ Class BoardroomAxioms {A : Type} :=
~(elmeq a zero) ->
elmeq (pow a (e + e')) (mul (pow a e) (pow a e'));
pow_pow a b e :
~(elmeq a zero) ->
elmeq (pow (pow a b) e)
(pow a (b * e)%Z);
pow_nonzero a e :
~(elmeq a zero) ->
~(elmeq (pow a e) zero);
......@@ -87,19 +93,24 @@ Class BoardroomAxioms {A : Type} :=
Arguments BoardroomAxioms : clear implicits.
Delimit Scope ffield_scope with ffield.
Delimit Scope broom_scope with broom.
Module BoardroomMathNotations.
Infix "==" := elmeq (at level 70) : broom.
Infix "=?" := elmeqb (at level 70) : broom.
Notation "a !== b" := (~(elmeq a b)) (at level 70) : broom.
Notation "0" := zero : broom.
Notation "1" := one : broom.
Infix "+" := add : broom.
Infix "*" := mul : broom.
Infix "^" := pow : broom.
Notation "a 'exp=' b" := (expeq a b) (at level 70) : broom.
Notation "a 'exp<>' b" := (~(expeq a b)) (at level 70) : broom.
End BoardroomMathNotations.
Infix "==" := elmeq (at level 70) : ffield.
Notation "a !== b" := (~(elmeq a b)) (at level 70) : ffield.
Notation "0" := zero : ffield.
Notation "1" := one : ffield.
Infix "+" := add : ffield.
Infix "*" := mul : ffield.
Infix "^" := pow : ffield.
Notation "a 'exp=' b" := (expeq a b) (at level 70) : ffield.
Notation "a 'exp<>' b" := (~(expeq a b)) (at level 70) : ffield.
Import BoardroomMathNotations.
Local Open Scope broom.
Local Open Scope ffield.
Global Instance oeq_equivalence {A : Type} (field : BoardroomAxioms A) : Equivalence expeq.
Proof.
unfold expeq.
......@@ -111,7 +122,7 @@ Qed.
Definition BoardroomAxioms_field_theory {A : Type} (field : BoardroomAxioms A) :
field_theory
zero one
0 1
add mul
(fun x y => x + (opp y)) opp
(fun x y => x * inv y) inv
......@@ -165,18 +176,43 @@ Section WithBoardroomAxioms.
Context {gen : Generator field}.
Context {disc_log : DiscreteLog field gen}.
Add Field ff : (BoardroomAxioms_field_theory field).
Local Open Scope ffield.
Hint Resolve one_neq_zero pow_nonzero generator_nonzero inv_nonzero : core.
Fixpoint prod (l : list A) : A :=
match l with
| [] => one
| x :: xs => x * prod xs
end.
Definition compute_public_key (sk : Z) : A :=
generator ^ sk.
Definition reconstructed_key (pks : list A) (n : nat) : A :=
let lprod := prod (firstn n pks) in
let rprod := inv (prod (skipn (S n) pks)) in
lprod * rprod.
Definition compute_public_vote (rk : A) (sk : Z) (sv : bool) : A :=
rk ^ sk * if sv then generator else 1.
Fixpoint bruteforce_tally_aux
(n : nat)
(votes_product : A) : option nat :=
if generator ^ (Z.of_nat n) =? votes_product then
Some n
else
match n with
| 0 => None
| S n => bruteforce_tally_aux n votes_product
end%nat.
Definition bruteforce_tally (votes : list A) : option nat :=
bruteforce_tally_aux (length votes) (prod votes).
Add Field ff : (BoardroomAxioms_field_theory field).
Local Open Scope broom.
Hint Resolve one_neq_zero pow_nonzero generator_nonzero inv_nonzero : core.
Instance plus_expeq_proper : Proper (expeq ==> expeq ==> expeq) Z.add.
Proof.
intros x x' xeq y y' yeq.
......@@ -299,31 +335,6 @@ Section WithBoardroomAxioms.
Hint Resolve -> prod_units : core.
Hint Resolve <- prod_units : core.
Definition compute_public_key (sk : Z) : A :=
generator ^ sk.
Definition reconstructed_key (pks : list A) (n : nat) : A :=
let lprod := prod (firstn n pks) in
let rprod := inv (prod (skipn (S n) pks)) in
lprod * rprod.
Definition compute_public_vote (rk : A) (sk : Z) (sv : bool) : A :=
rk ^ sk * if sv then generator else 1.
Fixpoint bruteforce_tally_aux
(n : nat)
(votes_product : A) : option nat :=
if elmeqb (generator ^ (Z.of_nat n)) votes_product then
Some n
else
match n with
| 0 => None
| S n => bruteforce_tally_aux n votes_product
end%nat.
Definition bruteforce_tally (votes : list A) : option nat :=
bruteforce_tally_aux (length votes) (prod votes).
Lemma compute_public_key_unit sk :
compute_public_key sk !== 0.
Proof. apply pow_nonzero, generator_nonzero. Qed.
......@@ -460,7 +471,7 @@ Section WithBoardroomAxioms.
destruct (i <? j)%nat; lia.
Qed.
Local Open Scope ffield.
Local Open Scope broom.
Lemma mul_public_votes
(sks : list Z)
(votes : nat -> bool) :
......@@ -559,6 +570,25 @@ Section WithBoardroomAxioms.
now intros ? ? <-.
Qed.
Global Instance elmeqb_elmeq_proper :
Proper (elmeq ==> elmeq ==> eq) elmeqb.
Proof.
intros x x' xeq y y' yeq.
destruct (elmeqb_spec x y), (elmeqb_spec x' y'); auto.
- contradiction n.
now rewrite <- xeq, <- yeq.
- contradiction n.
now rewrite xeq, yeq.
Qed.
Lemma elmeqb_refl a :
a =? a = true.
Proof.
destruct (elmeqb_spec a a); [easy|].
contradiction n.
reflexivity.
Qed.
Lemma bruteforce_tally_aux_correct result max :
Z.of_nat max < order - 1 ->
(result <= max)%nat ->
......@@ -568,13 +598,10 @@ Section WithBoardroomAxioms.
induction max as [|max IH].
- replace result with 0%nat by lia.
cbn.
destruct (elmeqb_spec (generator^0) (generator^0)); auto.
contradiction n; reflexivity.
now rewrite elmeqb_refl.
- destruct (Nat.eq_dec result (S max)) as [->|?].
+ cbn.
destruct (elmeqb_spec (generator ^ Z.pos (Pos.of_succ_nat max))
(generator ^ Z.pos (Pos.of_succ_nat max))); auto.
contradiction n; reflexivity.
now rewrite elmeqb_refl.
+ cbn -[Z.of_nat].
destruct (elmeqb_spec (generator ^ Z.of_nat (S max))
(generator ^ Z.of_nat result)) as [eq|?]; auto.
......@@ -957,6 +984,16 @@ Module Zp.
mod_pow_pos (a mod p) x p = mod_pow_pos a x p.
Proof. apply mod_pow_pos_aux_mod_idemp. Qed.
Lemma mod_pow_mod_idemp a e p :
mod_pow (a mod p) e p = mod_pow a e p.
Proof.
unfold mod_pow.
destruct e.
- now rewrite Z_pow_mod_idemp.
- now rewrite mod_pow_pos_mod_idemp.
- now rewrite mod_pow_pos_mod_idemp.
Qed.
Lemma mod_pow_pos_aux_mod a x p r :
mod_pow_pos_aux a x p r mod p = mod_pow_pos_aux a x p r.
Proof.
......@@ -1482,6 +1519,8 @@ Module Zp.
- intros a a' aeq.
cbn.
now rewrite <- mod_inv_mod_idemp, aeq, mod_inv_mod_idemp by auto.
- intros a a' aeq e ? <-.
now rewrite <- mod_pow_mod_idemp, aeq, mod_pow_mod_idemp.
- intros a anp e e' eeq.
rewrite <- (mod_pow_exp_mod _ e), <- (mod_pow_exp_mod _ e') by auto.
now rewrite eeq.
......@@ -1528,6 +1567,8 @@ Module Zp.
now rewrite mod_inv_mod_idemp.
- intros a e e' ap0.
now rewrite mod_pow_exp_plus by auto.
- intros a b e anz.
now rewrite mod_pow_exp_mul.
- auto.
- auto.
Defined.
......@@ -1669,24 +1710,25 @@ Module BigZp.
Hint Rewrite BigZ.spec_modulo : zsimpl.
Definition boardroom_axioms (p : bigZ) :
prime [p] -> BoardroomAxioms bigZ.
Local Open Scope Z.
Definition boardroom_axioms (p : Z) :
prime p -> BoardroomAxioms Z.
Proof.
intros isprime.
pose proof (prime_ge_2 _ isprime).
refine
{| elmeq a b := a mod p == b mod p;
{| elmeq a b := a mod p = b mod p;
elmeqb a b := a mod p =? b mod p;
zero := 0;
one := 1;
add a a' := (a + a') mod p;
mul a a' := (a * a') mod p;
opp a := p - a;
inv a := mod_inv a p;
pow a e := mod_pow a e p;
order := BigZ.to_Z p;
|}; unfold "==".
- intros x y; apply BigZ.eqb_spec.
inv a := [mod_inv (BigZ.of_Z a) (BigZ.of_Z p)];
pow a e := [mod_pow (BigZ.of_Z a) e (BigZ.of_Z p)];
order := p;
|}.
- intros x y; apply Z.eqb_spec.
- lia.
- constructor; auto.
now intros a a' a'' -> ->.
......@@ -1702,6 +1744,9 @@ Module BigZp.
- intros a a' aeq.
autorewrite with zsimpl in *.
now rewrite <- Zp.mod_inv_mod_idemp, aeq, Zp.mod_inv_mod_idemp.
- intros a a' aeq e ? <-.
autorewrite with zsimpl in *.
now rewrite <- Zp.mod_pow_mod_idemp, aeq, Zp.mod_pow_mod_idemp.
- intros a anp e e' eeq.
autorewrite with zsimpl in *.
rewrite <- (Zp.mod_pow_exp_mod _ e), <- (Zp.mod_pow_exp_mod _ e') by auto.
......@@ -1736,7 +1781,7 @@ Module BigZp.
- intros a.
autorewrite with zsimpl in *.
rewrite Z.mod_mod by lia.
replace ([p] - [a] + [a])%Z with [p] by lia.
replace (p - a + a)%Z with p by lia.
rewrite Z.mod_same, Z.mod_0_l; lia.
- intros a anp.
autorewrite with zsimpl in *.
......@@ -1764,6 +1809,9 @@ Module BigZp.
- intros a e e' ap0.
autorewrite with zsimpl in *.
now rewrite Zp.mod_pow_exp_plus by auto.
- intros a b e ap0.
autorewrite with zsimpl in *.
now rewrite Zp.mod_pow_exp_mul.
- intros a e ap0.
autorewrite with zsimpl in *.
auto.
......
From Bignums Require Import BigZ.
From Coq Require Import Cyclic31.
From Coq Require Import List.
From Coq Require Import Znumtheory.
Require Import BignumsSerializable.
Require Import Blockchain.
Require Import BoardroomMath.
Require Import BoardroomVoting.
......@@ -14,25 +12,26 @@ Require Import Monads.
Require Import Serializable.
Import ListNotations.
Import BoardroomMathNotations.
Local Open Scope bigZ.
Local Open Scope ffield.
Local Open Scope Z.
Local Open Scope broom.
(*
Definition modulus : bigZ := 1552518092300708935130918131258481755631334049434514313202351194902966239949102107258669453876591642442910007680288864229150803718918046342632727613031282983744380820890196288509170691316593175367469551763119843371637221007210577919.
Definition generator : bigZ := 2.
*)
Definition modulus : bigZ := 201697267445741585806196628073.
Definition generator : bigZ := 3.
Definition modulus : Z := 201697267445741585806196628073.
Definition generator : Z := 3.
Axiom modulus_prime : prime [modulus].
Instance axioms : BoardroomAxioms bigZ := BigZp.boardroom_axioms modulus modulus_prime.
Axiom modulus_prime : prime modulus.
Instance axioms : BoardroomAxioms Z := BigZp.boardroom_axioms modulus modulus_prime.
Lemma generator_nonzero : generator !== 0.
Proof. discriminate. Qed.
Axiom generator_is_generator :
forall z,
z !== 0 ->
~(z == 0) ->
exists! (e : Z), (0 <= e < order - 1)%Z /\ pow generator e == z.
Instance generator_instance : Generator axioms :=
......@@ -40,15 +39,11 @@ Instance generator_instance : Generator axioms :=
BoardroomMath.generator_nonzero := generator_nonzero;
generator_generates := generator_is_generator; |}.
Instance id_scheme : @VoteProofScheme bigZ :=
{| make_vote_proof l n z b := 0%Z;
verify_vote l n a z := true; |}.
Definition num_parties : nat := 7.
Definition votes_for : nat := 4.
(* a pseudo-random generator for secret keys *)
Definition sk n := [pow ((BigZ.of_Z (Z.of_nat n) + 1234583932) * (modulus - 23241)) 159338231].
Definition sk n := (Z.of_nat n + 1234583932) * (modulus - 23241)^159338231.
(* Make a list of secret keys, here starting at i=7 *)
Definition sks : list Z :=
......@@ -62,19 +57,30 @@ Definition svs : list bool :=
(seq 0 (num_parties - votes_for)).
(* Compute the public keys for each party *)
Definition pks : list bigZ :=
Definition pks : list Z :=
Eval native_compute in map compute_public_key sks.
(* Compute the signup messages that would be sent by each party *)
Definition rks : list Z :=
Eval native_compute in map (reconstructed_key pks) (seq 0 (length pks)).
(* In this example we just use xor for the hash function, which is
obviously not cryptographically secure. *)
Definition hash_func (l : list positive) : positive :=
N.succ_pos (fold_right (fun p a => N.lxor (Npos p) a) 1%N l).
(* Compute the signup messages that would be sent by each party.
We just use the public key as the chosen randomness here. *)
Definition signups : list Msg :=
Eval native_compute in map make_signup_msg sks.
Eval native_compute in map (fun '(sk, pk, i) => make_signup_msg hash_func sk 5 i)
(zip (zip sks pks) (seq 0 (length sks))).
(* Compute the submit_vote messages that would be sent by each party *)
(* Our functional correctness proof assumes that the votes were computed
using the make_vote_msg function provided by the contract *)
using the make_vote_msg function provided by the contract.
In this example we just use the secret key as the random parameters. *)
Definition votes : list Msg :=
Eval native_compute in map (fun '(i, sk, sv) => make_vote_msg pks i sk sv)
(zip (zip (seq 0 (length pks)) sks) svs).
Eval native_compute in map (fun '(i, sk, sv, rk) => make_vote_msg hash_func sk rk sv i sk sk sk)
(zip (zip (zip (seq 0 (length pks)) sks) svs) rks).
Definition AddrSize := (2^128)%N.
Instance Base : ChainBase := LocalChainBase AddrSize.
......@@ -118,7 +124,7 @@ Definition boardroom_example :=
block_reward := 50; |} in
builder_add_block chain next_header acts in
do chain <- add_block chain [];
let dep := build_act creator (create_deployment 0 (boardroom_voting BigZ.to_Z) deploy_setup) in
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))));
let send addr m := build_act addr (act_call caddr 0 (serialize m)) in
......@@ -128,7 +134,7 @@ Definition boardroom_example :=
do chain <- add_block chain votes;
let tally := build_act creator (act_call caddr 0 (serialize tally_votes)) in
do chain <- add_block chain [tally];
do state <- @contract_state _ (@State _ bigZ) _ (lcb_lc chain) caddr;
do state <- @contract_state _ (@State _ Z) _ (lcb_lc chain) caddr;
result state.
Check (@eq_refl (option nat) (Some votes_for)) <: boardroom_example = Some votes_for.
Check (@eq_refl (option nat) (Some votes_for)) <<: boardroom_example = Some votes_for.
......@@ -3,12 +3,14 @@ This format, SerializedValue, is either a unit/int/bool or a pair/list
of these. We also define Serializable as a type class capturing that a
type can be converted from and to this format. *)
From Coq Require Import ZArith.
Require Import Monads.
Require Import Containers.
Require Import Automation.
Require Import BoundedN.
From Coq Require Import List.
From Coq Require Import Psatz.
From Coq Require Import ZArith.
From stdpp Require countable.
Import ListNotations.
......@@ -397,3 +399,158 @@ Notation "'Derive' 'Serializable' rect < c0 , .. , cn >" :=
| [pairs := ?x |- _] => make_serializable rect x
end))
(at level 0, rect at level 10, c0, cn at level 9, only parsing).
Section Countable.
Instance SerializedType_interp_EqDecision
(t : SerializedType) : stdpp.base.EqDecision (interp_type t).
Proof. induction t; typeclasses eauto. Defined.
Instance SerializedType_interp_Countable
(t : SerializedType) : countable.Countable (interp_type t).
Proof. induction t; typeclasses eauto. Defined.
Global Instance SerializedValue_EqDecision : stdpp.base.EqDecision SerializedValue.
Proof.
intros x y.
destruct x as [xt xv], y as [yt yv].
destruct (SerializedType.eq_dec xt yt) as [<-|?]; [|right; congruence].
destruct (stdpp.base.decide (xv = yv)).
- left.
congruence.
- right.
intros eq.
inversion eq.
congruence.
Defined.
Instance SerializedType_EqDecision : stdpp.base.EqDecision SerializedType.
Proof.
intros x y.
destruct (SerializedType.eq_dec x y) as [<-|?]; [left|right]; easy.
Defined.
Fixpoint depth st : nat :=
match st with
| ser_unit => 1
| ser_int => 1
| ser_bool => 1
| ser_pair x y => S (max (depth x) (depth y))
| ser_list x => S (depth x)
end.
Local Open Scope positive.
Fixpoint encode_st_body (st : SerializedType) : positive :=
match st with
| ser_unit => countable.encode (1, 1)
| ser_int => countable.encode (2, 1)
| ser_bool => countable.encode (3, 1)
| ser_pair x y => countable.encode (4, countable.encode (encode_st_body x, encode_st_body y))
| ser_list x => countable.encode (5, encode_st_body x)
end.
Definition encode_st (st : SerializedType) : positive :=
countable.encode (depth st, encode_st_body st).
Fixpoint decode_st_body (depth : nat) (p : positive) : option SerializedType :=
match depth with
| 0%nat => None
| S depth =>
do '(tag, body) <- countable.decode p;
match tag with
| 1 => ret ser_unit
| 2 => ret ser_int
| 3 => ret ser_bool
| 4 => do '(x, y) <- countable.decode body;
do x <- decode_st_body depth x;
do y <- decode_st_body depth y;
ret (ser_pair x y)
| 5 => do x <- decode_st_body depth body;
ret (ser_list x)
| _ => None
end
end.
Definition decode_st (p : positive) : option SerializedType :=
do '(depth, body) <- countable.decode p;
decode_st_body depth body.
Local Open Scope nat.
Lemma decode_st_body_encode_st_body (d : nat) (st : SerializedType) :
depth st <= d ->
decode_st_body d (encode_st_body st) = Some st.
Proof.
revert st.
induction d; intros st dle; cbn in *.
- exfalso.
induction st; cbn in *; lia.
- destruct st; auto; cbn in *.
+ now rewrite !countable.decode_encode, !IHd by lia.
+ now rewrite !countable.decode_encode, !IHd by lia.
Qed.
Lemma decode_st_encode_st (st : SerializedType) :
decode_st (encode_st st) = Some st.
Proof.
unfold decode_st, encode_st.
rewrite countable.decode_encode; cbn.
now apply decode_st_body_encode_st_body.
Qed.
Local Open Scope positive.
Instance SerializedType_Countable : countable.Countable SerializedType :=
{| countable.encode := encode_st;
countable.decode := decode_st;
countable.decode_encode := decode_st_encode_st |}.
Definition encode_sv (sv : SerializedValue) : positive :=
countable.encode (ser_value_type sv, countable.encode (ser_value sv)).
Definition decode_sv (p : positive) : option SerializedValue :=
do '(ty, p) <- countable.decode p;
do v <- countable.decode p;
ret {| ser_value_type := ty; ser_value := v |}.
Lemma decode_sv_encode_sv (sv : SerializedValue) :
decode_sv (encode_sv sv) = Some sv.
Proof.
unfold decode_sv, encode_sv.
rewrite countable.decode_encode; cbn.
rewrite countable.decode_encode; cbn.
reflexivity.
Qed.
Global Instance SerializedValue_Countable : countable.Countable SerializedValue :=
{| countable.encode := encode_sv;
countable.decode := decode_sv;
countable.decode_encode := decode_sv_encode_sv |}.
Global Instance SerializableType_EqDecision
(A : Type) `{Serializable A} : stdpp.base.EqDecision A.
Proof.
intros a a'.
destruct (stdpp.base.decide (serialize a = serialize a')) as [eq|neq].
- left.
now apply serialize_injective.
- right.
intros ->.
congruence.
Defined.
Definition encode_serializable_type {A : Type} `{Serializable A} (a : A) : positive :=
countable.encode (serialize a).
Definition decode_serializable_type {A : Type} `{Serializable A} (p : positive) : option A :=
countable.decode p >>= deserialize.
Lemma decode_serializable_type_encode_serializable_type
{A : Type} `{Serializable A}
(a : A) :
decode_serializable_type (encode_serializable_type a) = Some a.
Proof.
unfold decode_serializable_type, encode_serializable_type.
rewrite countable.decode_encode.
cbn.
now rewrite deserialize_serialize.
Qed.
Global Instance SerializableType_Countable {A : Type} `{Serializable A} :
countable.Countable A :=
{| countable.encode := encode_serializable_type;
countable.decode := decode_serializable_type;
countable.decode_encode := decode_serializable_type_encode_serializable_type; |}.
End Countable.
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.
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.
(** 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"
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
].
Quote Recursively Definition counter_syn := (unfolded counter).
Time Eval vm_compute in (check_applied counter_syn).
Time Eval vm_compute in (erase_print_deboxed_all_applied TT counter_syn).
(** 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 TT ind.(ind_bodies);;
t1 <- toLiquidity TT inc_balance ;;
t2 <- toLiquidity TT dec_balance ;;
t3 <- toLiquidity TT counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops
++ nl ++ nl
++ "type storage = " ++ print_liq_type TT storage_body
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ printWrapper "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.
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.
(** 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"
; ("left", "Left")
; ("right", "Right")
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
; local <% my_bool_dec %>
].
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) ;;
ind <- tmQuoteInductive "msg" ;;
ind_liq <- print_one_ind_body TT ind.(ind_bodies);;
t1 <- toLiquidity TT inc_balance ;;
t2 <- toLiquidity TT dec_balance ;;
t3 <- toLiquidity TT my_bool_dec ;;
t4 <- toLiquidity TT counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops
++ nl ++ nl
++ "type storage = " ++ print_liq_type TT storage_body
++ nl ++ nl
++ ind_liq
++ nl ++ nl
++ t1
++ nl ++ nl
++ t2
++ nl ++ nl
++ t3
++ nl ++ nl
++ t4
++ nl ++ nl
++ printWrapper "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.
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).
Lemma lt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
Proof.
intros n m H.
induction m.
+ destruct n;