7 files changed, 77 insertions(+), 22 deletions(-)

M WebAssembly/Demo/Demo.thy
D WebAssembly/Demo/add.wasm
A WebAssembly/Demo/block.wat
A WebAssembly/Demo/linear.wat
M WebAssembly/PC_Interpreter/Interpreter.thy
M WebAssembly/SML/Printing.thy
M WebAssembly/SML/Reflect.thy

@@ 2,28 2,59 @@ theory Demo
   imports WebAssembly_SML.Reflect Show.Show_Instances
 begin
 
+text\<open>Helper function for running\<close>
 ML\<open>
-val (module, s, i, exps, start) = load @{theory} "block.wasm"
-val state = Wasm.c_init s (Wasm.nat_of_integer 0) []
+fun run_and_show state fuel =
+  let
+    val _ = if fuel > 0 then run_and_show state (fuel - 1) else ()
+    val s's = case Wasm.c_run (Wasm.nat_of_integer fuel) state of
+        (Wasm.Set s') => s'
+      | _ => raise (Fail "unexpected set")
+  in
+    writeln ("After " ^ (Int.toString fuel) ^ " steps:");
+    if length s's = 1 then
+      let
+        val s' = List.nth (s's, 0)
+      in
+        writeln ("  program counter: " ^ (Int.toString (Wasm.integer_of_nat (Wasm.c_ei (Wasm.c_pc s')))));
+        writeln ("  value stack:     " ^ (Wasm.show_vs (Wasm.val_stack s')));
+        writeln ("  reconstruction:  " ^ Wasm.show_es (Wasm.c_es s'));
+        if Wasm.terminated s' then writeln "  TERMINATED! ==================================" else ()
+      end
+    else
+      writeln ("  " ^ Int.toString (length s's) ^ " states")
+  end
+
+fun show_function s i =
+  let
+    val es = case List.nth (Wasm.funcs s, i) of
+      Wasm.Func_native (_, _, _, es) => es
+      | _ => raise (Fail "not a native function")
+    val r = Wasm.show_b_es es
+  in
+    writeln r
+  end
 \<close>
 
+text\<open>
+Load a module from a binary file.
+This includes full type-checking and instantiation.
+\<close>
+ML\<open>val (module, s, i, exps, start) = load @{theory} "block.wasm"\<close>
 
-ML\<open>
-val _ = let
-  val (Wasm.Set s') = Wasm.c_run  (Wasm.nat_of_integer 4) state
-  val r = Wasm.show_es (Wasm.c_es (List.nth (s', 0)))
-in
-  writeln r
-end
+text\<open>
+Inspect the raw code of function 0 in the instantiated store.
 \<close>
+ML\<open>val _ = show_function s 0\<close>
 
-ML\<open>
-let
-  val Wasm.Func_native (_, _, _, es) = List.nth (Wasm.funcs s, 0)
-  val r = Wasm.show_b_es es
-in
-  writeln r
-end
+text\<open>
+Initialize our interpreter using function 0 as the entrypoint
+\<close>
+ML\<open>val state = Wasm.c_init s (Wasm.nat_of_integer 0) []\<close>
+
+text\<open>
+Run and reconstruct!
 \<close>
+ML\<open>val _ = run_and_show state 10\<close>
 
 end=
\ No newline at end of file

@@ 0,0 1,13 @@
+(module
+ (export "block" (func $block))
+ (func $block (result i32)
+  (local i32)
+  i32.const 13
+  i32.const 34
+  block (param i32) (result i32)
+   local.get 0
+   i32.add
+  end
+  drop
+ )
+)

@@ 0,0 1,10 @@
+(module
+ (export "linear" (func $linear))
+ (func $linear (result i32)
+  i32.const 34
+  i32.const 13
+  i32.sub
+  i32.const 2
+  i32.mul
+ )
+)

@@ 56,13 56,13 @@ Cheating function to forcefully bring a list to at least a given length.
 Our use-cases would not necessarily need it as the lengths could be shown from typing too,
 but this requires significant additional effort and it is irrelevant for what we are trying to show.
 \<close>
-definition fill_length :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "fill_length n l \<equiv> l @ replicate (n - length l) undefined"
+definition fill_length :: "nat \<Rightarrow> v list \<Rightarrow> v list" where
+  "fill_length n l \<equiv> l @ replicate (n - length l) (ConstInt32 0)" \<comment>\<open>ConstInt32 0 could be just undefined here. But then SML crashes because it's strict :-(\<close>
 
-definition rip :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+definition rip :: "nat \<Rightarrow> v list \<Rightarrow> v list" where
   "rip n l = fill_length n (take n l)"
 
-definition tear :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+definition tear :: "nat \<Rightarrow> v list \<Rightarrow> v list" where
   "tear n l \<equiv> fill_length n (tail n l)"
 
 definition c_return_vs :: "c_state \<Rightarrow> v list" where

@@ 272,6 272,7 @@ instance apply standard unfolding equal_mem_rep_def .. end
 
 definition show_es :: "e list \<Rightarrow> String.literal" where "show_es es \<equiv> String.implode (show es)"
 definition show_b_es :: "b_e list \<Rightarrow> String.literal" where "show_b_es bs \<equiv> String.implode (show bs)"
+definition show_vs :: "v list \<Rightarrow> String.literal" where "show_vs vs \<equiv> String.implode (show vs)"
 
 export_code open m_imports module_type_checker interp_instantiate typing run c_run
   in SML module_name WasmRef_Isa file_prefix WasmRef_Isa

@@ 15,8 15,8 @@ code_reflect Wasm
     and module_import_ext = _ and module_export_ext = _
     and s_ext = _
   functions m_imports module_type_checker interp_instantiate typing run c_run
-    nat_of_integer SML_int32_to_isabelle_int32 SML_int64_to_isabelle_int64 SML_char_to_isabelle_byte
-    c_init c_step c_run c_es s.funcs show_es show_b_es Func_native set
+    nat_of_integer integer_of_nat SML_int32_to_isabelle_int32 SML_int64_to_isabelle_int64 SML_char_to_isabelle_byte
+    c_init c_step c_run c_es s.funcs show_es show_b_es Func_native set terminated val_stack c_ei c_pc show_vs
 
 ML_file "Decode.ML"