Merge pull request #6 from wilbowma/canon

Polishing commits

README.md

@@ -6,27 +6,27 @@ The goal of this model is to provide a starting point for modeling extensions to
 For example, for a research project we have built an extended type system for WebAssembly on top of this model.
 There are two straightforward ways to build language extensions using this model:
 
-1. The preferred way is to use Redex's `define-extended-*` forms to explicity extend the basic WebAssembly specification. For example, using `define-extended-language` to extend the base WebAssembly syntax with new types or instructions, and then using `define-extended-relation` and `define-extended-judgment` when necessary, or creating new reduction relations and judgement forms.
+1. The preferred way is to use Redex's `define-extended-*` forms to explicitly extend the basic WebAssembly specification. For example, using `define-extended-language` to extend the base WebAssembly syntax with new types or instructions, and then using `define-extended-relation` and `define-extended-judgment` when necessary, or creating new reduction relations and judgement forms.
 2. Create a fork of this repository, and change the language definition, reduction relation, and judgment forms as needed.
 
 ## Syntax
 The syntactic representation used in the model is `s-expression` based.
-It contains a few more parentheses than are present in the original grammer (to speed up parsing).
+It contains a few more parentheses than are present in the original grammar (to simplify parsing).
 Other small differences include:
 * The removal of the `.` character between types and a number of terminal expressions (e.g., `i32.add` becomes `(i32 add)`).
 * The explicit enumeration of the `sx` non-terminal in binops and relops.
 * Optional terms are handled via enumeration or faked using lists (there's a hidden low-priority TODO to clean this up).
 
-The WASM Redex language is defined in `Syntax.rkt`. A typeset version can be viewed below and uses similar terminology to the WebAssembly paper.
+The WASM Redex syntax is defined in `Syntax.rkt`. A typeset version can be viewed below and uses similar terminology to the WebAssembly paper.
 
 ![The WebAssembly language syntax](Syntax.pdf)
 
 ## Semantics
 WebAssembly introduces several administrative instructions to define the semantics.
 Therefore, we extend the base WebAssembly syntax with these forms to create a run-time language, `WASM-Admin`, defined in ![Semantics/AdministrativeSyntax.rkt](Semantics/AdministrativeSyntax.rkt)
 
-The reduction relation is in the form of a small-step operational semantics inside an evaluation context.
-The evaluation context, L, keeps track of the list of instructions surrounding the current code block.
+The reduction relation is a small-step operational semantics inside an evaluation context.
+The evaluation context, `L`, keeps track of the list of instructions surrounding the current code block.
 Evaluation contexts can be thought of as being akin to a stack frame.
 There are four parameters: `(s v* e*) (-> i) (s v* e*)` with roughly equivalent meaning to the ones in the paper:
 * `s`: the store which keeps track of all instances (modules), as well as all function tables and memories.
@@ -46,13 +46,13 @@ The typing rules for instructions are defined in ![Validation/InstructionTyping.
 The typing rules for modules and module objects (tables, memories, globals, and functions) are defined in `Validation/ModuleTyping.rkt`,
 which provides the `⊢-module-func`, `⊢-module-global`, `⊢-module-table`, `⊢-module-memory`, and `⊢-module` judgment-forms.
 
-In `Validation/Typechecking.rkt` we provide an algorithm for finding a derivation that types a given syntax object.
-This algorithm is more complicated than the reference validation algorithm since it needs to synthesize the actual program stacks for instructions after unconditional branches and `unreachable`.
+In `Validation/Typechecking.rkt` we provide an inference algorithm for finding a typing derivation over syntax.
+This algorithm is more complicated than the reference validation algorithm since it produces a derivation witness, and needs to synthesize the actual program stacks for instructions after unconditional branches and `unreachable`.
 
 The typechecking algorithm is split between typechecking functions for each judgment-form.
 * `typecheck-module` produces derivations of `⊢-module` for a given `mod`.
 * `typecheck-table` produces derivations of `⊢-module-table` for a given context and `tab`.
 * `memory-derivation` produces derivations of `⊢-module-memory` for a given context and `mem`.
 * `typecheck-global` produces derivations of `⊢-module-global` for a given context and `glob`.
 * `typecheck-func` produces derivations of `⊢-module-func` for a given context and `func`.
-* `typecheck-ins` produces derivaitions of `⊢` for a given context, `e*`, and pre- and post-stacks.
+* `typecheck-ins` produces derivations of `⊢` for a given context, `e*`, and pre- and post-stacks.

Semantics/SimpleOps.rkt

@@ -14,59 +14,59 @@
 ; equivalent to unop_t(c)
 (define-metafunction WASM-Admin
   eval-unop : unop t c -> c
-  
+
   [(eval-unop clz t c) ,(sized-clz (term (bit-width t)) (term c))]
   [(eval-unop ctz t c) ,(sized-ctz (term (bit-width t)) (term c))]
   [(eval-unop popcnt t c) ,(sized-popcnt (term (bit-width t)) (term c))]
   [(eval-unop abs t c) ,(abs (term c))]
   [(eval-unop neg t c) ,(- (term c))]
-  
+
   [(eval-unop sqrt f32 c)
    ,(if (negative? (term c))
         +nan.0
         (flsingle (flsqrt (term c))))]
-  
+
   [(eval-unop sqrt f64 c)
    ,(if (negative? (term c))
         +nan.0
         (flsqrt (term c)))]
-  
+
   [(eval-unop ceil t c) ,(ceiling (term c))]
   [(eval-unop floor t c) ,(floor (term c))]
   [(eval-unop nearest t c) ,(round (term c))])
 
 ; equivalent to binop_t(c1, c2)
 (define-metafunction WASM-Admin
   eval-binop : binop t c c -> (c ...)
-  
+
   [(eval-binop add inn c_1 c_2) (,(sized-add (term (bit-width inn)) (term c_1) (term c_2)))]
   [(eval-binop sub inn c_1 c_2) (,(sized-sub (term (bit-width inn)) (term c_1) (term c_2)))]
   [(eval-binop mul inn c_1 c_2) (,(sized-mul (term (bit-width inn)) (term c_1) (term c_2)))]
-  
+
   [(eval-binop div-s inn c_1 c_2)
    (,(sized-signed-div (term (bit-width inn)) (term c_1) (term c_2)))
    (side-condition (not (equal? (term c_2) 0)))
    or
    ()]
-  
+
   [(eval-binop div-u inn c_1 c_2)
    (,(sized-unsigned-div (term (bit-width inn)) (term c_1) (term c_2)))
    (side-condition (not (equal? (term c_2) 0)))
    or
    ()]
-  
+
   [(eval-binop rem-s inn c_1 c_2)
    (,(sized-signed-rem (term (bit-width inn)) (term c_1) (term c_2)))
    (side-condition (not (equal? (term c_2) 0)))
    or
    ()]
-  
+
   [(eval-binop rem-u inn c_1 c_2)
    (,(sized-unsigned-rem (term (bit-width inn)) (term c_1) (term c_2)))
    (side-condition (not (equal? (term c_2) 0)))
    or
    ()]
-  
+
   [(eval-binop and inn c_1 c_2) (,(bitwise-and (term c_1) (term c_2)))]
   [(eval-binop or inn c_1 c_2) (,(bitwise-ior (term c_1) (term c_2)))]
   [(eval-binop xor inn c_1 c_2) (,(bitwise-xor (term c_1) (term c_2)))]
@@ -75,21 +75,21 @@
   [(eval-binop shr-u inn c_1 c_2) (,(sized-unsigned-shr (term (bit-width inn)) (term c_1) (term c_2)))]
   [(eval-binop rotl inn c_1 c_2) (,(sized-rotl (term (bit-width inn)) (term c_1) (term c_2)))]
   [(eval-binop rotr inn c_1 c_2) (,(sized-rotr (term (bit-width inn)) (term c_1) (term c_2)))]
-  
-  
+
+
   [(eval-binop add f32 c_1 c_2) (,(flsingle (fl+ (term c_1) (term c_2))))]
   [(eval-binop sub f32 c_1 c_2) (,(flsingle (fl- (term c_1) (term c_2))))]
   [(eval-binop mul f32 c_1 c_2) (,(flsingle (fl* (term c_1) (term c_2))))]
   [(eval-binop div f32 c_1 c_2) (,(flsingle (fl/ (term c_1) (term c_2))))]
-  
+
   [(eval-binop add f64 c_1 c_2) (,(fl+ (term c_1) (term c_2)))]
   [(eval-binop sub f64 c_1 c_2) (,(fl- (term c_1) (term c_2)))]
   [(eval-binop mul f64 c_1 c_2) (,(fl* (term c_1) (term c_2)))]
   [(eval-binop div f64 c_1 c_2) (,(fl/ (term c_1) (term c_2)))]
-  
+
   [(eval-binop min fnn c_1 c_2) (,(flmin (term c_1) (term c_2)))]
   [(eval-binop max fnn c_1 c_2) (,(flmax (term c_1) (term c_2)))]
-  
+
   [(eval-binop copysign fnn c_1 c_2)
    (,(if (or (negative? (term c_2))
              (fl= (term c_2) -0.0))
@@ -105,20 +105,20 @@
 
 (define-metafunction WASM-Admin
   eval-relop : relop t c c -> c
-  
+
   [(eval-relop eq t c_1 c_2) (bool ,(= (term c_1) (term c_2)))]
   [(eval-relop ne t c_1 c_2) (bool ,(not (= (term c_1) (term c_2))))]
 
   [(eval-relop lt-u t c_1 c_2) (bool ,(< (term c_1) (term c_2)))]
   [(eval-relop gt-u t c_1 c_2) (bool ,(> (term c_1) (term c_2)))]
   [(eval-relop le-u t c_1 c_2) (bool ,(<= (term c_1) (term c_2)))]
   [(eval-relop ge-u t c_1 c_2) (bool ,(>= (term c_1) (term c_2)))]
-  
+
   [(eval-relop lt-s t c_1 c_2) (bool ,(< (term (signed t c_1)) (term (signed t c_2))))]
   [(eval-relop gt-s t c_1 c_2) (bool ,(> (term (signed t c_1)) (term (signed t c_2))))]
   [(eval-relop le-s t c_1 c_2) (bool ,(<= (term (signed t c_1)) (term (signed t c_2))))]
   [(eval-relop ge-s t c_1 c_2) (bool ,(>= (term (signed t c_1)) (term (signed t c_2))))]
-  
+
   [(eval-relop lt t c_1 c_2) (bool ,(fl< (term c_1) (term c_2)))]
   [(eval-relop gt t c_1 c_2) (bool ,(fl> (term c_1) (term c_2)))]
   [(eval-relop le t c_1 c_2) (bool ,(fl<= (term c_1) (term c_2)))]
@@ -131,7 +131,7 @@
   [(do-convert i64 i32 () c) (,(to-unsigned-sized 32 (term c)))]
   [(do-convert i32 i64 (signed) c) (,(to-unsigned-sized 64 (to-signed-sized 32 (term c))))]
   [(do-convert i32 i64 (unsigned) c) (c)]
-  
+
   [(do-convert f64 f32 () c) (,(flsingle (term c)))]
   [(do-convert f32 f64 () c) (c)]
 
@@ -149,9 +149,9 @@
                       (expt 2 (sub1 (term (bit-width inn))))))
    or
    ()]
-  
+
   [(do-convert fnn inn (unsigned) c)
    (,(fl->exact-integer (truncate (term c))))
    (side-condition (< -1 (truncate (term c)) (expt 2 (term (bit-width inn)))))
    or
-   ()])
+   ()])