fix(Wasm) --target wasm in the compiler now generates binary wasm for…

… execution

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>

Makefile.coq_modules

@@ -72,7 +72,8 @@ MODULES = \
   ErgoNNRC/Lang/ErgoNNRC \
   ErgoNNRC/Lang/ErgoNNRCSugar \
   ErgoImp/Lang/ErgoImp \
-  ErgoWasm/Lang/ErgoWasm \
+  ErgoWasmAst/Lang/ErgoWasmAst \
+  ErgoWasmBinary/Lang/ErgoWasmBinary \
   Translation/CTOtoErgo \
   Translation/ErgoNameResolve \
   Translation/ErgoAssembly \
@@ -83,7 +84,8 @@ MODULES = \
   Translation/ErgoNNRCtoErgoImp \
   Translation/ErgoImptoES6 \
   Translation/ErgoNNRCtoJava \
-  Translation/ErgoImptoWasm \
+  Translation/ErgoImptoWasmAst \
+  Translation/WasmAsttoWasmBinary \
   Compiler/ErgoDriver \
   Compiler/ErgoCompiler \
   Tests/HelloWorld

compiler/core/Compiler/ErgoDriver.v

@@ -38,7 +38,8 @@ Require Import ErgoSpec.ErgoC.Lang.ErgoCTypecheckContext.
 Require Import ErgoSpec.ErgoC.Lang.ErgoCTypecheck.
 Require Import ErgoSpec.ErgoC.Lang.ErgoCExpand.
 Require Import ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.
-Require Import ErgoSpec.ErgoWasm.Lang.ErgoWasm.
+Require Import ErgoSpec.ErgoWasmAst.Lang.ErgoWasmAst.
+Require Import ErgoSpec.ErgoWasmBinary.Lang.ErgoWasmBinary.
 Require Import ErgoSpec.Translation.CTOtoErgo.
 Require Import ErgoSpec.Translation.ErgoAssembly.
 Require Import ErgoSpec.Translation.ErgoNameResolve.
@@ -49,7 +50,8 @@ Require Import ErgoSpec.Translation.ErgoCTtoErgoNNRC.
 Require Import ErgoSpec.Translation.ErgoNNRCtoErgoImp.
 Require Import ErgoSpec.Translation.ErgoImptoES6.
 Require Import ErgoSpec.Translation.ErgoNNRCtoJava.
-Require Import ErgoSpec.Translation.ErgoImptoWasm.
+Require Import ErgoSpec.Translation.ErgoImptoWasmAst.
+Require Import ErgoSpec.Translation.WasmAsttoWasmBinary.
 
 Section ErgoDriver.
   Section CompilerPre.
@@ -322,10 +324,11 @@ Section ErgoDriver.
     Definition ergoc_module_to_wasm
                (bm:brand_model)
                (contract_name:string)
-               (p:ergo_nnrc_module) : ErgoWasm.wasm_ast :=
-      ergo_imp_module_to_wasm
-        contract_name
-        (ergo_nnrc_module_to_imp p).
+               (p:ergo_nnrc_module) : ErgoWasmBinary.wasm :=
+      ergo_wasm_ast_to_ergo_wasm
+        (ergo_imp_module_to_wasm_ast
+           contract_name
+           (ergo_nnrc_module_to_imp p)).
 
     Definition ergo_module_to_es6_top
                (inputs:list lrergo_input)
@@ -378,7 +381,7 @@ Section ErgoDriver.
                          let pc := ergo_module_to_ergoct ctxt p in
                          let pn := eolift (fun xy => ergoct_module_to_nnrc (fst xy)) pc in
                          elift (fun x => (contract_name, x,
-                                          ErgoWasm.wasm_ast_to_string (ergoc_module_to_wasm bm contract_name x))) pn)
+                                          ErgoWasmBinary.wasm_to_string (ergoc_module_to_wasm bm contract_name x))) pn)
                       ec
                 in
                 elift (fun xyz =>

compiler/core/ErgoWasm/Lang/ErgoWasm.v → compiler/core/ErgoWasmAst/Lang/ErgoWasmAst.v

@@ -27,17 +27,17 @@ Require Import ErgoSpec.Backend.Qcert.QcertEJson.
 Require Import ErgoSpec.Common.Provenance.
 Require Import ErgoSpec.Common.Result.
 
-Section ErgoWasm.
+Section ErgoWasmAst.
   Context {m : brand_model}.
 
   (** WASM programs are in AST form *)
   (** Same type as in Q*cert *)
   Definition wasm_ast : Set := wasm_ast.
-  Definition wasm_ast_eval :brand_relation_t -> wasm_ast -> jbindings -> option ejson
+  Definition wasm_ast_eval : wasm_ast -> jbindings -> option ejson
     := @wasm_ast_eval enhanced_ejson.
   Definition wasm_ast_to_string : wasm_ast -> nstring := wasm_ast_to_string.
 
-End ErgoWasm.
+End ErgoWasmAst.
 
 Extract Constant wasm_ast => "Wasm_ast.t".
 Extract Constant wasm_ast_eval => "Wasm_ast.eval".

compiler/core/ErgoWasmBinary/Lang/ErgoWasmBinary.v

@@ -0,0 +1,30 @@
+(*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
+(** ErgoWasm is an IL for Wasm *)
+
+(** * Abstract Syntax *)
+
+Require Import Qcert.WasmBinary.Lang.WasmBinary.
+
+Section ErgoWasmBinary.
+  (** WASM programs are in AST form *)
+  (** Same type as in Q*cert *)
+  Definition wasm : Set := wasm.
+  Axiom wasm_to_string : wasm -> Qcert.Utils.NativeString.nstring.
+
+End ErgoWasmBinary.
+
+Extract Constant wasm => "string".
+Extract Constant wasm_to_string => "(fun x -> x)".

compiler/core/Translation/ErgoImptoWasm.v → compiler/core/Translation/ErgoImptoWasmAst.v

@@ -26,20 +26,20 @@ Require Import ErgoSpec.Common.Names.
 Require Import ErgoSpec.Types.ErgoType.
 Require Import ErgoSpec.ErgoImp.Lang.ErgoImp.
 Require Import ErgoSpec.Backend.QLib.
-Require Import ErgoSpec.ErgoWasm.Lang.ErgoWasm.
+Require Import ErgoSpec.ErgoWasmAst.Lang.ErgoWasmAst.
 
-Section ErgoImptoWasm.
+Section ErgoImptoWasmAst.
   Local Open Scope list_scope.
 
   Context {bm:brand_model}.
 
   Axiom ergo_imp_ejson_to_wasm_ast : brand_relation_t -> ergo_imp_module -> wasm_ast.
   Definition ergo_imp_ejson_to_wasm_ast_typed := ergo_imp_ejson_to_wasm_ast brand_relation_brands.
 
-  Definition ergo_imp_module_to_wasm
+  Definition ergo_imp_module_to_wasm_ast
              (contract_name:string)
              (p:ergo_imp_module) : wasm_ast :=
     ergo_imp_ejson_to_wasm_ast_typed p.
-End ErgoImptoWasm.
+End ErgoImptoWasmAst.
 
 Extract Constant ergo_imp_ejson_to_wasm_ast => "Wasm_ast.ergo_imp_ejson_to_wasm_ast".

compiler/core/Translation/WasmAsttoWasmBinary.v

@@ -0,0 +1,36 @@
+(*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
+(** Translates ErgoNNRC to JavaScript *)
+
+Require Import String.
+Require Import List.
+
+Require Import Qcert.JavaScriptAst.JavaScriptAstRuntime.
+Require Import Qcert.Driver.CompDriver.
+Require Import ErgoSpec.Version.
+Require Import ErgoSpec.Utils.Misc.
+Require Import ErgoSpec.Common.Result.
+Require Import ErgoSpec.Common.Names.
+Require Import ErgoSpec.Types.ErgoType.
+Require Import ErgoSpec.ErgoImp.Lang.ErgoImp.
+Require Import ErgoSpec.Backend.QLib.
+Require Import ErgoSpec.ErgoWasmAst.Lang.ErgoWasmAst.
+Require Import ErgoSpec.ErgoWasmBinary.Lang.ErgoWasmBinary.
+
+Section WasmAsttoWasmBinary.
+  Axiom ergo_wasm_ast_to_ergo_wasm : wasm_ast -> wasm.
+End WasmAsttoWasmBinary.
+
+Extract Constant ergo_wasm_ast_to_ergo_wasm => "Wasm.Encode.encode".

compiler/lib/config.ml

@@ -43,15 +43,15 @@ let extension_of_lang lang =
   | Ergo -> ".ergo"
   | ES6 -> ".js"
   | Java -> ".java"
-  | Wasm -> ".wat"
+  | Wasm -> ".wasm"
   end
 
 let script_lang_of_lang lang =
   begin match lang with
   | Ergo -> ".ergo"
   | ES6 -> ".js"
   | Java -> ".java"
-  | Wasm -> ".wat"
+  | Wasm -> ".wasm"
   end
 
 let script_lang_of_target s =