forked from AU-COBRA/ConCert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
CrowdfundingLiquidity.v
139 lines (117 loc) · 5.28 KB
/
CrowdfundingLiquidity.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
(** * Extraction of a crowdfunding contract *)
From Coq Require Import ZArith.
From Coq Require Import String.
From ConCert.Embedding Require Import Notations.
From ConCert.Extraction Require Import LiquidityExtract.
From ConCert.Extraction Require Import LiquidityPretty.
From ConCert.Extraction Require Import Common.
From ConCert.Embedding.Extraction Require Import PreludeExt.
From ConCert.Embedding.Extraction Require Import SimpleBlockchainExt.
From ConCert.Examples.Crowdfunding Require Import CrowdfundingDataExt.
From ConCert.Examples.Crowdfunding Require Import CrowdfundingExt.
From MetaCoq.Template Require Import All.
From MetaCoq.Erasure.Typed Require Import ResultMonad.
Import AcornBlockchain.
Import MCMonadNotation.
Import CrowdfundingContract.
Import Receive.
Local Open Scope string_scope.
Open Scope Z.
Definition PREFIX := "".
(** A translation table for definitions we want to remap. The corresponding top-level definitions will be *ignored* *)
Definition TT_remap : list (kername * String.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 <%% ConCert.Execution.ResultMonad.result %%> "result"
; remap <%% Maps.addr_map_coq %%> "(address,tez) map"
; remap <%% SimpleActionBody_coq %%> "operation"
(* operations *)
; 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 <%% Maps.add_map %%> "Map.add"
; remap <%% lookup_map' %%> "Map.find" ].
(** A translation table of constructors and some constants. The corresponding definitions will be extracted and renamed. *)
Definition TT_rename :=
[ ("Z0" ,"0DUN")
; ("O", "0")
; ("nil", "[]")
; ("mnil", "Map []")
; ("Ok", "Ok")
; ("Err", "Err")
; ("tt", "()")
; ("true", "true")
; ("false", "false")].
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 0" ++ Common.nl ++ Common.nl++
"let%entry main (msg : msg_coq)(st : ((timestamp * (tez * address)) * ((address,tez) map * bool))) = wrapper msg st".
Notation storage := ((time_coq × Z × address_coq) × Maps.addr_map_coq × bool).
Notation params := ((time_coq × address_coq × Z × Z) × msg_coq).
Definition Error : Type := nat.
Definition default_error : Error := 1%nat.
Definition crowdfunding_init (ctx : SimpleCallCtx)
(setup : (time_coq × Z × address_coq))
: ConCert.Execution.ResultMonad.result storage Error :=
if ctx.2.2.1 =? 0
then ConCert.Execution.ResultMonad.Ok (setup, (Maps.mnil, false))
else ConCert.Execution.ResultMonad.Err default_error.
(* (unfolded Init.init) setup ctx. *)
Definition crowdfunding_receive
(params : params)
(st : storage)
: ConCert.Execution.ResultMonad.result (list SimpleActionBody_coq × storage) Error :=
match receive params.2 st params.1 with
| Some v => ConCert.Execution.ResultMonad.Ok v
| None => ConCert.Execution.ResultMonad.Err default_error
end.
Definition CROWDFUNDING_MODULE :
LiquidityMod params SimpleCallCtx (time_coq × Z × address_coq) storage SimpleActionBody_coq nat :=
{| (* a name for the definition with the extracted code *)
lmd_module_name := "liquidity_crowdfunding" ;
(* definitions of operations on pairs and ints *)
lmd_prelude :=
LiquidityPrelude
++ Common.nl
++ "type storage = ((timestamp * (tez * address)) * ((address,tez) map * bool))";
(* initial storage *)
lmd_init := crowdfunding_init ;
(* init requires some extra operations *)
lmd_init_prelude :=
"let fst (p : 'a * 'b) : 'a = p.(0) in"
++ Common.nl
++ "let snd (p : 'a * 'b) : 'b = p.(1) in"
++ Common.nl
++ "let eqTez (a : tez) (b : tez) = a = b in"
++ Common.nl
++ "let default_error = 1 in" ;
(* the main functionality *)
lmd_receive := crowdfunding_receive ;
(* code for the entry point *)
lmd_entry_point := printWrapper (PREFIX ++ "crowdfunding_receive") ++ Common.nl
++ printMain |}.
(** We run the extraction procedure inside the [TemplateMonad].
It uses the certified erasure from [MetaCoq] and the certified deboxing procedure
that removes application of boxes to constants and constructors. *)
Time MetaCoq Run
(t <- liquidity_extraction PREFIX TT_remap TT_rename [] CROWDFUNDING_MODULE ;;
tmDefinition (String.of_string CROWDFUNDING_MODULE.(lmd_module_name)) t
).
(** We redirect the extraction result for later processing and compiling with the Liquidity compiler *)
Redirect "../extraction/tests/extracted-code/liquidity-extract/CrowdfundingCertifiedExtraction.liq"
Compute liquidity_crowdfunding.