...
 
Commits (2)
......@@ -11,6 +11,8 @@
*~
CoqMakefile
CoqMakefile.conf
CoqMakefile.plugin
CoqMakefile.plugin.conf
Makefile.coq
Makefile.coq.conf
execution/CoqMakefile
......
......@@ -59,7 +59,7 @@ embedding/examples/SimpleBlockchain.v
extraction/theories/Liquidity.v
extraction/theories/LPretty.v
extraction/theories/Certified.v
#extraction/theories/Extraction.v
# extraction/theories/Extraction.v
-Q extraction/examples ConCert.Extraction.Examples
......
......@@ -166,4 +166,4 @@ 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
# extraction/theories/Loader.v
\ No newline at end of file
......@@ -6,7 +6,7 @@ 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 Notations CustomTactics.
From ConCert.Embedding Require Import SimpleBlockchain.
From ConCert.Extraction Require Import LPretty Certified.
From ConCert.Extraction Require Import Counter.
......@@ -24,21 +24,46 @@ Open Scope Z.
Import Lia.
Module CounterRefinmentTypes.
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 × nat.
Definition non_neg := {z : Z | 0 <=? z}.
Definition positive := {z : Z | 0 <? z}.
Inductive msg :=
| Inc (_ : Z)
| Dec (_ : Z).
Definition inc_balance (st : storage) (new_balance : non_neg) :=
(st.1 + proj1_sig new_balance, st.2).
Definition dec_balance (st : storage) (new_balance : non_neg) :=
Lemma lt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
Proof.
intros n m H.
induction m.
+ destruct n;auto.
+ destruct n;auto.
* inversion H.
* apply Pos.lt_add_r.
* inversion H.
+ destruct n;auto.
* inversion H.
* todo "".
* inversion H.
Qed.
Program Definition inc_balance (st : storage) (new_balance : positive) :
{new_st : storage | st.1 <? new_st.1}:=
exist (st.1 + proj1_sig new_balance, st.2) _.
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_balance (st : storage) (new_balance : positive) :=
(st.1 - proj1_sig new_balance, st.2).
Definition my_bool_dec := Eval compute in bool_dec.
......@@ -47,31 +72,38 @@ Module CounterRefinmentTypes.
: option (list SimpleActionBody * storage) :=
match msg with
| Inc i =>
match (my_bool_dec (0 <=? i) true) with
| left h => Some ([], inc_balance st (exist i h))
match (my_bool_dec (0 <? i) true) with
| left h => Some ([], proj1_sig (inc_balance st (exist i h)))
| right _ => None
end
| Dec i =>
match (my_bool_dec (0 <=? i) true) with
| left h => Some ([], inc_balance st (exist i h))
match (my_bool_dec (0 <? i) true) with
| left h => Some ([], dec_balance st (exist i h))
| right _ => None
end
end.
End CounterRefinmentTypes.
Import 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.
(** 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 <% nat %> "address"
; remap <% bool %> "bool"
; remap <% proj1_sig %> "(fun x -> x)" (* this is a safe, but ad-hoc optimisation*)
; remap <% non_neg %> "int" (* this is again an ad-hoc optimisation *)
; remap <% positive %> "int" (* this is again an ad-hoc optimisation *)
; ("left", "Left")
; ("right", "Right")
; ("Z0" ,"0")
......@@ -81,22 +113,25 @@ Definition TT_rt : env string :=
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
; local <% my_bool_dec %>
].
(** 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) ;;
ind <- tmQuoteInductive "msg" ;;
ind_liq <- print_one_ind_body TT_rt ind.(ind_bodies);;
t1 <- toLiquidity TT_rt CounterRefinmentTypes.inc_balance ;;
t2 <- toLiquidity TT_rt CounterRefinmentTypes.dec_balance ;;
t3 <- toLiquidity TT_rt CounterRefinmentTypes.my_bool_dec ;;
t4 <- toLiquidity TT_rt CounterRefinmentTypes.counter ;;
t1 <- toLiquidityEnv TT_rt (Counter.1) inc_balance ;;
t2 <- toLiquidityEnv TT_rt (Counter.1) dec_balance ;;
t3 <- toLiquidityEnv TT_rt (Counter.1) my_bool_dec ;;
t4 <- toLiquidityEnv TT_rt (Counter.1) counter ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops ++ nl ++ exists_def
++ nl ++ nl
......
All_Forall
Ascii
Ast0
AstUtils
BasicAst
Basics
BinInt
BinNat
BinNums
BinPos
Bool
Byte
Classes0
Compare_dec
Config0
Datatypes
EAst
EAstUtils
ELiftSubst
Environment
EPretty
EqDecInstances
EqdepFacts
Equalities
ErasureFunction
ETyping
Extract
G_concert_extract
Init
LiftSubst
List0
Main
MCCompare
MCList
MCOption
MCProd
MCString
Monad_utils
MSetDecide
MSetFacts
MSetInterface
MSetList
MSetProperties
MSetWeakList
Nat0
OrdersFacts
OrdersLists
Orders
OrdersTac
PCUICAst
PCUICAstUtils
PCUICChecker
PCUICCumulativity
PCUICEquality
PCUICLiftSubst
PCUICNormal
PCUICPosition
PCUICPretty
PCUICReflect
PCUICSafeChecker
PCUICSafeConversion
PCUICSafeLemmata
PCUICSafeReduce
PCUICSafeRetyping
PCUICTyping
PCUICUnivSubst
PeanoNat
Pretty
SafeErasureFunction
SafeTemplateChecker
SafeTemplateErasure
Specif
Ssrbool
String0
TemplateToPCUIC
Typing0
UGraph0
Universes0
UnivSubst0
Utils
WGraph