Commit 07cc3b76 authored by Danil's avatar Danil

Add a prefix to avoid clashes on extraction. Ad-hoc removal of constuctor...

Add a prefix to avoid clashes on extraction. Ad-hoc removal of constuctor arguments (inductive definitions) on extraction to Liquidity. A workaround for fetching dependencies (by Jakob).
parent 3963d3d8
Pipeline #20597 failed with stage
in 13 minutes and 30 seconds
......@@ -19,6 +19,8 @@ Import MonadNotation.
Open Scope Z.
Definition PREFIX := "".
Module Counter.
Notation address := nat.
......@@ -80,6 +82,8 @@ 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"
......@@ -87,34 +91,38 @@ Definition TT : env string :=
; remap <% Z.leb %> "leInt"
; remap <% Z %> "int"
; remap <% nat %> "address"
; ("Some", "Some")
; ("None", "None")
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
; 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).
Time Eval vm_compute in (check_applied counter_syn).
Time Eval vm_compute in (erase_print_deboxed_all_applied TT counter_syn).
Time Eval vm_compute in (erase_print_deboxed_all_applied PREFIX 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 ;;
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 TT storage_body
++ "type storage = " ++ print_liq_type PREFIX TT storage_body
++ nl ++ nl
++ ind_liq
++ nl ++ nl
......@@ -124,7 +132,7 @@ Time Run TemplateProgram
++ nl ++ nl
++ t3
++ nl ++ nl
++ printWrapper "counter"
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted" res).
......
......@@ -22,6 +22,8 @@ Open Scope Z.
Import Lia.
Definition PREFIX := "coq_".
Module Counter.
Definition storage := Z × nat.
......@@ -61,6 +63,8 @@ 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"
......@@ -69,17 +73,21 @@ Definition TT : env string :=
; remap <% Z %> "int"
; remap <% bool %> "bool"
; remap <% nat %> "address"
; ("left", "Left")
; ("right", "Right")
; remap <% option %> "option"
; ("Some", "Some")
; ("None", "None")
; ("true", "true")
; ("false", "false")
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_balance %>
; local <% dec_balance %>
; local <% my_bool_dec %>
; 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 :=
......@@ -105,16 +113,20 @@ Compute (check_applied ex_partially_applied_syn).
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 TT ind.(ind_bodies);;
t1 <- toLiquidity TT inc_balance ;;
t2 <- toLiquidity TT dec_balance ;;
t3 <- toLiquidity TT my_bool_dec ;;
t4 <- toLiquidity TT counter ;;
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 TT storage_body
++ "type storage = " ++ print_liq_type PREFIX TT storage_body
++ nl ++ nl
++ sumbool_liq
++ nl ++ nl
++ ind_liq
++ nl ++ nl
......@@ -126,7 +138,7 @@ Run TemplateProgram
++ nl ++ nl
++ t4
++ nl ++ nl
++ printWrapper "counter"
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted" res).
......
......@@ -22,6 +22,8 @@ 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.
......@@ -37,22 +39,6 @@ Module CounterRefinmentTypes (ZT : ZTheorems).
| 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;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_counter (st : storage) (new_balance : positive) :
{new_st : storage | st <? new_st} :=
exist (st + proj1_sig new_balance) _.
......@@ -92,6 +78,9 @@ 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"
......@@ -99,21 +88,26 @@ Definition TT_rt : env string :=
; remap <% Z.leb %> "leInt"
; remap <% Z.ltb %> "ltInt"
; remap <% Z %> "int"
; remap <% nat %> "address"
; 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 *)
; ("left", "Left")
; ("right", "Right")
; ("Some", "Some")
; ("None", "None")
; ("true", "true")
; ("false", "false")
; ("exist", "exist")
; ("Z0" ,"0")
; ("nil", "[]")
; local <% @fst %>
; local <% @snd %>
; local <% storage %>
; local <% msg %>
; local <% inc_counter %>
; local <% dec_counter %>
; local <% my_bool_dec %>
; 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 *)
......@@ -125,16 +119,20 @@ Quote Recursively Definition Counter := (counter).
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 TT_rt ind.(ind_bodies);;
t1 <- toLiquidityEnv TT_rt (Counter.1) inc_counter ;;
t2 <- toLiquidityEnv TT_rt (Counter.1) dec_counter ;;
t3 <- toLiquidityEnv TT_rt (Counter.1) my_bool_dec ;;
t4 <- toLiquidityEnv TT_rt (Counter.1) counter ;;
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 TT_rt storage_body
++ "type storage = " ++ print_liq_type PREFIX TT_rt storage_body
++ nl ++ nl
++ sumbool_liq
++ nl ++ nl
++ ind_liq
++ nl ++ nl
......@@ -146,7 +144,7 @@ Time Run TemplateProgram
++ nl ++ nl
++ t4
++ nl ++ nl
++ printWrapper "counter"
++ printWrapper (PREFIX ++ "counter")
++ nl ++ nl
++ printMain) ;;
tmDefinition "counter_extracted_refinment_types" res).
......
......@@ -20,6 +20,9 @@ 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 :=
......@@ -31,6 +34,8 @@ Definition TT : env string :=
; 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"
......@@ -51,15 +56,12 @@ Definition TT : env string :=
; ("nil", "[]")
; ("tt", "()")
; local <% msg_coq %>
; local <% @fst %>
; local <% @snd %>
; local_def <% msg_coq %>
; local <% update_contribs %>
; local <% maybe_bind_unit %>
; local <% set_done %>
; local <% validate %>
; local_def <% update_contribs %>
; local_def <% maybe_bind_unit %>
; local_def <% set_done %>
; local_def <% validate %>
].
......@@ -74,12 +76,12 @@ Time Run TemplateProgram
(* storage_def <- tmQuoteConstant "storage" false ;; *)
(* storage_body <- opt_to_template storage_def.(cst_body) ;; *)
ind <- tmQuoteInductive "msg_coq" ;;
ind_liq <- print_one_ind_body TT ind.(ind_bodies);;
t1 <- toLiquidity TT update_contribs ;;
t2 <- toLiquidity TT maybe_bind_unit ;;
t3 <- toLiquidity TT set_done ;;
t4 <- toLiquidity TT validate ;;
t5 <- toLiquidity TT receive ;;
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
......
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.
......@@ -6,8 +7,7 @@ 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 ConCert.Extraction Require Import LPretty Certified Extra.
From ConCert.Execution Require Import Containers.
From Coq Require Import List Ascii String.
......@@ -18,17 +18,15 @@ From MetaCoq.Template Require Import All.
Import ListNotations.
Import MonadNotation.
Definition PREFIX := "".
(** Quoting this runs forever, because of many dependencies *)
Definition my_lookup (m : FMap string Z) (k : string) := FMap.find k m.
(* Quote Recursively Definition zz := (my_lookup). *)
Definition lookup (m : FMap string Z) (k : string) := FMap.find k m.
(* Quote Recursively Definition lookup_quoted :=lookup. *)
(** To overcome the dependency issue, we parameterise the development with a module of the following type *)
Module Type FiniteMap.
Parameter FM : Type -> Type.
Parameter lookup : forall {V}, (string * Z) -> FM V -> option V.
End FiniteMap.
Definition map_key_type := (string * Z).
Module Interpreter (FinMap : FiniteMap).
Module Interpreter.
Inductive op : Set := Add | And | Equal.
......@@ -40,10 +38,13 @@ Module Interpreter (FinMap : FiniteMap).
Inductive value : Set := BVal : bool -> value | ZVal : Z -> value.
Definition ext_map := FinMap.FM 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.
Definition key_eq (k1 : string * Z) (k2 : string * Z)
......@@ -56,7 +57,7 @@ Module Interpreter (FinMap : FiniteMap).
match hd with
| IPushZ i => interp ext inst' (ZVal i :: s)
| IPushB b => interp ext inst' (BVal b :: s)
| IObs l i => match FinMap.lookup (l,i) ext with
| IObs l i => match lookup (l,i) ext with
| Some v => Some (v :: s)
| None => None
end
......@@ -77,30 +78,14 @@ Module Interpreter (FinMap : FiniteMap).
end
end.
(** A wrapper for calling the main functionality. It is important to be explicit about types for all the parameters of entry points *)
Definition main (param_type : string):=
"let%entry main (prog : " ++ param_type ++ ")" ++ " s ="
++ nl
++ "let s = interp (prog.(1), prog.(0) ,[]) in"
++ nl
++ "match s with"
++ nl
++ "| Some res -> ( [], res ) "
++ nl
++ "| _ -> Current.failwith s".
End Interpreter.
(** Now, we create a module of [FiniteMap] type using the [FMap] functionality *)
Module MyFinMap : FiniteMap.
Definition FM := FMap (string * Z).
Definition lookup {V} : (string * Z) -> FM V -> option V :=
FMap.find.
End MyFinMap.
Import Interpreter.
Module Interp := Interpreter MyFinMap.
Definition local_def := local PREFIX.
Import Interp.
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 :=
......@@ -110,65 +95,67 @@ Definition TT : env string :=
; remap <% nat %> "address"
; remap <% list %> "list"
; remap <% string %> "string"
; remap <% ext_map %> "((string*int),value) map"
; remap <% ext_map %> (print_finmap_type PREFIX "string * int" "value")
(* remapping operations *)
; remap <% Z.add %> "addInt"
; remap <% Z.eqb %> "eqInt"
; remap <% @MyFinMap.lookup %> "Map.find"
; 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 declarations (available in the same module or in the prelude) *)
; local <% @fst %>
; local <% @snd %>
; local <% andb %>
(* local types *)
; local <% storage %>
; local <% value %>
; local <% op %>
; local_def <% storage %>
; local_def <% instruction %>
; local_def <% value %>
; local_def <% op %>
].
(** We translate required definitions and print them into a single string containing the whole program. *)
Time Run TemplateProgram
(storage_def <- tmQuoteConstant "storage" false ;;
storage_body <- opt_to_template storage_def.(cst_body) ;;
(* ext_map_def <- tmQuoteConstant "ext_map" false ;; *)
(* ext_map_body <- opt_to_template ext_map_def.(cst_body) ;; *)
ind1 <- tmQuoteInductive "op" ;;
ind_liq1 <- print_one_ind_body TT ind1.(ind_bodies);;
ind2 <- tmQuoteInductive "instruction" ;;
ind_liq2 <- print_one_ind_body TT ind2.(ind_bodies);;
ind3 <- tmQuoteInductive "value" ;;
ind_liq3 <- print_one_ind_body TT ind3.(ind_bodies);;
t0 <- toLiquidity TT obs0 ;;
t1 <- toLiquidity TT interp ;;
res <- tmEval lazy
(prod_ops ++ nl ++ int_ops ++ nl ++ bool_ops
++ nl ++ nl
++ ind_liq1
++ nl ++ nl
++ ind_liq2
++ nl ++ nl
++ ind_liq3
++ nl ++ nl
++ "type storage = " ++ print_liq_type TT storage_body
++ nl ++ nl
++ "let%init storage = []"
++ nl ++ nl
++ t0
++ nl ++ nl
++ t1
++ nl ++ nl
++ main "(instruction list) * ((string * int,value) map)") ;;
tmDefinition "interp_extracted" res).
(** A wrapper for calling the main functionality. It is important to be explicit about types for all the parameters of entry points *)
Definition print_main (Σ : global_env) (param_type : term) : string :=
let param_liq_type := print_liq_type PREFIX TT param_type in
let func_name := PREFIX ++ "interp" in
"let%entry main (prog : " ++ param_liq_type ++ ")" ++ " s ="
++ nl
++ "let s = " ++ func_name ++ "(prog.(1), prog.(0) ,[]) in"
++ nl
++ "match s with"
++ nl
++ "| Some res -> ( [], res ) "
++ nl
++ "| _ -> Current.failwith s".
(** Adds a definition containing a "program" corresponding to the [interp] function. The "program" is a global environment containing all dependencies required for erasure and validation to go through and a quoted term*)
Run TemplateProgram (t <- erasable_program "interp" ;;
tmDefinition "interp_quoted" t).
Definition GE := interp_quoted.1.
Definition INTERP_MODULE : LiquidityModule :=
{| lm_module_name := "liquidity_interp" ;
lm_prelude := prod_ops ++ nl ++ int_ops ++ nl ++ bool_ops;
lm_adts := ["op";"instruction";"value"];
lm_functions := ["params"; "storage";"obs0";"interp"];
lm_entry_point := print_main GE <% unfolded params %>;
lm_init := "[]" |}.
(** We translate required definitions and print them into a single string containing the whole program. The definition with the corresponding code is added to Coq's environment. *)
Time Run TemplateProgram (printLiquidityModule PREFIX GE TT INTERP_MODULE).
(** The extracted program can be printed and copy-pasted to the online Liquidity editor *)
Print interp_extracted.
Print liquidity_interp.
(** or redirected to a file, creating "interp.liq.out".
The contents require further post-processing to be compiled with the Liquidity compiler.*)
Redirect "interp.liq" Compute interp_extracted. (* creates "interp.liq.out"*)
Redirect "interp.liq" Compute liquidity_interp. (* creates "interp.liq.out"*)
This diff is collapsed.
(* TODO : delete this when we merge proper utilities to fetch dependencies *)
From Coq Require Import List.
From Coq Require Import String.
From MetaCoq Require Import monad_utils.
From MetaCoq.Template Require Import All.
From MetaCoq.SafeChecker Require Import PCUICSafeChecker.
From ConCert.Extraction Require Import Certified.
Import MonadNotation.
Import ListNotations.
Fixpoint erasable_program (name : ident) : TemplateMonad program :=
cst <- tmQuoteConstant name false;;
let body := cst_body cst in
match body with
| None => tmFail ("cannot get body of constant " ++ name)
| Some body =>
(fix aux (tries : nat) (env : global_env) : TemplateMonad program :=
match tries with
| 0 => tmFail "out of fuel"
| S tries =>
let p := (env, body) in
result <- tmEval lazy (check_applied p);;
match result with
| CorrectDecl _ => ret p
| EnvError Σ (IllFormedDecl _ e) =>
match e with
| UndeclaredConstant c =>
tmMsg ("need constant " ++ c);;
cst <- tmQuoteConstant c false;;
let cst := {| cst_type := cst_type cst;
cst_body := None;
cst_universes :=
Monomorphic_ctx (LevelSetProp.of_list [], ConstraintSet.empty); |} in
let env := List.filter (fun '(n, _) => negb (n =? c)%string) env in
aux tries ((c, ConstantDecl cst) :: env)
| UndeclaredInductive c
| UndeclaredConstructor c _ =>
let name := inductive_mind c in
tmMsg ("need inductive " ++ name);;
ind <- tmQuoteInductive name;;
let ind := {| ind_finite := ind_finite ind;
ind_npars := ind_npars ind;
ind_params := ind_params ind;
ind_bodies := ind_bodies ind;
ind_universes :=
Monomorphic_ctx (LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := ind_variance ind |} in
let env := List.filter (fun '(n, _) => negb (n =? name)%string) env in
aux tries ((name, InductiveDecl ind) :: env)
| _ =>
tmFail (string_of_type_error Σ e)
end
| EnvError Σ (AlreadyDeclared id) =>
tmFail ("Already declared: " ++ id)
end
end) 1000 []
end.
This diff is collapsed.
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