Merge pull request #39 from raoxiaojia/2.0

Wasm 2.0 Update

.github/workflows/main.yml

@@ -3,6 +3,12 @@ name: Test compilation
 on:
   push:
   pull_request:
+    types: 
+      - opened
+      - synchronize
+      - reopened
+      - ready_for_review
+
   workflow_dispatch:
     inputs:
 

LICENSE.txt

@@ -1,6 +1,6 @@
 The MIT License (MIT)
 
-Copyright (c) 2019-2023  Martin Bodin, Philippa Gardner, Jean Pichon, Xiaojia Rao, Conrad Watt
+Copyright (c) 2019-2024  Martin Bodin, Philippa Gardner, Jean Pichon, Xiaojia Rao, Conrad Watt
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,12 +1,11 @@
 # wasm_coq
-WebAssembly (aka Wasm) 1.0 formalisation in Coq, based on the [official formalisation](https://www.w3.org/TR/wasm-core-1/).
-Our definitions and proofs initially drew from those given in the [Isabelle mechanisation of Conrad Watt](https://www.isa-afp.org/entries/WebAssembly.html).
+A WebAssembly (aka Wasm) formalisation in Coq, based on the [official specification](https://webassembly.github.io/spec/core/).
 
-(C) M. Bodin, P. Gardner, J. Pichon, C. Watt, X. Rao 2019-2023 - see LICENSE.txt
+(C) M. Bodin, P. Gardner, J. Pichon, C. Watt, X. Rao 2019-2024 - see LICENSE.txt
 
 The quotes from the WebAssembly standard (starting with `std-doc`) are (C) their respective authors.
 
-This work is in progress. While our initial work used the definitions published in PLDI'17, we have now adapted the mechanisation to Wasm 1.0., the specification as ratified by the W3C. A large part of the work has been published at [FM'21](https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4), with more additions to the repository since then.
+The current master branch formalises Wasm version 2.0, plus additional subtyping systems from the future funcref/GC extension proposals. A large part of the old Wasm 1.0 formalisation has been published at [FM'21](https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4), with many additions to the repository since then.
 
 # Components of the Repository
 
@@ -22,11 +21,11 @@ This work is in progress. While our initial work used the definitions published
 - [x] Soundness results for module instantiation.
 - [x] Proof carrying interpreter deriving progress.
 - [x] Interpreter with optimised context representations.
+- [x] Updates for Wasm 2.0 (except SIMD and new numerics ops) + subtyping systems.
 
 ## Unmerged/Future Work
 - [ ] Validate WasmRef-Coq (conformance tests).
-- [ ] Updates for Wasm 2.0 (except SIMD).
-- [ ] Updates for further extension proposals (SIMD, GC, tail calls, etc).
+- [ ] Updates for further extension proposals.
 
 # Program Logic
 
@@ -35,6 +34,7 @@ This is migrated from an older build for the [artefact](https://zenodo.org/recor
 
 # Binary Parser (experimental)
 This repository contains some experimental work on a parser for the binary format which is currently unverified.
+As the parser forms a part of the extracted interpreter, any error in the parser would result in the interpreter reporting `syntax error` for some valid Wasm binaries. Bug reports are appreciated!
 
 # Usage
 
@@ -48,10 +48,6 @@ opam repo add coq-released https://coq.inria.fr/opam/released
 opam install .
 ```
 
-## Build Based on Esy
-
-The previous esy-based build is now deprecated; it is moved to esy branch.
-
 ## Testing the Installation
 
 The project comes with a small set of tests for the extracted interpreter:
@@ -63,71 +59,82 @@ dune test
 
 A file `wasm_coq_interpreter` will have been generated under `_build/install`.
 It takes as argument a list of Wasm files, followed by a function name to run (with the `-r` flag).
-For instance, to interpret the function `main` defined in [tests/floatmul.wasm](tests/floatmul.wasm), run:
+For instance, to interpret the function `main` defined in [tests/add.wasm](tests/add.wasm), run:
 ```bash
-dune exec -- wasm_coq_interpreter tests/floatmul.wasm -r main
+dune exec -- wasm_coq_interpreter tests/add.wasm -r main
 ```
 The interpreter can display intermediate states of the operational semantics:
 ```bash
-dune exec -- wasm_coq_interpreter tests/floatmul.wasm -r main --vi
+dune exec -- wasm_coq_interpreter tests/add.wasm -r main --vi
 ```
 would produce:
 ```bash
-parsing OK
+parsing OK                            
 instantiation OK
+
+Post-instantiation stage for table and memory initialisers...
+step 1:
+(empty)
+
+step 2:
+Value:
+(empty)
+success after 2 steps
+
+Instantiation success
 interpreting OK
 step 0:
 
-invoke 0
+Executing configuration:
+frame 0
 with values (empty)
+  invoke 0
+end frame
 
 step 1:
-normal
-  local 1
-  with values (empty)
-    block f32
-        f32.const 4350553f
-        f32.const 431c4000
-        f32.mul
-    end
-  end local
+frame 0
 with values (empty)
-and store unchanged
-step 2:
-normal
-  local 1
+  frame 1
   with values (empty)
     label 1
     label_cont
-      f32.const 4350553f
-      f32.const 431c4000
-      f32.mul
+      i32.const 40
+      i32.const 2
+      i32.add
     end label
-  end local
+  end frame
+end frame
+
+step 2:
+frame 0
 with values (empty)
-and store unchanged
-step 3:
-normal
-  local 1
+  frame 1
   with values (empty)
     label 1
     label_cont
-      f32.const 46fe500f
+      i32.const 42
     end label
-  end local
+  end frame
+end frame
+
+step 3:
+frame 0
 with values (empty)
-and store unchanged
-step 4:
-normal
-  local 1
+  frame 1
   with values (empty)
-    f32.const 46fe500f
-  end local
+    i32.const 42
+  end frame
+end frame
+
+step 4:
+frame 0
 with values (empty)
-and store unchanged
+  i32.const 42
+end frame
+
 step 5:
-normal
-  f32.const 46fe500f
-with values (empty)
-and store unchanged
+Value:
+i32.const 42
+
+success after 5 steps
 ```

changelogs/v2.0.md

@@ -0,0 +1,76 @@
+# Release 2.0 + Subtyping
+
+This release for Wasm 2.0 + Subtyping implemented the following changes in the official spec release 2.0:
+- Multiple-value blocks;
+- Reference types;
+- Table instructions;
+- Multiple tables;
+- Bulk memory and table instructions.
+
+In addition, this release also implemented the subtyping system from the future funcref/GC proposals.
+
+The new sign extension, non-trapping float-to-int conversion, and vector types are added but without any concrete implementation.
+
+## Updated Components:
+- [x] Base opsem/typing definitions;
+- [x] Preservation theorems;
+- [x] Interpreter and progress theorem;
+- [x] Instantiation;
+- [x] Instantiation soundness theorems;
+- [x] Type checker;
+- [x] Type checker correctness theorem;
+- [x] Binary printer/parser;
+- [x] Code pretty printer;
+- [x] Subtyping.
+
+# Major Structural Changes
+
+## Values vs Instructions
+Due to the introduction of reference values, values are no longer necessarily basic instructions; function references and external references are expressed as administrative instructions due to their direct usage of store addresses instead of module indices. This change has broken some assumptions that many original proofs and definitions based on -- mostly those related to value typing (see below). 
+Total and partial conversion operations are now provided for conversion between values and their corresponding instructions:
+- `v_to_e/e_to_v` for total conversions;
+- `e_to_v_opt` for partial operations.
+
+## Value Typing and the Store
+Due to the use of store addresses, the new reference values can only be typed given a store. This necessitated the introduction
+of a separate `value_typing` relation with respect to a store. In addition, value typing relation now has to be done at the
+`e_typing` level (for administrative instructions) as they can no longer be converted to basic instructions and typed using the `const` rule in `be_typing`. New value typing inversion lemmas were added to help reasoning with this change; search for terms involving `value_typing` and `values_typing`.
+
+## Threads
+Threads are now properly spelt out as a separate type that constitutes the configuration tuple. The old thread-related definitions (e.g. `s_typing`) are renamed to the names used in the standard (e.g. `thread_typing`).
+
+## Type System and Subtyping
+In addition, this release also implements subtyping introduced in the future funcret/GC proposal as a forward-looking move. There is currently no observable effect in Wasm 2.0 except for typing instructions past unconditional branches, as there is no non-trivial subtypings between any of the base value types. There exists a principal type (potentially with some free type parameters) for every value/instruction, which all possible types of it are supertypes of.
+The largest impact of this type system change is that, in the future, values can no longer uniquely typed even if it is well typed. This is not the case in Wasm 2.0 yet, but examples can be introduced in future proposals.
+The old `weakening` typing rules are replaced by a subtyping rule as a result of this change, which reflects the shift in the future proposals.
+
+# Refactorings and Feature Improvements
+
+## Host Formulation
+The parametric host language is now defined using typeclasses. 
+The main major benefit is the automatic filling of implicit host parameter, instead of needing to redefine all operations involving anything downstream from function instances and stores. The proof context is also greatly simplified since all these redefinitions no longer exist to occupy a major chunk of the buffer window.
+
+## Numerics
+- Refactored the old collection of conversion operations *cvtop* to be split up by their individual constructors to better match the spec.
+
+## Name Changes
+- Changed the name of some types, instructions, and constructors to better match the official spec.
+- Instance indices are now simplified to the base `u32` type without additional constructors.
+
+## Pretty Printer
+- Implemented pretty printing for conversion operations.
+
+## Typing
+- Massively improved the scope and automation of the typing inversion lemmas.
+- Provided a new tactic `resolve_e_typing` that automatically tries to resolve `e_typing` goals, dealing mostly with the operands.
+- Provided a separate file for the new subtyping lemmas and tactics.
+
+## Type Checker
+- Completely reimplemented the type checker, which should now be slightly more efficient (although this should hardly be observable).
+
+## Miscellaneous
+- Introduced many additional excerpts in comments from the official spec for various definitions.
+
+# Bug Fixes
+- Fixed a bug where the binary printer incorrectly prints all types of reinterpret conversions to 0xBC.
+- Fixed a bug where the binary printer sometimes prints indices via a conversion to nat first.

coq-wasm.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1"
+version: "2.0"
 synopsis: "Wasm formalisation in Coq"
 description:
   "Wasm formalisation in Coq, following the AFP formalisation of Conrad Watt"

dune-project

@@ -2,7 +2,7 @@
 (using coq 0.2)
 (using mdx 0.2)
 (name coq-wasm)
-(version 0.1)
+(version 2.0)
 
 (generate_opam_files true)
 (license MIT)

src/convert.ml

@@ -46,13 +46,6 @@ let to_triple (a, b, c) = Extract.Pair (Extract.Pair (a, b), c)
 
 let from_string str = Utils.implode str
 
-let string_of_value =
-  Extract.value_rec_safe
-    (fun v -> Printf.sprintf "Int32: %s" (from_string (Extract.pp_i32 v)))
-    (fun v -> Printf.sprintf "Int64: %s" (from_string (Extract.pp_i64 v)))
-    (fun v -> Printf.sprintf "Float32: %s" (from_string (Extract.pp_f32 v)))
-    (fun v -> Printf.sprintf "Float64: %s" (from_string (Extract.pp_f64 v)))
-
 let rec to_nat = function
   | 0 -> Extract.O
   | n when n > 0 -> Extract.S (to_nat (n - 1))

src/convert.mli

@@ -51,6 +51,4 @@ val from_positive : Extract.positive -> int
 (** Convert [Extract.z] to [int]. *)
 val from_z : Extract.z -> int
 
-(** Print a Wasm value. *) (* TODO: Removed, now subsumed by [Execute.Interpreter.pp_values]. *)
-val string_of_value : Extract.value0 -> string