Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Geller, Adam T.
Master of Science - MSc
University of British Columbia
Downloading and executing untrusted code is inherently unsafe, but also something that happens often on the internet. Therefore, untrusted code often requires run-time checks to ensure safety during execution. These checks compromise performance and may be unnecessary. We present the Wasm-prechk language, an assembly language based on WebAssembly that is intended to ensure safety while justifying the static elimination of run-time checks.
An Indexed Type System for Faster and SaferWebAssemblybyAdam T. Gellera thesis submitted in partial fulfillmentof the requirements for the degree ofMaster of Scienceinthe faculty of graduate and postdoctoralstudies(Computer Science)The University Of British Columbia(Vancouver)August 2020© Adam T. Geller, 2020The following individuals certify that they have read, and recommend tothe Faculty of Graduate and Postdoctoral Studies for acceptance, the thesisentitled:An Indexed Type System for Faster and Safer WebAssemblysubmitted by Adam T. Geller in partial fulfillment of the requirements forthe degree of Master of Science in Computer Science.Examining Committee:William J. Bowman, Computer ScienceCo-supervisorIvan Beschastnikh, Computer ScienceCo-supervisorRonald Garcia, Computer ScienceAdditional ExamineriiAbstractDownloading and executing untrusted code requires careful considerationsto ensure that it is safe, but also something that happens often on theinternet. Therefore, untrusted code often requires run-time checks to ensuresafety during execution. These checks compromise performance and may beunnecessary. We present the Wasm-prechk language, an assembly languagebased on WebAssembly that is intended to ensure the same level of safety asWebAssembly while justifying the static elimination of run-time checks.iiiLay SummaryDownloading and running code from unknown sources is unsafe, but also quitecommon. Ill-behaved or erroneous code can expose your data or crash yourbrowser. Unfortunately, mitigating these risks often slows down programs.WebAssembly is a language supported by many browsers and designed to beboth fast and safe, but the language still requires potentially unnecessarysafety check which make websites slower and less efficient.We have designed a programming language based on WebAssembly, calledWasm-prechk, that is meant to be as safe as WebAssembly without requiringas many safety check. Wasm-prechk uses a more expressive type systemthen WebAssembly to help the computer reason about when this extra workmay be unnecessary. We contribute the design of Wasm-prechk, as well as areference implementation, and prove that Wasm-prechk is in fact as safe asWebAssembly.ivPrefaceThis dissertation is original, unpublished, independent work by the author,Adam T. Geller, except for Chapter 4 and Appendix B. The subject reductionproof in Chapter 4 and Appendix B, and formulation of administrative typingrules in Chapter 4 was joint work between Adam. T. Geller and Justin Frank.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixAcknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . xDedications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xii1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11.1 Unsafe Code . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11.2 Type Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 21.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.5 Thesis Statement . . . . . . . . . . . . . . . . . . . . . . . . . 52 Background: Wasm . . . . . . . . . . . . . . . . . . . . . . . . 62.1 Wasm Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 62.2 Wasm Dynamic Semantics . . . . . . . . . . . . . . . . . . . . 92.2.1 The Wasm Reduction Relation . . . . . . . . . . . . . 112.3 The Wasm Type System . . . . . . . . . . . . . . . . . . . . . 18vi2.3.1 Stack Polymorphism . . . . . . . . . . . . . . . . . . . 213 Wasm-prechk . . . . . . . . . . . . . . . . . . . . . . . . . . . 223.1 Wasm-prechk Syntax . . . . . . . . . . . . . . . . . . . . . . . 233.1.1 The Wasm-prechk Index Language . . . . . . . . . . . 243.2 Wasm-prechk Dynamic Semantics . . . . . . . . . . . . . . . . 273.3 The Wasm-prechk Indexed Type System . . . . . . . . . . . . 293.3.1 Subtyping, Implication, and Constraint Satisfaction . 373.3.2 Using Types for Check Elimination . . . . . . . . . . . 383.3.3 Module Types . . . . . . . . . . . . . . . . . . . . . . 434 Metatheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464.1 Administrative Typing Rules . . . . . . . . . . . . . . . . . . 464.2 Relationship Between Wasm and Wasm-prechk . . . . . . . . 504.2.1 Embedding Wasm in Wasm-prechk . . . . . . . . . . . 504.2.2 Erasing Wasm-prechk to Wasm . . . . . . . . . . . . . 544.3 Type Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . 684.3.1 Subject Reduction . . . . . . . . . . . . . . . . . . . . 684.3.2 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . 815 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . 885.1 Reference Implementation . . . . . . . . . . . . . . . . . . . . 885.2 Constraint Solving in Practice . . . . . . . . . . . . . . . . . . 895.2.1 Translation of Constraints to Z3 . . . . . . . . . . . . 895.2.2 Impact of Using Z3 . . . . . . . . . . . . . . . . . . . . 926 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 946.1 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 956.2 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 967 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98A Complete Wasm-prechk Typing Judgment Definition . . . 100viiB Metatheory Proofs . . . . . . . . . . . . . . . . . . . . . . . . 105B.1 Sound Erasure Proofs . . . . . . . . . . . . . . . . . . . . . . 105B.2 Subject Reduction Lemmas and Proofs . . . . . . . . . . . . . 112viiiList of FiguresFigure 2.1 Wasm Types . . . . . . . . . . . . . . . . . . . . . . . . . 7Figure 2.2 Wasm Instructions . . . . . . . . . . . . . . . . . . . . . . 8Figure 2.3 Wasm Module Definitions . . . . . . . . . . . . . . . . . . 9Figure 2.4 Wasm Administrative Instructions and Run-Time Structures 10Figure 2.5 Branching Examples . . . . . . . . . . . . . . . . . . . . . 15Figure 3.1 An Example of an Unnecessary Wasm check . . . . . . . . 22Figure 3.2 Wasm-prechk syntax including the four prechk-taggedinstructions . . . . . . . . . . . . . . . . . . . . . . . . . . 24Figure 3.3 Syntax of the Wasm-prechk index type language . . . . . 25Figure 3.4 Wasm-prechk indexed function types . . . . . . . . . . . . 25Figure 3.5 Wasm instructions that have preconditions for reduction . 27Figure 3.6 Behavior of new prechk-tagged instructions . . . . . . . . 28Figure 3.7 An Example of Using a Wasm-prechk prechk-tagged In-struction . . . . . . . . . . . . . . . . . . . . . . . . . . . 29Figure 3.8 Indexed Module Typing Rules . . . . . . . . . . . . . . . . 45Figure 4.1 Wasm-prechk Program Typing Rules . . . . . . . . . . . . 47Figure 4.2 Wasm-prechk Store Typing Rules . . . . . . . . . . . . . . 49Figure 4.3 Wasm-prechk Administrative Instruction Rules . . . . . . 50Figure 5.1 Translation of Wasm-prechk Index Language to Z3 . . . . 90Figure 5.2 Example of a Z3 query for constraint satisfaction . . . . . 91ixAcknowledgementsThis section proceeds through my life in reverse chronological order.University of British ColumbiaFirst and foremost I would like to thank my wonderful advisors, who madethis whole process much easier and significantly contributed to my edification.• William Bowman - Despite being a new professor, William has been awonderful advisor and provided a large amount of guidance when I wasstruggling. William has been a fantastic resource for all of the workhere.• Ivan Beschastnikh - Ivan helped me navigate through the system whenI was a wide-eyed first-year and learn from various mistakes I madealong the way. Ivan was a great source of wisdom and gave me thefreedom to pursue the topics I found most interesting.I would also like to thank various professors for providing guidance andadvice, some of whom are listed below.• Ron Garcia - Ron is definitely one of the nicest people I have met andhas forgotten way more about PL than I have ever learned. He alsoprovided great feedback on this thesis (part of which led to much clearerdefinitions).• Alex Summers - Alex spent time to give me helpful feedback that greatlyimproved this thesis.x• Margo Seltzer - Margo is a kickass professor who is intelligent and caresa lot about students.• Alan Hu - Alan has provided me with many nuggets of wisdom.Thank you to Justin Frank, for helping to prove type safety and developthe reference implementation.Finally, all of my fellow graduate students and lab mates who have becomemy friends and helped me in various ways. There are way too many awesomepeople to thank them all, but I include some notable names below.• Anny Gakhokidze, Puneet Mehrotra, Nico Ritschel, Chris Chen, FelipeBañados Schwerter, Paulette Koronkevich, Aarti Kashyap, ClementFung, Vaastav Anand, and countless others.My ParentsLast but certainly not least, I’d like to thank my awesome parents foreverything they have done and continue to do for me. I’m not sure one couldask for better parents than I have been given (even if I did not ask for them).They have both always been there for me, especially my mom who spent ahuge amount of effort and time taking care of every issue that came up inmy early years, as well as homeschooling me. My Dad has always been myrole model and is the smartest person I know. He tried to introduce me toset theory when I was around 4 and calculus when I was about 13 (the firstone stuck pretty well, the second one not so much).xiDedicationsThis is dedicated to Tabby, Koko, and Socrates. These have been my best(feline) friends who have always helped me maintain my mental health.xiiChapter 1Introduction1.1 Unsafe CodeBrowsers and the Internet-of-Things (IoT) require running untrusted code(i.e., unknown code from an unknown source that could do anything), thatmay have been downloaded from anywhere. It is crucial to ensure the safety ofthe code being executed in these contexts. Otherwise, one website may crashyour entire browser/IoT device, read secret data in your browser/IoT device,or attempt to take over control browser/IoT device. Many such exploitshave originated due to unsafe code being downloaded and run. Typically,sandboxing and/or dynamic safety checks are used to ensure the safety ofuntrusted code.Sandboxing involves placing untrusted code into a secure environmentto contain the damage caused by unsafe behavior [3]. For example, GoogleChrome places the running scripts for each website in separate processes sothat unsafe code cannot access the address space of other websites or thebrowser [7]. This prevents websites from crashing, stealing data, or takingcontrol of other websites and the browser. However, sandboxing in this wayrequires more run time resources than running scripts in one process, asprocesses require overhead in most OSes.Dynamic safety checks are run time checks that catch any attemptedunsafe operations. For example, WebAssembly (Wasm) is a low-level language1designed to be both safe and fast to execute in place of JavaScript forperformance-critical applications in browsers. While Wasm is type safe,memory safe, and its semantics enforce the separation of control flow and data(which together work like sandboxing to, e.g., prevent websites from crashingeach other), it still relies on dynamic checks to ensure these properties at runtime. These dynamic checks potentially slow down programs by introducingunnecessary instructions to perform the checks.We have designed an extension to Wasm, called Wasm-prechk, that addsnew instructions that do not require dynamic safety checks. However, underthe existing Wasm model the new Wasm-prechk instructions have potentiallyunsafe semantics, as they require stronger static guarantees than Wasm canprovide to ensure the same level of safety as Wasm. These instructions arelikely to be faster than their Wasm counterparts because they do not requirethe addition of instructions by the compiler/interpreter to perform checks.To provide these additional static guarantees, we equip Wasm-prechk with amore advanced type system than Wasm.1.2 Type SystemsTypes systems are useful for reasoning about programs. They can be usedto reason about the behavior of programs, usually in the form of safetyguarantees. For example, type safety is the property that a well-typedprogram will never become stuck ; that is, an expression will always be a well-formed irreducible value, reduce to an error, or reduce to another well-formedexpression. The safety guarantees of type systems provide a degree of trustin programs, as a well-typed program implicitly contains a checkable proofthat it will only exhibit well-defined behavior (which, in the case of Wasm,has several safety guarantees as discussed above).Generally, low-level languages are either untyped or have simple typesystems that provide minimal guarantees. More expressive type systemscan encode richer invariants, enabling ruling out more bad behaviors withstatic checks alone. Generally, such type systems are attached to high-levellanguages, where explicit abstractions make it easier to reason about programs2compared to low-level languages. Conversely, using expressive type systemsin low-level languages often requires reasoning about program state andunstructured control flow (e.g., goto), which introduces more complexity intothe type system. However, prior work has attached expressive type systemsthat permit rich correctness guarantees to simple low-level languages.1.3 Related WorkUsing type information to improve compiler optimizations is not a new idea.Tarditi et al. [8] used strongly typed intermediate languages (TIL) to improveoptimizations of SML code. Compiling SML involves many translationsamong intermediate languages, and by preserving type information acrossthose translations Tarditi et al. [8] were able to safely perform additionalcompiler operations. Using TIL in the compilation of programs led to up to50% faster programs. TIL focuses on compiler optimizations and eventuallytranslates into untyped languages and finally runnable assembly, so theensured guarantees of the type system are lost along the way (they may stillbe present, but it is no longer possible to statically check them).Proof-carrying code (PCC) was introduced by Necula [6]. PCC attachedexplicit proofs that low-level code satisfies some safety properties. The proofcan then be checked to ensure the safety of the code before it is run. Whiletyped intermediate languages require types to be considered as part of thelanguage, PCC adds a separate logical framework on top. Thus, PCC can beused with any language, and requires no support from the language. However,because PCC has no support from the language, it has a higher proof burdenthan using types inside a language.Necula [6] provides a detailed example of invariants for extensions to TILto ensure type safety of compiled code. The example uses the EdinburghLogical Framework (LF) to encode the proof. A type safety proof of aLF program is a proof of correctness (with respect to some specification).Encoded proofs may be quite large, requiring extra time to transmit andcheck compared to type annotations and typechecking.Morrisett et al. [5] showed how types could provably be preserved during3five different compilation passes to get from System F all the way down to atyped assembly language (TAL). The purpose of TAL was focused on safety.Although Morrisett et al. [5] argued that the type-preserving compilationpasses would permit similar optimizations to TIL, they didn’t include furtheroptimizations based on TAL. However, Morrisett et al. [5] did argue thatthe guarantees of TAL were sufficient to allow untrusted code to be safelyexecuted.Xi and Harper [9] created a much more expressive type system for anassembly language which had the potential to allow more compiler optimiza-tions. Their language, a dependently typed assembly language (DTAL), useda limited dependent type system, which enabled safely removing some runtime checks, including array bounds checks. The goal of DTAL, similar toTAL, was to support type-preserving compilation from a high-level languagefor both optimizations and safety. DTAL intended to support type-preservingcompilation from Dependent ML as well as SML.After almost two decades of JavaScript being the dominant language inbrowsers, it was decided that an alternative was necessary for performance-critical code. The alternative that was jointly created by the major browserdevelopers was WebAssembly (Wasm) [4]. Wasm is a stack-based assemblylanguage with structured control flow. It is designed to be safe as well asperformant, with a small binary footprint. The Wasm type system is simple,only encoding primitive types, but strong enough to ensure certain safetyproperties (i.e., that arbitrary code cannot be executed). Memory safety inWasm is enforced using run time checks. Wasm is supported by most majorbrowsers, and can work well for IoT devices due to its portability and safety.1.4 ContributionsWe want to use types to improve performance while ensuring safety in real-world low-level programs. While prior work has used expressive type systemsfor low-level languages, we want to show the feasibility of doing this with alanguage commonly used in contexts that are both performance-critical anduntrusted. Towards that goal, we introduce Wasm-prechk, an extension of4the WebAssembly (Wasm) language.We chose Wasm to build on because it is used in browsers and IoT devices.Both browsers and IoT device require strong safety guarantees (such aspreventing programs from crashing the whole browser/IoT device) since theydownload and execute code from unknown sources. Further, the use case forWasm is often performance-critical applications such as in-browser gamesand cryptographic algorithms.Wasm-prechk introduces new versions of Wasm instructions which requireno dynamic checks, but also require stronger type-level safety guaranteesthan their Wasm counterparts (section 3.2). To facilitate type-checking thesenew instructions, Wasm-prechk uses an indexed type system which is able toencode linear constraints on program variables and therefore ensure safetyproperties of the new Wasm-prechk instructions (section 3.3). We ensurethat Wasm-prechk is as safe as Wasm by providing a type safety proof of theWasm-prechk indexed type system (section 4.3). Together, these additionsmean that Wasm-prechk is as safe as Wasm while potentially improvingperformance by moving run-time checks to compile time.We show that Wasm-prechk is backwards compatible with Wasm byshowing that Wasm programs can be turned into Wasm-prechk programs(subsection 4.2.1). This means that there is no additional proof burden onthe programmer to use Wasm-prechk. We also show that we can go theother way by turning Wasm-prechk programs into well-typed Wasm programs(subsection 4.2.2).1.5 Thesis StatementAn indexed type system can be used in an existing low-levellanguage to reduce the number of dynamic checks required, with-out sacrificing safety and security guarantees or increasing theprogrammer’s proof burden.5Chapter 2Background: WasmHere we present an overview of Wasm so readers have some familiaritywith it for when we present Wasm-prechk. We do not cover the entirety ofthe Wasm language as presented in the 2017 paper [4], but rather presentselected important facets of the syntax, semantics, and type system. It isrecommended that the reader first skim this chapter to understand the basicsand then refer back while reading chapter 3 and chapter 4.2.1 Wasm SyntaxFigure 2.1 shows the types of Wasm. Primitive Wasm types, representedas t, include 32- and 64-bit floats and integers. Packed types, tp, include8-, 16-, and 32- bit integers, are used in memory operations to load/store asmaller payload (e.g., i8 loads/stores just one byte). Wasm is a stack-basedlanguage, so the type of an instruction in Wasm consists of a preconditionand postcondition on the shape of the stack, which is what a Wasm functiontype tf is encoding. This can be viewed as though instructions consumecertain values from the stack and then produce values to be pushed on thestack. Thus, function types, tf , are just syntax used in certain instructions,function declarations, and the Wasm typing judgment, not function types inthe traditional sense. Lastly, global types consist of a primitive type t andan optional mutable flag (the ? form is explained more below).6t ::= i32 | i64 | f32 | f64tp ::= i8 | i16 | i32tf ::= t∗ → t∗tg ::= mut? tFigure 2.1: Wasm TypesThe Wasm syntax uses the Kleene star within its BNF (e.g., t∗) to denotepossibly empty sequences. For example, t∗ matches  (the empty sequence,which is an empty sequence of anything), i32 i32, and i32 i64 i32. Instructions,represented by the metavariable e, are usually grouped into sequences e∗which are possibly empty . As a further point on metavariables, e1 ande2, both instruction metavariables, may happen to be the same instruction,or not, we do not know. Similarly, e∗1 and e∗2 refer to different sequencemetavariables that may or may not be the same; we can make no assumptionsabout them.We can use different annotations in place of the Kleene star to addadditional information. The Kleene star may be replaced with an exact valuen when we know that the sequence has length n (e.g., a sequence of 3 types bephrased as t3). We can also use a question mark to represent either an emptysequence (), or a sequence with exactly one item (e.g., v? = v′ ∨ v? = ).There is no requirement that a sequence of non-terminals, e∗1, be made upof entirely the same pattern, unless it is explicitly written out as in (t.const c)∗.For example, e∗1 matches (t.const c1) (t.const c2) (t.binop). Further, we mayseparate out subsequences: from (t.const c)∗ we may separate out t∗ and c∗to refer to the sequences of types and constant values respectively.With this notation in mind, we can now look over the Wasm instructionsin Figure 2.2 (we will discuss the instructions in section 2.2). Syntax writtenin a blue sans serif font denotes a keyword, while text written in italicsrepresents a metavariable. Throughout the Wasm syntax there are manymetavariables used to represent natural numbers: n and m are usually usedfor the table and memory sizes, i and j are often used as indexes (e.g., toreference a local variable), o and align are used within memory operations(we replace a with align for clarity and since we use a elsewhere), and lastly7unopiN ::= clz | ctz | popcnttestopiN ::= eqzbinopiN ::= add | sub | shl | or | ...relopiN ::= eq | ne | gt | ge | ...cvtop ::= convert | reinterprete ::= unreachable | nop | drop | select |block tf e∗ end | loop tf e∗ end | if tf e∗ else e∗ end |br i | br if i | br table i+ | return | call i | call indirect tf |get local i | set local i | tee local i | get global i |set global i | t.load (tp_sx)? align o | t.store tp? align o |current memory | grow memory | t.const c |t.unopt | t.binopt | t.testopt | t.relopt | t.cvtop t_sx? | ...Figure 2.2: Wasm Instructionsc is used as a constant metavariable (which could also be a float). iN is usedto annotate operations that support integers, and fN is used to annotateoperations that support floats.Some instructions, such as loop tf e∗ end include a sequence of instructionse∗. We refer to such instructions as block instructions, since they definecontrol flow blocks for the instructions inside (not to be confused with theblock instruction, which is a block instruction). In a block instruction, youwill see one or more instruction sequences e∗ as part of the syntax before end,we refer to this as the body. Further, many block instructions also include anexplicit type annotation tf declaring their precondition and postcondition.Wasm has modules that include functions (f), global variables (glob), anoptional function table (tab), and an optional linear memory chunk (mem),as seen in Figure 2.3. Functions, globals, the table, and memory can beimported, using import ”name1” ”name2”, which imports name2 from thefile name1. Similarly, they can also be exported under any number of namesusing export ”name”.Functions include a list of local variable declarations to use within thebody (a sequence of instructions). Additionally, function arguments areaccessible as local variables within the body of functions. Global variablesmay be mutable (although, exported global variables, which are accessible in8(imports) im ::= import ”name” ”name”(exports) ex ::= export ”name”(functions) f ::= ex ∗ func tf local t∗ e∗ | ex ∗ func tf im(globals) glob ::= ex∗ global tg e∗ | ex∗ global tg im(table) tab ::= ex∗ table n i∗ | ex ∗ table n im(memory) mem ::= ex∗ memory n | ex ∗ memory n im(modules) module ::= module f∗ glob∗ tab? mem?Figure 2.3: Wasm Module Definitionsother modules, cannot be mutable, as we will see later), and are initializedvia a sequence of instructions. Function tables store references to functionsthat can be called using indirect function calls; they are used to more safelyrepresent function pointers. Indirect function calls take an index and use itto lookup a function in the function table and call it. They must supply afunction type annotation, tf that gets checked against the function that endsup being called at run-time. Linear memory, mem, is a continuous chunkof memory. Memory load and store operations operate within the linearmemory chunk.2.2 Wasm Dynamic SemanticsWasm is a stack-based assembly language specified using reduction semantics1. Before we introduce the Wasm semantics, we first must introduce someadministrative structures and instructions that are used in the reductionrelation to keep track of information. Administrative instructions are notpart of the surface syntax of a language (e.g., you cannot put a local blockin a Wasm-prechk program), and can only appear as an intermediate termduring reduction. Figure 2.4 shows the new administrative instructions andrun-time structures.The runtime store, s, includes runtime instances for every module (inst∗),as well as all of the tables (tabinst∗), and memory chunks (meminst∗). In1For those unfamiliar with reduction semantics, I highly recommended these notes byRon Garcia: https://www.cs.ubc.ca/~rxg/cpsc509/05-reduction.pdf9(closures) cl ::= {inst i, func f}(bytes) b ::= 0x00, 0x01, ..., 0xff(table instances) tabinst ::= cl∗(memory instances) meminst ::= b∗(modules instances) inst ::= {func cl∗, glob v∗, tab i?,mem i?}(stores) s ::= {inst inst∗, tab tabinst∗,mem meminst∗}(values) v ::= t.const c(admin. instrs.) e ::= ... | trap | call cl | labeln{e∗} e∗ end |localn{i; v∗} e∗ end(reduction contexts) L0 ::= v∗  e∗Lk+1 ::= v∗ labeln{e∗} Lk end e∗Figure 2.4: Wasm Administrative Instructions and Run-Time Structuresother words, s includes an instantiation of every module. Module instances,inst, represent Wasm modules after linking. They refer to their table andmemory (if they have either), by indexing into the list of runtime instances oftables and memory chunks in the store s. A table instance tabinst containsa list of closures that can be called. b represents a byte. A memory instancememinst is a sequence of bytes representing a contiguous memory chunk.Wasm closures, cl, intuitively represents a function closed under linking.Closures include the module instance that the function is defined in, as wellas the function definition (which cannot be an import) with any exportserased.There are a few final notational digressions we must make before describingthe reduction relation. Firstly, objects such as s = {inst inst∗, . . .} can bedereferenced using their keywords (e.g., “inst”). For example, sinst = inst∗given the above definition of s. Secondly, we can index into a sequence toget a specific element (e.g., inst∗(i) returns the ith inst in inst∗). Lastly,Wasm uses several shorthands to get information out of module instances in s:sfunc(i, j) = sinst(i)func(j). Essentially, this allows us to implicitly dereferencethe ith module instance to get the jth function inside of the instance. Thisshorthand is used similarly for glob, tab, and mem.Constant instructions t.const c represent values, and are denoted by the10metavariable v, when they should be interpreted that way. They produce aconstant value (known statically). This leads to a particular representationof the stack, as discussed in subsection 2.2.1. A trap (trap) is the Wasm termfor a run-time error. call cl is a function call on a closure. As we will see, itis an intermediate step for performing both direct and indirect function calls.Two types of block instructions are introduced. The first, the labelblock, is used in handling control flow. Specifically, they are used to handlebranching. All block instructions (block, loop, and if) reduce to label blocks.Label blocks can store instructions (e∗ inside the curly braces), and theannotation n is equal to the expected number of inputs to those instructions.This is explained more when we describe how branching works.The second block instruction is the local block. A local is the result ofreducing a closure call; it is used to reduce a function body within the closedenvironment of the closure. They introduce an environment consisting of themodule instance and local variables inside which their body is reduced.Finally, we introduce reduction contexts, Lk, where k is the nesting depth.Reduction contexts are defined using label blocks, so Lk contains k nestedlabel blocks. As well as nested label blocks, reduction contexts containpreceding values v∗ (i.e., a stack), and proceeding instructions e∗ that arenext to be executed after the nested label block finishes reducing.2.2.1 The Wasm Reduction RelationThe Wasm Reduction Relation works on configurations that include thestore s, local variables (represented as a sequence of values v∗), and theinstruction sequence e∗. Reduction is relative the the current module index i,which is used to know which module instance in the store to look at whendereferencing the store. The store, local variables, and module index areomitted when not used. We present all the reduction rules below.s; v∗; e∗ ↪→i s′; v′∗; e′∗Instructions are reduced in place by decomposing the program using11reduction contexts. Intuitively, we pull out the next instruction to execute,reduce it, and push the result on top of the stack. The “stack” is just thesequence of values (i.e., constant instructions) preceding the first reducibleinstruction. When an instruction reduces to a value, that value becomesthe new top of the stack and the next instruction is reduced. This methodof decomposing ensures that all of the instructions preceding the instructioncurrently being reduced have already been reduced to values.Binary and relation operations consume two values from the stack andeither push back onto the stack the specified operation applied to thosevalues, or trap if the operation on the values is not defined (in the caseof dividing by zero). Test operators only consume one value, and do nottrap, but are otherwise similar. The reduction rules for these operatorsuse metafunctions (e.g., testopt(c)) to compute the result of applying theoperator for the produced value.The instruction unreachable causes a trap (it is similar to e.g., assertfalse), nop reduces to the empty sequence, and drop consumes one valueand reduces to the empty sequence (i.e., it discards the value on top of thestack). select is a ternary operator (like ? : in C) that consumes three valuesand produces either the first or the second depending on the third value.The true/non-zero case of select returns the first value consumed (k + 1 is acommon shorthand for a non-zero value), and the false/zero case returns thesecond value consumed.12(t.const c1) (t.const c2) t.binop ↪→ t.const cif c = binop(c1, c2)(t.const c1) (t.const c2) t.binop ↪→ trapotherwise(t.const c1) (t.const c2) t.relop ↪→ t.const relop(c1, c2)(t.const c) t.testop ↪→ i32.testopt(c)unreachable ↪→ trapnop ↪→ v drop ↪→ v1 v2 (i32.const 0) select ↪→ v2v1 v2 (i32.const k + 1) select ↪→ v1Block instructions define a control flow environment used by branchinginstructions inside which their bodies are reduced. The true case of an ifblock reduces to the first body inside of a block; the false case does thesame but with the second body. Both block and loop reduces to label blocks.Stored instructions are only added when reducing a loop, in which case itstores the loop code so it can run the loop again. If the body of a labelblock is a trap or a sequence of values then the trap/values replace the block.Since decomposition happens on label blocks, we have included the inductivereduction rule, which intuitively pulls instructions out of the context, reducesthem outside the context, and then plugs them back in.13s; v∗; e∗ ↪→ s′; v′∗; e′∗s; v∗; Lk[e∗] ↪→ s′; v′∗; Lk[e′∗]L0[trap] ↪→ trapvn block (tn1 → tm2 ) e∗ end ↪→ labelm{}vn e∗ endvn loop (tn1 → tm2 ) e∗ end ↪→ labeln{loop (tn1 → tm2 ) e∗end}vn e∗end(i32.const 0) if tf e∗1 else e∗2 end ↪→ block tf e∗2 end(i32.const k + 1) if tf e∗1 else e∗2 end ↪→ block tf e∗1 endlabeln {e∗0} v∗ end ↪→ v∗labeln {e∗0} trap end ↪→ trapBranching (br j) intuitively jumps to the j + 1th outer control flow block(i.e., a label block). More concretely, a br j inside a label block (which, youmay recall, are used as control flow blocks) jumps to the surrounding labelblock with nesting depth j + 1 (essentially peeling back j layers). Afterbranching, execution continues with the values vn consumed by the br andthe stored instructions e∗0 of the j + 1th outer label block (this is in placeto support loops, as jumping to the label block introduced by loop is whatcauses the next iteration to be performed). Extra stack values beyond thoseconsumed are discarded. Figure 2.5 has several examples of branching inaction.Wasm also has a conditional branch instruction. This instruction, br if j,consumes a value and reduces to br j if the value is non-zero, otherwise itreduces to the empty sequence. Table branches, br table , has a list of oneor more numbers, i+ that may be used for a branch. It consumes a i32 kand reduces to br with the kth number, or the last number if there is no kthnumber.14label0{loop . . . end} br 0 end↪→ loop . . . endlabel0{}label0{loop . . . end} br 1 endend↪→ label0{}label0{}label0{} br 1 endendend↪→ label0{} endFigure 2.5: Branching Exampleslabeln {e∗0} Lj [vn br j] end ↪→ vn e∗0(i32.const 0) br if j ↪→ (i32.const k + 1) br if j ↪→ br j(i32.const k) br table jk1 j j∗2 ↪→ br j(i32.const k + n) br table jk1 j ↪→ br jDirect and indirect function calls are expanded in two steps. First, theassociated closure is fetched either from the current module instance (fordirect calls) or from the table (for indirect calls, which traps if the type ofthe fetched closure doesn’t match the expected type). This step reduces adirect or indirect call to a call cl. Then, the closure body is placed into alocal block with the arguments from the stack and locals declared by thefunction (tk), which are zero-initialized, being used as the local variables.15s; call j ↪→i call sfunc(i, j)s; call indirect j ↪→i stab(i, j)if stab(i, j)code = (func tf local t∗ e∗)s; call indirect j ↪→i trapotherwisevn (call cl) ↪→i localm{clinst;vn (t.const 0)k}block (→ tm2 ) e∗endendwhere clfunc = (func tf local t∗ e∗)The local block has the same module index, i, as the closure, so the bodyof the local block is reduced within the module that the closure is definedin and thus uses the global variables, table, and memory of that moduleinstance. This is handled by the inductive reduction rule (which has muchmore of a structural operational small-step semantics flavor). In general,return can be thought of as br k, where k is the context depth. A label blockis added inside of the local block when expanded a function call, so at thetop level of a function br 0 is essentially equivalent to return, except withan additional reduction step. Returning, somewhat similarly to branching,replaces the local block with the arguments to the return instruction, exceptthat it skips over any label blocks. If the body of a local block is a trap orsequence of values equal to the number annotation on the local block, thenthat is what the local block reduces to, similar to branching (also similar tobranching, any extra values on the stack are discarded).16s; v∗; e∗ ↪→i s′; v′∗; e′∗s; v∗0; localn{i; v∗}e∗ end ↪→j s′; v∗0; localn{i; v′∗}e′∗ endlocaln{i; v∗l }vn ↪→ vnlocaln{i; v∗l }trap ↪→ traplocaln{i; v∗l }Lk[vnreturn] ↪→ vnLocal variables are represented as a list of values at run time. They areget/set by indexing into them, like everything else in Wasm. The same istrue of global variables, except there is an extra step since they are stored inthe current module instance inside the store s.vj1 v v2; get local j ↪→ vvj1 v v2; v′ (set local j) ↪→ vj1 v′ v2; vj1 v v2; v′ (tee local j) ↪→ vj1 v′ v2; v′s; get global j ↪→i sglob(i, j)s; v; (set global j) ↪→i s′; where s′ = s with glob(i, j) = v′Finally, there are the memory instructions. One can load or store a valuefrom or to memory, get the current memory size, or try to grow the memory.|t| is used to represent the size of the type (e.g., |i64| = 8 bytes). We omit tworules, one each for store and load, that include the ability to use packed typesto load/store smaller values and to load signed/unsigned. There is a lot ofminutiae detail, but none of it is particularly important. For example, tp is anoptional packed type which allows storing values smaller than the normal sizeof the type of the value (e.g., storing eight bits i8 of a thirtytwo bit integeri32). Loading from memory can optionally be signed or unsigned using sx,which represented signed or unsigned. The “alignment exponent” align isa mysterious variable that is not used during reduction, and is only usedduring typechecking without any explanation. Two metafunctions, constt17and bitst, are used to convert bits to values and vice versa. The key highlevel takeaway is that load and store will trap if the supplied index k plusthe static offset o is out of bounds.s; (i32.const k)(t.load tp_sx align o) ↪→i s; (t.const constt(b∗))if smem(i, k + o, |t|) = b∗s; (i32.const k)(t.load tp_sx align o) ↪→i trapotherwises; (i32.const k) (t.const c)(t.store tp_sx align o) ↪→i s′; if s′ = s with mem(i, k + o, |t|) = bitst(c)s; (i32.const k) (t.const c)(t.store tp_sx align o) ↪→i trapotherwises; current memory ↪→i i32.const |smem(i, ∗)|/64Kis; (i32.const k)grow memory ↪→i s′; i32.const |s′mem(i, ∗)|/64Kiif s′ = s with mem(i, ∗) = smem(i, ∗)(0)k∗64Kis; (i32.const k)grow memory ↪→i i32.const (−1)otherwise2.3 The Wasm Type SystemInstructions in Wasm are typed under a module type context C. C keepstrack of various module-level types: functions, globals, the table, memory,locals, the label stack (i.e., the expected types for branching instructions),and the return stack (i.e., the expected type of the return instruction).18C ::= {func tf∗, global tg∗, table n?, memory m?,local t∗, label (t∗)∗, return (t∗)?}Here is an example of a Wasm typing rule, a binary operation of sometype t consumes two values of the given type t on the stack and produces avalue of type t:C ` t.binop : t t→ tThe above example shows what a typical Wasm typing rule looks like.The type associated with the instruction t.binop is a Wasm function type,which is just the precondition (t t on the left of the →) and postcondition (ton the right of the →) on the stack. In the precondition, the top of the stackis the rightmost type (for example, in t1 t2 t3, t3 is the top of the stack),since that represents the value closest to the instruction getting reduced. Theprecondition and postcondition represent the shape of the stack before andafter executing a sequence of instructions. Intuitively, they represent the“state of the world” before and after the instruction sequence is executed:they require the world to be in a certain state, and then transform it intosome other state. Thus, the static Wasm typing judgement is as follows:C ` e∗ : tfIn addition to this typing judgment, Wasm also includes typing judgmentsfor administrative instructions (which require additional type informationabout runtime structures, so the judgment has a different form) and a typingjudgment in the form of the reduction relation for the Wasm type safety proof.Wasm also has typing judgments for modules and module-level declarations.We reproduce and explain a few selected typing rules from Wasm usingthe static typing judgement. Most typing rules are for a single instructionand there are a few rules which can combine rules. The rule for typing ablock, Rule Wasm-Block typechecks the body e∗ under the module typecontext with the postcondition tm2 appended to the label stack. This is yet19another common notational shorthand where x, y means x extended withy. The branch rule, Rule Wasm-Br, accepts any precondition, extendedwith the ith postcondition on the label stack (counting backwards), andreturns to any postcondition. A branch will return the n values before it,so it is ok if there are more values on the stack, as they will be discarded.Execution does not proceed after branching, so the postcondition can beanything. For function calls we lookup the type of the function in the context(Rule Wasm-Call). Recall that local variables are represented by a listof values at runtime. Thus, the typing rule for set local checks that thevalue consumed by set local , which will replace the ith local in the list, hasthe correct type that is given by looking up the type of the ith local in thecontext (Rule Wasm-Set-Local).C ` t.binop : t t→ tWasm-Binoptf = tn1 → tm2 C, label(tm2 ) ` e∗ : tfC ` block tf e∗ end : tfWasm-BlockClabel(i) = tnC ` br i : t∗1 tn → t∗2Wasm-BrCfunc(i) = tfC ` call i : tfWasm-CallClocal(i) = tC ` set local i : t→ Wasm-Set-LocalThe empty instruction sequence has an empty precondition and post-condition (Rule Wasm-Empty). An instruction e2 can be appended toa sequence of instructions e∗1 if the precondition of e2 is the same as thepostcondition of e∗1 (Rule Wasm-Composition). Then, the preconditionof the full sequence e∗1 e2 is the precondition of e∗1 and the postcondition ofe∗1 e2 is the postcondition of e2.20C `  : → Wasm-EmptyC ` e∗1 : t∗1 → t∗2 C ` e2 : t∗2 → t∗3C ` e∗1 e2 : t∗1 → t∗3Wasm-Composition2.3.1 Stack PolymorphismTo compose together the types of many instructions, it is necessary to carryaround extra type information about the rest of the stack while type-checkinginstructions. Stack polymorphism allows extending the precondition andpostcondition with the same data to thread unmodified parts of the stackthrough a list of instructions. Intuitively, this allows you to “forget” the restof the stack and focus only on the part being manipulated by the instructionbeing checked, after which point the “forgotten” part can be re-added.For example, if the stack has the shape i64 i32 i32, then stack polymor-phism allows us to ignore i64 and typecheck i32.binop with i32 i32. Then thestack would look like i32, at which point we add i64 back to the postconditionto get i64 i32 after executing i32.binop.21Chapter 3Wasm-prechkThe goal of Wasm-prechk is to eliminate unnecessary dynamic checks. Toaccomplish this, it must (1) have instructions that do not require dynamicchecks and (2) statically prove that the assumptions of those instructions aremet. Wasm-prechk extends Wasm with new instructions that explicitly donot require dynamic checks, and an indexed type system to reason about thesafety of omitting checks. Intuitively, we are replacing dynamic checks withstatic checks whenever possible.Consider the example of a Wasm program with an unnecessary dynamiccheck in Figure 3.1. The program consists of a block instruction that consumestwo arguments from the stack and produces onto the stack their quotient ifthe second argument is non-zero, and the first argument otherwise. In Wasm,this program would have a dynamic division-by-zero check inserted for theblock (i32 i32→ i32)(tee local 0)(i32.const 1)(get local 0)(select)(i32.div)endFigure 3.1: An Example of an Unnecessary Wasm check22division instruction (i32.div). However, this check would be unnecessary sincethe instructions preceding the division instruction ensures that the secondargument is non-zero. This is guaranteed because the select instruction selectsthe first value (the local) if the local is non-zero, and, otherwise, selects thesecond value (i32.const 1).In the above example, it is possible to check the necessary preconditionof the division instruction (that the second argument is non-zero) statically,rather than dynamically. Wasm-prechk performs such static checks usingan indexed type system. An indexed type language uses an index languagein the type system to encode information within types. Wasm-prechk’sindex language must be capable of capturing enough information about aWasm-prechk program to statically verify the preconditions of prechk-taggedinstructions.The Wasm-prechk index language is designed to encode linear constraintson program values (the details of how they are encoded is discussed insubsection 3.1.1). To do this, we “shadow” Wasm-prechk program valuesusing what we call index variables to track constraints on and relationshipsbetween program values. Many of these constraints/relationships are writtenusing Wasm operators (e.g., binop), since they are the predominant waythat Wasm values end up being related to each other. Index variables areassociated with program values using indexed types, which combine the typeinformation from Wasm: the primitive type t of the value, with the indexedtype variable that represents the value in the index language. Finally, wealso use index variables to track local variables (specifically the current valueof local variables, since they are mutable and may change) via an index localstore.3.1 Wasm-prechk SyntaxThe syntax of Wasm-prechk has the same structure as Wasm, but differentinstructions and richer types. First, Wasm-prechk introduces four additionalinstructions, which are referred to as “prechk-tagged” instructions. Second,Wasm-prechk does not support floating point values or unary operators on23testopiN ::= eqzbinopiN ::= add | sub | shl | or | ...relopiN ::= eq | ne | gt | ge | ...e ::= unreachable | nop | drop | select |block tfi e∗ end | loop tfi e∗ end | if tfi e∗ else e∗ end |br i | br if i | br table i+ | return | call i | call indirect tfi |get local i | set local i | tee local i | get global i |set global i | t.load (tp_sx)? align o | t.store tp? align o |current memory | grow memory | t.const c |t.binopt | t.testopt | t.relopt |t.divprechk | t.call indirectprechk |t.loadprechk (tp_sx)? align o | t.storeprechk tp? align oFigure 3.2: Wasm-prechk syntax including the four prechk-tagged instructionsintegers since they are difficult to reason about (this is explained in moredetail in chapter 5). While it would be possible to support them, we wouldhave no more type information about them than Wasm, and the focus of thiswork is on the type information. Wasm-prechk uses a different representationof types within instructions and functions, as we see in subsection 3.1.1.Recall from section 2.2 that four Wasm instructions require run-timechecks: integer division, indirect function calls, and memory loads and stores.“prechk-tagged” instructions refer to four Wasm-prechk instructions, listed inFigure 3.2, that are counterparts to these four Wasm instructions. Intuitively,we add a tag to the instruction to show that it doesn’t require run-timechecks. Formally, however, different instructions have different semantics andtyping rules, as explained below.3.1.1 The Wasm-prechk Index LanguageWasm-prechk uses an indexed type system. We use the Wasm-prechk indexlanguage to encode constraints on program values within types. Figure 3.3shows the syntax for the index type language. Remember, syntax written ina blue sans serif font denotes a Wasm keyword. Below is a quick overview ofeach metavariable.24t ::= i32 | i64a ::= IndexV ariablex y ::= a | (t c) | (binop x y) | (testop x) | (relop x y)P ::= (= x y) | (if P P P ) | ¬P | P ∧ P | P ∨ Pφ ::= ◦ | φ, (t a) | φ, PFigure 3.3: Syntax of the Wasm-prechk index type languageti ::= (t a)l ::= ti∗tfi ::= ti∗; l; φ→ ti∗; l; φC ::= {func tfi∗, global (mut? t)∗, table n?, memory m?,local t∗, label(ti∗; l; φ)∗, return (ti∗; l; φ)?}Figure 3.4: Wasm-prechk indexed function types• t represents a primitive Wasm type. We do not reason about floatingpoint values, so it is either a 32-bit integer (i32) or a 64-bit integer(i64).• a is a type index variable, which is used to track constraints on programvalues.• x and y are type indices; they can be an index type variable, a constantwith an explicit type, or a Wasm operation on a type index.• P is a proposition about type indices which can encode equality con-straints on type indices, or combine propositions using common first-order logic operators.• φ is the type index context which stores index type variable declarationsand propositions. Essentially, it contains all of the knowledge we haveabout all of the index variables.Indexed types are used to associate index variables a with values in theprogram. Figure 3.4 shows the form of an indexed type, ti, which includesboth the type t and an index variable a. In Wasm-prechk, we represent theshape of the stack as a sequence of indexed types ti∗.25The index local store associates index variables with local variables. It hasan identical form to the stack: a sequence of indexed types to associate indexvariables with local variables. We use the shorthand l to refer to the indexlocal store. The index type context φ is used to reason about the possiblevalues of computations. It stores constraints on and between program valuestracked by indexed types representing the stack and index local store.Wasm-prechk uses indexed “function” types tfi , which, similar to Wasm’sfunction types, are just a precondition and postcondition. However, indexedfunction types include much more information in their precondition andpostcondition! They represent the stack using a sequence of indexed typesand track local variables using the index local store, and include φ whichcontains constraints about those values. We see how this information is usedin subsection 3.3.2.We retain C to refer to the module type context in Wasm-prechk, althoughthe representation of module types is slightly different. Wasm functiontypes are replaced with Wasm-prechk indexed function types. Further, thepostconditions in the label stack and return stack are replaced with Wasm-prechk indexed postconditions including indexed types, the local index store,and the index type context.We can now introduce the Wasm-prechk typing judgement for instructions.It is similar to the Wasm typing judgment, but uses indexed function typeswhich include much more information by tracking constraints about programvalues.C ` e∗ : tfiRecall that certain Wasm instructions (such as block and call indirect )include Wasm function types to declare the expected types of their bodies. InWasm-prechk, we replace those function types with indexed function types.26s; v∗; e∗ → s′; v′∗; e′∗(t.const c1) (t.const c2) t.binop ↪→ t.const cif c = binop(c1, c2)(t.const c1) (t.const c2) t.binop ↪→ trapotherwises; call indirect j ↪→i stab(i, j)if stab(i, j)code = (func tf local t∗ e∗)s; call indirect j ↪→i trapotherwises; (i32.const k)(t.load tp_sx align o) ↪→i s; (t.const constt(b∗))if smem(i, k + o, |t|) = b∗s; (i32.const k)(t.load tp_sx align o) ↪→i trapotherwises; (i32.const k) (t.const c)(t.store tp_sx align o) ↪→i s′; if s′ = s withmem(i, k + o, |t|) = bitst(c)s; (i32.const k) (t.const c)(t.store tp_sx align o) ↪→i trapotherwiseFigure 3.5: Wasm instructions that have preconditions for reduction3.2 Wasm-prechk Dynamic SemanticsWasm-prechk uses the same reduction relation with the same structure asWasm (explained in detail in section 2.2). All the reduction rules for all of theWasm-prechk instructions are the same as they are for Wasm, as presentedin section 2.2, except that indexed function types are used instead of Wasmfunction types. We also have four new instructions, for which we introducenew reduction rules.The formal reason why certain Wasm instructions require run-time checksis because they have preconditions as part of their semantics. If the precondi-tions are not met then those instructions trap to avoid undefined behavior27s; v∗; e∗ → s′; v′∗; e′∗(t.const c1) (t.const c2)t.divprechk ↪→ cwhere c2 6= 0 ∧ c = c1/c2s; (t.const j)t.call indirectprechk tfi ↪→i call stab(i, j)where stab(i, j) =func tfi2 local t∗ e∗and tfi2 <: tfis; (i32.const k)(t.loadprechk (tp_sx)? a o) ↪→i t.const constt(b∗)where smem(i, k + o, |t|) = b∗s; (i32.const k) (t.const c)(t.storeprechk tp? a o) ↪→i s′; where s′ = swith mem(i, k + o, |t|) = bits|t|t (c)Figure 3.6: Behavior of new prechk-tagged instructions(we’ve reproduced the reduction rules for those instructions in Figure 3.5).The Wasm type system is not expressive enough to ensure these precondi-tions statically, so they instead must be checked at run-time. However, theWasm-prechk type system is capable of statically checking these preconditions.In Wasm-prechk, “prechk-tagged” instructions can assume that the pre-conditions on their behavior hold because it is enforced by the Wasm-prechktype system. This can be seen in the reduction rules for the “prechk-tagged”instructions in Figure Figure 3.6, where they do not have rules to trap whentheir preconditions do not hold. For example, in the divprechk rule, the secondargument c2 is guaranteed to be non-zero, so there will be no trap on division-by-zero. call indirectprechk can assume that the function that gets pulled fromthe table tfi2 has a subtype of the expected type tfi , so it is a valid type forthe indirect call (we will go over subtyping in more detail in subsection 3.3.1).The prechk-tagged memory operations loadprechk and storeprechk can assumethat the memory operation takes place inside the memory bounds.28Now, we can rewrite the example from Figure 3.1 to use the prechk-taggeddivision instruction, as seen in Figure 3.7. Remember that we know thesecond argument to divprechk is guaranteed to be non-zero, so we know theassumption of the divprechk instruction (c2 6= 0) holds. Since divprechk does notrequire a dynamic check, this program will presumably be faster than theversion with the dynamic check. We still have not shown how we staticallyensure that this assumption holds, which we will do in subsection 3.3.2.3.3 The Wasm-prechk Indexed Type SystemThe Wasm-prechk type system is designed to provide sufficient informationto safely eliminate dynamic checks (i.e., to ensure that the required precon-ditions are met to prechk-tag an instruction). As explained in 3.1.1, theWasm-prechk type system can encode constraints on program values in thepreconditions and postconditions of instructions. We will now show howthese constraints are added and used.Recall the form of the Wasm-prechk typing judgement for instructions.C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2Under C, the module type context, e∗ has the precondition ti∗1; l1; φ1and postcondition ti∗2; l2; φ2. We sometimes use the metavariable abbrevi-ation tfi ::= ti∗1; l1; φ1 → ti∗2; l2; φ2 as shorthand for the precondition andpostcondition of an instruction.block (i32 i32→ i32)(tee local 0)(i32.const 1)(get local 0)(select)(i32.divprechk)endFigure 3.7: An Example of Using a Wasm-prechk prechk-tagged Instruction29As in Wasm, Wasm-prechk generally has two kinds of typing rules. Mostrules are for inferring or checking the types of instructions (in which case e∗will be a single instruction). There are also a few rules to compose togetherinstruction sequences. We present the typing rules mixed with discussion ofthose rules. The typing judgment definition in its entirety is reproduced inthe appendix Appendix A.Here are some of the simpler rules. These rules don’t use or modifyindex type information. Rule Unreachable accepts any precondition andguarantees any postcondition since it just causes a trap. In Rule Nop, nochanges are made from the precondition to the post condition because theinstruction does nothing. Rule Drop consumes the top value from the stack(without caring about its type) and does not change the local index store orindex type context.C ` unreachable : ti∗1; l1; φ1 → ti∗2; l2; φ2UnreachableC ` nop : ; l; φ→ ; l; φNopC ` drop : (t a); l; φ→ ; l; φDropThe constant instruction is a simple example of how indexed types work.Rule Const adds a new indexed type onto the stack to track the new programvariable (t a), declares the new indexed type in the index type context φ(the (t a) part of φ, (t a), (= a (t c))), and constrains that indexed type tobe equal to the constant in φ (the (= a (t c)) part of φ, (t a), (= a (t c))).We require a to be fresh (i.e., that it is not present in any types in theprogram up to this point), so that we know a is not constrained/referencedanywhere in the precondition. This is a common pattern to see in rules whichintroduce new index variables. Since const does not change or reference thelocal variables, the local index store l is unchanged between the preconditionand postcondition.a is freshC ` t.const c : ; l; φ→ (t a); l; φ, (t a), (= a(t c))Const30There are several different kinds of operations, but they all work similarly.The binary operator instruction adds constraints between new and old pro-gram values, since the result of the instruction is a new program value, whilethe consumed values may already be constrained. A binary operation con-sumes two values from the stack, which have associated indexed types (t a1)and (t a2), and produces a value which is associated with the fresh indexedtype (t a3). The index type declaration (t a3) is added to the index typecontext φ and a3 is constrained to be equal to the binary operator appliedto the index variables that correspond to the input (= a3 (‖binop‖ a1 a2).As a side note, we use ‖binop‖ to indicate that we are moving the binop (orrelop or testop) from Wasm-prechk to the index language, where it will beinterpreted by the semantics of the index language. Binary operators do notaffect or use local variables, so the local index store. l, is the same in theprecondition and postcondition.a3 is freshC ` t.binop : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖binop‖ a1 a2))Binopa3 is freshC ` t.testop : (t a1) l; φ→ (i32 a2); l; φ, (t a2), (= a2 (‖testop‖ a1))Testopa3 is freshC ` t.relop : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖relop‖ a1 a2))RelopRule Select constrains indexed types in a rather complex way. Selectconsumes three values from the stack, it returns the second value if the thirdvalue is zero, and otherwise returns the first value (similar to C’s ternaryoperator). We use the type-level “if” to allow the constraint on the result todepend on the third value consumed: (if (= a (i32 0)) (= a3 a2) (= a3 a1)).31a3 is freshC ` select : (t a1) (t a2) (i32 a); l; φ→ (t a3); l; φ, (t a3),(if (= a (i32 0)) (= a3 a2) (= a3 a1))SelectThe rules for the three different kinds of blocks (block, loop, and if) aresimilar to Wasm. They simply ensure that the interior instruction sequencehas the expected type under the context with the expected postcondition(or precondition in the case of loop) appended to the local stack. In Wasm-prechk, if blocks make extra assumptions about the consumed value inthe subsequences (that it is non-zero in the first sequence and zero in thesecond), because those constraints must be true for that sequence to beexecuted. While if and block append their postcondition to the label stackfor typechecking branching instructions within the block, loop appends itsprecondition because branching to a loop means running the loop again.C2, label (ti∗2; l2; φ2) ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` block (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2BlockC2, label (ti∗1; l1; φ1)∗ ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` loop (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2LoopC2, label (ti∗2; l2; φ2) ` e∗1 : ti∗1; l1; φ1,¬(= a (i32 0))→ ti∗2; l2; φ2C2, label (ti∗2; l2; φ2) ` e∗2 : ti∗1; l1; φ1, (= a (i32 0)))→ ti∗2; l2; φ2C ` if (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗1 else e∗2 end : ti∗1; l1; φ1 → ti∗2; l2; φ2IfOne thing to note is that all three of these rules include their expectedpreconditions and postconditions as part of their syntax. We consider theindex variables in these indexed function types to be unification variablesrather than literals, allowing them to match any literal as long as the typesunify. Intuitively, this is very similar to alpha equivalence, where the precon-32dition matches any preceding postcondition with the same structure as longas the variable can be renamed to match. The postcondition appended tothe label stack also has unification variables instead of the supplied literals.The rules for branching instructions and return are similar to Wasm.However, br if adds the assumption that the consumed value is zero to itspostcondition. This assumption can be safely added because the value mustbe zero for execution to continue without a branch occurring. If the consumedvalue is constrained to be non-zero in the indexed type system, then this willcause a contradiction in the constraints of the index type context φ. However,that is fine since this means that no instructions following the br if will beexecuted. Also remember the above note that the postconditions on the labelstack contain unification variables, not literals.Recall from section 2.2 that br table branches to one of many differentlabels. Thus, we must ensure that every possible branching postcondition towhich it might branch is implied by the precondition.Clabel(i) = ti∗; l1; φ1C ` br i : ti∗1 ti∗; l1; φ1 → ti∗2; l2; φ2BrCreturn = ti∗; l1; φ1C ` return : ti∗1 ti∗; l1; φ1 → ti∗2; l2; φ2ReturnClabel(i) = ti∗; l1; φ1,¬(= a (i32 0))C ` br if i : ti∗ a; l1; φ1 → ti∗; l1; φ1, (= a (i32 0))Br-If(Clabel(i) = ti∗; l1; φi)+ (φ1 =⇒ φi)nC ` br table i+ : ti∗1 ti∗ a; l1; φ1 → ti∗2; l2; φ2Br-TableRecall that functions are declared within the module with a specificindexed function type tfi , that is a precondition and postcondition. Thesedeclared indexed function types are placed inside the module type contextC. Direct function calls call i have the same type as the declared indexed33function type of the function they are calling with two differences. First,the local index store is unchanged, since the called function will have beenturned into a closure that operates on separate local variables in a localblock. Second, the index type context in the postcondition of the call isextended with the declarations and constraints from the precondition of thecall. The precondition and postcondition of a function can only containconstraints about the arguments supplied to that function, so simply copyingthe postcondition of the function would result in the loss of information aboutall other index variables.Indirect function calls call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2 include theexpected indexed function type ti∗1; l1; φ1 → ti∗2; l2; φ2 provided as part oftheir syntax (the same note about index variables being unification variablesfrom above holds). Remember that indirect function calls perform a runtime typecheck against the closure that they end up calling, so we assumestatically that the check will proceed because if it does not the program willtrap (trap satisfies any tfi , including the one for the indirect call) and notbe able to do any harm. The same two differences described above betweenthe expected indexed function type tfi and the type of the call indirect tfiinstruction also hold.Cfunc(i) = ti∗1; l1; φ1 → ti∗2; l2; φ2C ` call i : ti∗1; l; φ1 → ti∗2; l; φ1, φ2CallCtable(i) = (j, tfi∗2)C ` call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2: ti∗1 (i32 a); l; φ1 → ti∗2; l; φ1, φ2Call-IndirectThe only instructions that actually mutate the local index store are thosethat operate on local variables. get local produces a fresh indexed type (t a2)that is constrained to be equal to the index variable associated with the localbeing retrieved. set local works in the reverse direction, replacing the indexvariable associated with the local being set. Because set local reasons about34local variables, which are not part of the instruction sequence (unlike valueson the stack), we can copy the index variable instead of creating a freshone and constraining it to be equal like for get local Finally, tee local iseffectively a combined set local and get local that consumes and immediatelyregurgitates a value, like the Unix tool “tee”. Thus, the typing rule is similarlya combination of the set local and get local rules, where the indexed typefrom the stack replaces the local variable indexed type, and a fresh indexedtype is produced that is constrained to be equal to the consumed indexvariable.Clocal(i) = t l(i) = (t a) a2 is freshC ` get local i : ; l; φ→ (t a2); l; φ, (t a2), (= a2 a)Get-LocalClocal(i) = t l2 = l1[i := (t a)]C ` set local i : (t a); l1; φ→ ; l2; φSet-LocalClocal(i) = t l2 = l1[i := (t a)] a2 is freshC ` tee local i : (t a); l1; φ→ (t a2); l2; φ, (t a2), (= a2 a)Tee-LocalInstructions for getting and setting globals produce and consume uncon-strained values respectively. Global variables are difficult to reason about inthe type system since they are different between modules. At compile-time,before linking, a module has no information about globals from anothermodule which would be necessary for reasoning about the types of functionsimported from the other module. Therefore, we do not track index variablesfor globals (we just treat them as unconstrained values when they are intro-duced onto the stack by get global ). We do still statically ensure the sameproperties as Wasm: that the value is of the correct Wasm type and in thecase of setting a global variable that the global variable is mutable (has the35mut flag in its type).Cglobal(i) = mut? t a is freshC ` get global i : ; l; φ→ (t a); l; φ, (t a)Get-GlobalCglobal(i) = mut tC ` set global i : (t a); l; φ→ ; l; φSet-GlobalThe typing rules for memory instructions are very similar to Wasm aswe do not reason about the contents of memory or how its size can changethroughout a program. As in Wasm, there are many small details related tohow exactly values are loaded and stored that are not particularly importantto the understanding of the type system, but they are explained with thereduction rules for these values in section 2.2. One thing that does not appearin the Wasm reduction rules but mysteriously appears in the typing ruleswithout much explanation is align. It is checked against the size of the typeof the value being stored/loaded |t| (or optionally |tp|, which should be lessthan |t|) in the premise 2align ≤ (|tp| <)?|t|.Cmemory = n 2align ≤ (|tp| <)?|t| a2 is freshC ` t.load (tp_sx)? align o : (i32 a1); l; φ→ (t a2); l; φ, (t a2)Mem-LoadCmemory = n 2align ≤ (|tp| <)?|t|C ` t.store tp? align o : (i32 a1) (t a2); l; φ→ ; l; φMem-StoreCmemory = n a is freshC ` current memory : ; l; φ→ (i32 a); l; φ, (i32 a)Current-MemoryCmemory = n a2 is freshC ` grow memory : (i32 a1); l; φ→ (i32 a2); l; φ, (i32 a2)Grow-MemoryThe last rules are the ones that can be used to compose sequences of36instructions. The first rule is for the empty instruction sequence , which,similar to Wasm, simply has the same precondition and postcondition ; l; φ.Second, we have Rule Stack-Poly to add stack polymorphism (see subsec-tion 2.3.1). Third, there is a rule to compose a sequence of instructions e∗1with another instruction e2.C `  : ; l; φ→ ; l; φEmptyC ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e∗ : ti∗ ti∗1; l1; φ1 → ti∗ ti∗2; l2; φ2Stack-PolyC ` e∗1 : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e2 : ti∗2; l2; φ2 → ti∗3; l3; φ3C ` e∗1 e2 : ti∗1; l1; φ1 → ti∗3; l3; φ3Composition3.3.1 Subtyping, Implication, and Constraint SatisfactionOne issue with adding the index type context φ to preconditions and postcon-ditions is that the postcondition of one instruction and the precondition of thenext instruction might not match up exactly. For example, one instructionmay ensure a value is greater than ten, but the next just wants the value tobe greater than zero. Intuitively, if a value, “x”, is greater than ten it mustalso be greater than zero, and we want the Wasm-prechk type system to beable to figure this out as well. However, computers as of yet are unable touse intuition, so we must instead formalize this.Our formalization of this problem is to allow strengthening preconditionsand weakening postconditions. Strengthening and weakening is based onimplication ( =⇒ ). We say that φ1 =⇒ φ2 when the following holds: if φ1is satisfied, then φ2 must also be satisfied. If φ1 =⇒ φ2, then we considerφ1 to be stronger than φ2, and φ2 to be weaker than φ1. This solves theaforementioned problem because we can weaken “x is greater than 10” to “xis greater than 0” (or equivalently strengthen “x is greater than 0” to “x isgreater than 10”).37To fit strengthening and weakening into the type system, we define asubtyping judgment based on implication. We essentially parameterize ourtyping judgment with the implication relation. As an aside, we show that thisis a practical thing to do and that such a relation exists by implementing suchan implication relation using Z3 (see subsection 5.2.1). The Rule Impliessays that if an indexed function type tfi1 has a stronger precondition andweaker postcondition than some other indexed function type tfi2, and isotherwise equivalent, then tfi1 is a subtype of tfi2 since it can safely be usedin place of tfi2.φ0 =⇒ φ1 φ2 =⇒ φ3ti∗1; l1; φ1 → ti∗2; l2; φ2 <: ti∗1; l1; φ0 → ti∗2; l2; φ3ImpliesWe then use this in the Wasm-prechk type system by adding a typing rulethat allows the indexed function type for a list of instructions to be replacedby a subtype of that indexed function type.ti∗1; l1; φ1 → ti∗2; l2; φ2 <: ti∗1; l1; φ0 → ti∗2; l2; φ3C ` e∗ → ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e∗ → ti∗1; l1; φ0 → ti∗2; l2; φ3Subtyping3.3.2 Using Types for Check EliminationIn Section 3.2 we explained that prechk-tagged instructions do not needdynamic checks because of the static guarantees of the Wasm-prechk typesystem. Here, we see how the Wasm-prechk type system provides thoseguarantees by looking at the typing rules for each of the prechk-taggedinstructions.Integer division simply requires that the second argument is non-zero.The premise φ =⇒ ¬(= a2 0) requires that the index constraints satisfythe proposition a2 6= 0 for the pre-checked instruction to be safe. Therefore,since a divide-by-zero is provably absent, it is safe to use the prechk-tagged38division instruction. As an aside, recall that requiring a3 is fresh ensures thatit is not declared, constrained, or referenced by the precondition.φ =⇒ ¬(= a2 0) a3 is freshC ` t.divprechk : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖div‖ a1 a2))Div-PrechkTagging memory loads and stores with prechk requires ensuring that thememory index is valid. Since Wasm and Wasm-prechk use linear memory,which is a contiguous block of memory, we simply have to ensure that theindex is within those bounds. The initial memory size is the number of 64Ki pages (65, 536 bytes), so we check that the constraints in the index typecontext ensure that the memory index plus the static offset is between 0 and65, 536−width. We use width as a shorthand to denote the number of bytesthat is being stored/loaded, it is equal to |t|/8 if tp? = , and otherwise equalto |tp|/8.Unfortunately, while the size of memory may be grown during programexecution, we are currently unable to reason about changing memory size.Therefore, we just use the initial memory size.Cmemory = n 2align ≤ (|tp| <)?|t| a3 is freshφ =⇒ (ge (add a1 (i32 o))(i32 0)),(le (add a1 (add (i32 o+ width))) (i32 n ∗ 64Ki))C ` t.loadprechk (tp_sx)? align o : (i32 a1); l; φ→ (t a2); l; φ, (t a2)Load-PrechkCmemory = n 2align ≤ (|tp| <)?|t|φ =⇒ (ge (add a1 (i32 o)) (i32 0)),(le (add a1 (add (i32 o+ width))) (i32 n ∗ 64Ki))C ` t.storeprechk tp? align o : (i32 a1) (t a2); l; φ→ ; l; φStore-PrechkIndirect function calls in Wasm require a dynamic check to ensure thatthe index into the table points to a function of a suitable type (recall the39explanation of tables and call indirect from section 2.2). Proving the safetyof an indirect function call involves showing that every possible functionthat could be called will not cause a run-time type error. We ensure this byrequiring that the type of every function at every possible index value has asubtype of the expected type: ∀0 < i ≤ n.(φ =⇒ ¬(= (i32 i) a)) ∨ tfis(i) <:tfi where tfis = (tfi2...). The ∀ and ∨ (as in (φ =⇒ ¬(= (i32 i) a))∨ tfis(i) <:tfi) in this case are at the meta level and not within the index language.Further, we must show that the provided table index is within the tableboundaries: φ =⇒ (gt n a) ∧ (le (i32 0) a).Ctable(i) = (n, (tfi2...))φ =⇒ (gt n a) ∧ (le (i32 0) a)tfis = (tfi2...) tfi = ti∗1; l1; φ1 → ti∗2; l2; φ2∀0 < i ≤ n. (φ =⇒ ¬(= (i32 i) a)) ∨ tfis(i) <: tfiC ` call indirectprechk tfi : ti∗1 (i32 a); l; φ1→ ti∗2; l; φ1, φ2Call-Indirect-PrechkAn Example of Using Types for Check Elimination Here we presenta short contrived example of using types for check elimination, based on theexample from Figure 3.7. We are typechecking a divprechk. First, we give themodule type context C1, which contains one local variable, which is an i32,and the instruction sequence we are typing, which is a safe division happeninginside of a block (Figure 3.7). We also use the shorthand C2 for C1 extendedwith the label postcondition for the instructions inside the block.C1 = {func , global , table , memory ,local i32, label , return }C2 = {func , global , table , memory ,local i32, label ((i32 a0); (i32 a2); ◦), return }The block takes two integers, and, using the local as temporary storage,either divides the first by the second, or the first by 1 if the second is 0. Inthe example we build up type derivations to reach a typing derivation for thewhole block. We first state the rule that we will use, than give the derivation(in many cases we apply Rule Stack-Poly inline for brevity). Typechecking40the example relies on select, where the second argument (i32.const 1) is chosenif the first argument (and the conditional) get local 0 is equal to zero, so theresult must be non-zero.1. Rule Tee-Local and Rule Stack-PolyNote that φ1 = ◦, (i32 a1), (i32 a2), and φ2 = φ1, (i32 a4), (= a4 a2).C2local(0) = i32(i32 a2) = (i32 a3)[0 := (i32 a2)] a4 is freshC2 ` tee local 0 : (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a1) (i32 a4); (i32 a2); φ22. Rule Const and Rule Stack-PolyNote that φ3 = φ2, (= a4 a2), (i32 a5), (= a5 (i32 1)).a5 is freshC2 ` i32.const 1 : (i32 a1) (i32 a4); (i32 a2); φ2→ (i32 a1) (i32 a4) (i32 a5); (i32 a2); φ33. Rule Composition1. 2.C2 ` (tee local 0) (i32.const 1): (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a1) (i32 a4) (i32 a5); (i32 a2); φ34. Rule Get-Local and Rule Stack-PolyNote that φ4 = φ3, (i32 a6), (= a6 a2).a6 is freshC2 ` get local 0 : (i32 a1) (i32 a4) (i32 a5); (i32 a2); φ3→ (i32 a1) (i32 a4) (i32 a5) (i32 a6); (i32 a2); φ45. Rule Composition41Note that φ4 = φ3, (i32 a6), (= a6 a2).3. 4.C2 ` (tee local 0) (i32.const 1) (get local 0): (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a1) (i32 a4) (i32 a5) (i32 a6); (i32 a2); φ46. Rule Select and Rule Stack-PolyNote that φ5 = φ4, (i32 a7), (if (= a6 (i32 0)) (= a7 a5)(= a7 a4)).a7 is freshC2 ` select:→ (i32 a1) (i32 a4) (i32 a5) (i32 a6); (i32 a2); φ4→ ((i32 a1) (i32 a7); (i32 a2); φ57. Rule Composition5. 6.C2 ` (tee local 0) (i32.const 1) (get local 0) (select): (i32 a1) (i32 a2); (i32 a3); φ1→ ((i32 a1) (i32 a7); (i32 a2); φ58. Rule Div-PrechkNote that φ5 = φ5, (i32 a8), (= a8(‖div‖ a1 a7)).φ5 =⇒ ¬(= a7 0) a8 is freshC2 ` (i32.divprechk): ((i32 a1) (i32 a7); (i32 a2); φ5→ (i32 a8); (i32 a2); φ69. Rule Composition427. 8.C2 ` (tee local 0) (i32.const 1) (get local 0) (select) (i32.divprechk): (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a8); (i32 a2); φ610. Rule Block9.C1 ` block (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a8); (i32 a2); φ6(tee local 0)(i32.const 1)(get local 0)(select)(i32.div)end : (i32 a1) (i32 a2); (i32 a3); φ1→ (i32 a8); (i32 a2); φ63.3.3 Module TypesThe complete module typing rules are in Figure 3.8 (note that im is animport and ex is an export). Functions f , typecheck their body e∗ underthe module type context C with the expected postcondition ti∗2; l2; φ2 in thelabel stack and return position, and with the local index store (t1 a1)∗ (t a2)∗constructed from the function’s arguments (t1 a1)∗ and declared locals (t a2)∗.Global variables glob must ensure that their initialization instructions e∗produce a value of the proper type t. Exported global variables cannot bemutable, if there are any exports defined, the global cannot have the mutabletag mut: ex∗ =  ∨ tg = t. Tables tab ensure that the indices in refer towell-typed functions and there are exactly as many indices as the expectedsize n. Memory mem simply has its declared initial size n from which it canonly grow bigger. All imported functions, globals, tables, and memories are43expected to have their declared type. They are typechecked during linking.Typechecking a module involves typechecking every component of themodule. Functions, f , are typechecked under the module type context, C,containing the entirety of the module. This means that functions can referto themselves, other functions, all globals, the table, and memory. Thismay seem to be a circular definition, but the type of the module is declaredstatically (as the combined declared types of all the module components), soit is just checking against the expected module index type context. Globals,glob, are typechecked under the module index context containing only theglobal variable declarations preceding the current declaration.44tfi = (t1 a1)∗; ; φ1 → ti∗2; l2; φ2C2 = C, local t∗1 t∗, label (ti∗2; l2; φ2), return (ti∗2, l2, φ2)C2 ` e∗ : ; (t1 a1)∗ (t a2)∗; φ1 → ti∗2; l2; φ2C ` ex∗ func tfi localt∗ e∗ : ex∗ tfi FuncC ` ex∗ func tfi im : ex∗ tfitg = mut? t ex∗ =  ∨ tg = t C ` e∗ : ; ; φ1 → (t a); ; φ2C ` ex∗ global tg e∗ : ex∗ tgtg = tC ` ex∗ global tg im : ex∗ tg(Cfunc(i) = tfi)nC ` ex∗ table n in : ex∗ (n, tfin) TableC ` ex∗ table (n, tfin) im : ex∗ (n, tfin) C ` ex∗ memory n : ex∗ nC ` ex∗ memory n im : ex∗ n(C ` f : ex∗f tfi)∗ (Ci ` globi : ex∗g tgi)∗(C ` tab : ex∗t (n, tfin))? (C ` mem : ex∗m n)?(Ci = {global tgi−1})∗i ex∗ ∗f ex∗ ∗g ex∗ ?t ex∗ ?m distinctC = {func tfi∗, global tg∗, table (n, tfin)?,memory n?}` module f∗ glob∗ tab? mem?Figure 3.8: Indexed Module Typing Rules45Chapter 4MetatheoryNow that we have introduced Wasm-prechk and shown how it can be usedfor reasoning, it is time to reason about Wasm-prechk itself. First, we willtake a look at the relationship between Wasm and Wasm-prechk, by showingmethods to translate Wasm programs to Wasm-prechk programs and viceversa. Then, we will prove the type safety of Wasm-prechk, to ensure thatour claim that Wasm-prechk is as safe as Wasm is valid. However, before wecan do any of that, we must “complete” our reasoning ability by creating away to connect the reduction relation form with the type system.4.1 Administrative Typing RulesWhile we have shown the Wasm-prechk typing rules for instructions within astatic context, we still need typing rules for administrative instructions andthe store used in reduction. Administrative instructions are introduced forreduction to keep track of information during reduction. For example, localis the result of reducing a closure call; it is used to reduce a function bodywithin the closed environment of the closure. They are not part of the surfacesyntax of a language (e.g., you cannot put a local block in a Wasm-prechkprogram), and can only appear as an intermediate term during reduction.Figure 4.2 shows the Wasm-prechk typing rules for module instances inst,the run time store s, and various data structures contained within s. There46S ::= {inst C∗, tab n∗, mem m∗}` s; v∗; e∗` s : S S;  `i v∗; e∗ : ti∗; l; φ`i s; v∗; e∗ : ti∗; l; φProgramS; (ti∗; l; φ)? `i v∗; e∗ : ti∗; l; φ(` v : (t a); φv)∗ C = Sinst(i), local t∗, return (tin; l; φ)?S; C ` e∗ :  : (t a)∗; φ∗v → tin; l; φS; (tin; l; φ)? `i v∗; e∗ : tin; l; φCodeFigure 4.1: Wasm-prechk Program Typing Rulesare many different judgments being introduced, so we explicitly state theform of the judgment before stating the rule for that judgment.During reduction, we use Rule Program (Figure 4.1) to ensure that aWasm-prechk program state (consisting of the store s, local variables v∗, andinstruction sequence e∗) is well typed (notice that it has the same form asthe reduction relation). It uses Rule Code and relies on the store being well-typed (Rule Store in Figure 4.2), to ensure that a reducible Wasm-prechkprogram is well typed. Rule Code checks that a sequence of instructions iswell typed with an empty stack, the indexed types and constraints for thegiven local variables in the precondition, and an optional return postcondition(not used by Rule Program). Since local variables are values, we knowthat each one of them is equal to some constant, so Rule Code is really justchecking that the sequence of instructions has some postcondition reachablefrom the given local variables. There is an optional return postcondition forRule Code because the typing rule for local blocks (as seen in Rule Localin Figure 4.3) has as a premise a judgment of the exactly same form, exceptwith a return postcondition.In addition to getting the type of the instructions being reduced, we also47need to know the type of the store s since it is part of the reduction relation.Rule Store checks that a run-time store, s is well typed by the store contextS. The store context S is to s as C is to inst. That is, it contains the typeinformation for everything in s. Rule Store ensures that every moduleinstance inst in s has the type of the index module context C in S usingRule Instance. Further, Rule Store ensures that all of the closures in all ofthe tables in s are well typed, and the the sizes of all the tables and memorychunks in S do not exceed the actual size of their implementations.To get the type of the store, we in turn have to know the types of each ofthe various run-time data structures. Rule Instance checks that a moduleinstance is well-typed by the index module context under the store contextS. It checks all of the closures cl∗ against their expected types tfi∗ inC, and similarly for all of the globals (v∗ and (mut? t)∗). The table andmemory indices (i and j, respectively) are used to look up the the relevanttypes ((n, tfi∗) and m, respectively) in the store context S. Closures aretypechecked by Rule Closure, which falls back on the module typing rulesfrom Figure 3.8 to typecheck the function definition inside of the closure.Rule Admin-Const gets the postcondition indexed types and constraints onvalues; it is used to typecheck local and global variables.Now we will introduce the typing rules for administrative instructions,and the administrative typing judgment in Figure 4.3. The administrativetyping judgment S; C ` e∗ : tfi extends the Wasm-prechk typing rules forinstructions to include administrative instructions and the store context S.Every rule of the judgment C ` e∗ : tfi (recall the rules enumerated insection 3.3) is implicitly added to the administrative judgment by acceptingany S.Most of the rules for administrative instructions check against extrainformation provided by the administrative typing judgment. Rule Localtypechecks a local block using Rule Code to ensure that the body e∗ is welltyped with the indexed types and constraints for local variables providedby the local block as the precondition and any postcondition. Since localblocks are inline expansions of function calls, we use the optional returnpostcondition functionality of Rule Code to ensure that returning from48` s : SS = {inst C∗, tab n∗,mem m∗}(S ` inst : C)∗ ((S ` cl : tfi)∗)∗ (n ≤ |cl∗|)∗ (m ≤ |b∗|)∗` {inst inst∗, tab (cl∗)∗,mem (b∗)∗} : S StoreS ` inst : C(S ` cl : tfi)∗ (` v : (t a), φv)∗(Stab(i) = n)? (Smem(j) = m)?S ` {func cl∗, glob v∗, tab i?,mem j?}: {func tfi∗, global (mut? t)∗, table n?,memory m?}Instance` v : ti; φ` t.const c : (t a); ◦, (t a), (eq a (t c)) Admin-ConstS ` cl : tfiSinst(i) ` f : tfiS ` {inst i, code f} : tfi ClosureFigure 4.2: Wasm-prechk Store Typing Rulesinside the local block will be well typed. Rule Call-Cl typechecks callinga closure by ensuring that the closure cl being called has the same type asthe call instruction call cl in S. Rule Trap is always well typed under anyprecondition and postcondition. Rule Label typechecks the body of thelabel block with the precondition of the saved instructions pushed onto thelabel stack. If the label was generated by a loop, then the precondition ofthe saved values is the precondition of the loop, and we know the loop is welltyped. Otherwise, the saved instructions will be an empty sequence and willbe well typed from the precondition.49S; C ` e∗ : tfiS; (tin; l2; φ2) `i v∗l ; e∗ : tin; l2; φ2S; C ` local{i; v∗l } e∗ end : ; l1; φ1 → tin; l1; φ1, φ2LocalS ` cl : tfiS; C ` call cl : tfi Call-Cl S; C ` trap : tfi TrapS; C ` e∗0 : ti∗3; l3; φ3 → ti∗2; l2; φ2S; C, label (ti∗3; l3; φ3) ` e∗ : ; l1; φ1 → ti∗2; l2; φ2S; C ` label{e∗0} e∗ end : ; l1; φ1 → ti∗2; l2; φ2LabelFigure 4.3: Wasm-prechk Administrative Instruction RulesGiven these additional typing judgments and rules, we can now show themetatheoretic properties mentioned above.4.2 Relationship Between Wasm and Wasm-prechkWe want to show two properties about the relationship between Wasm andWasm-prechk. First, we want Wasm-prechk to be backwards compatiblewith Wasm. It should be possible to convert well-typed Wasm programsinto well-typed Wasm-prechk programs with no additional developer effort.We demonstrate a simple yet naive way of embedding Wasm programsinto Wasm-prechk in subsection 4.2.1. Second, we want to show that well-typed Wasm-prechk programs can be turned into Wasm programs. Thisis accomplished in subsection 4.2.2 using an erasure function that turnsWasm-prechk programs and types into Wasm programs and types.4.2.1 Embedding Wasm in Wasm-prechkWe present a way to embed Wasm programs in Wasm-prechk. The embeddingfunction takes a Wasm program and replaces all of the type annotations withindexed function types that have no constraints on the variables. Intuitively,50the type annotations are the only part of the surface syntax of Wasm thatisn’t in Wasm-prechk, so we must figure out a way to bring it over. While thisembedding requires no additional developer effort, it provides no informationto the indexed type system beyond what can be inferred from the instructionsin the program. We conjecture that a well typed Wasm program embeddedin Wasm-prechk is also well typed, but we have not proved it.We typeset Wasm-prechk instructions in a blue sans serif font and Wasminstruction in a bold red font to set them apart.Conjecture 1. Well Typed Wasm Programs Embedded in Wasm-prechk areWell TypedIf `module f∗ glob∗ tab? mem?,then ` embedmodule(module f∗ glob∗ tab? mem?)Embedding works purely over the surface syntax of the languages. Assuch, we define embedding over modules: the pinnacle syntactic objects ofboth the Wasm and Wasm-prechk surface syntax hierarchies. Embedding amodule module means embedding all of the functions f∗ in the module, andembedding the table tab parameterized with all of the function definitions f∗.We do not have to embed globals glob∗ or the memory mem? as they havethe same syntax in both Wasm and Wasm-prechk. We explain how to embedtables tab in Definition 2, and functions f in Definition 3.Definition 1. embedmodule(module)C = moduleembedmodule(module f∗ glob∗ tab? mem?) = module embedf (f)∗glob∗embedtab(tab?)f∗mem?Tables in Wasm-prechk must also provide the indexed function typesof all the functions they contain, so to embed them we must include thosetypes. We do this by parameterizing the embedding of the table tab with allof the declared functions f∗. Then, we retrieve the indexed function typeti1; l1; φ1 → ti2; l2; φ2 of the function pointed to by the function index i in51f∗ for every function index i in the table. We cannot embed imported tablesbecause we have no way of accessing the types of the functions included inthe table.Definition 2. embedtab(tab)f∗= tabembedtab(tab n in) = tab n (ti1; l1; φ1 → ti2; l2; φ2)nwhere ∀i.f∗(i) = func ti1; l1; φ1 → ti2; l2; φ2local t∗ e∗The embedding of functions, Definition 3, both must construct an indexedfunction type for itself and embed its body. Function bodies have their localvariables defined by the function that they are enclosed in. Thus, when thefunction body is embedded we pass the local types (t∗1 t∗) so the body knowshow to constrain local variables. We construct an indexed function type thathas the precondition of the expected values on the stack turned into indexedtypes using fresh index variables and the types t∗1 from the Wasm type, anddo the same with the postcondition and t∗2. We cannot embed importedfunctions because we have no way of accessing the types of the local variablesof the function.Definition 3. embedf (f) = fembedf (func (t∗1 → t∗2)local t∗ e∗)= func ((t1 a1)∗; ; (◦, (t1 a1)∗)→ (t2 a2)∗; (t1 a3)∗ (t a4)∗;(◦, (t2 a2)∗, (t1 a3)∗(t a4)∗))t∗ (embede(e)(t∗1 t∗))∗endEmbedding instructions replaces all function types used within the Wasmsyntax with Wasm-prechk indexed function types, and adds the functiontypes for all of the functions in a table to the table’s type declaration. Thisoccurs within blocks and indirect function calls, as shown in Definition 4.The indexed types simply have fresh index variables that are different in theprecondition and postcondition, and the primitive types for the stack are52known from the Wasm type t∗1 → t∗2. To know what the local variables are,we parameterize the embedding over the types of local variables (t∗).Definition 4. embede(e)t∗= eembede∗(block (t∗1 → t∗2)e∗end)t∗= block((t1 a1)∗; (t a3)∗; (◦, (t1 a1)∗, (t a3)∗)→ (t2 a2)∗; (t a4)∗; (◦, (t2 a2)∗, (t a4)∗))embede∗(e∗)t∗endembede∗(loop (t∗1 → t∗2)e∗end)t∗= loop((t1 a1)∗; (t a3)∗; (◦, (t1 a1)∗, (t a3)∗)→ (t2 a2)∗; (t a4)∗; (◦, (t2 a2)∗, (t a4)∗))embede∗(e∗)t∗endembede∗(if (t∗1 → t∗2)e∗end)t∗= if((t1 a1)∗; (t a3)∗; (◦, (t1 a1)∗, (t a3)∗)→ (t2 a2)∗; (t a4)∗; (◦, (t2 a2)∗, (t a4)∗))embede(e∗1)t∗ embede(e∗2)t∗endembede∗(call indirect(t∗1 → t∗2))t∗= call indirect((t1 a1)∗; (t a3)∗; (◦, (t1 a1)∗, (t a3)∗)→ (t2 a2)∗; (t a4)∗; (◦, (t2 a2)∗, (t a4)∗))embede∗(e)t∗ = e, otherwiseembede∗(e∗)t∗ = (embede∗(e)t∗)∗These are not the only differences in the surface syntax between Wasm andWasm-prechk: we also introduced four new instructions (the prechk-taggedinstructions). The definition of embedding we have introduced has beenentirely syntactic, but that will not work for replacing non-prechk-taggedinstructions with prechk-tagged versions during embedding since we must beable to ensure that stronger guarantees are met. Thus, we do not have anexplicit embedding that provides prechk-tagged instructions, though we doposit the existence of a trivial embedding that would provide prechk-tagged53instructions. One could, for example, check at every div, call indirect , load ,and store whether the prechk-tagged version of the instruction is well typed,and only if it is well typed replace the instruction with the prechk-taggedversion. However, a more sophisticated static analysis could provide moreprecise type annotations and therefore potentially allow even more checkeliminations.4.2.2 Erasing Wasm-prechk to WasmWe provide an erasure function for Wasm-prechk that transforms Wasm-prechk programs into Wasm programs by discarding the extra informationfrom the Wasm-prechk type system and replacing prechk-tagged instructionswith their non-tagged counterparts. Erasure is useful in the type safetyproof because it lets us reuse much of the proof of progress from Wasm (seesubsection 4.3.2). Therefore, we define erasure not just for the surface syntax,like we did for embedding, but also for typing constructs (such as the moduletype context), administrative instructions, and runtime data structures (suchas the store). We show that erasing a well-typed Wasm-prechk programproduces a well-typed Wasm program.As with the presentation of the embedding, we typeset Wasm-prechkinstructions in a blue sans serif font and Wasm instruction in a bold redfont.Erasing Surface Syntax As with embedding, we start by defining erasurewith the pinnacle syntactic object: the module. Defining and erasure formodules relies on the erasure of tables and functions, and therefore instructionsand indexed function types. Keep in mind that the proofs of sound erasurework over the typing rules for these constructs, so we also define erasure ofmodule type contexts since they are used in the typing rules for modules.Erasing a module erases all of the functions f∗ and the table tab?. Theglobals glob∗ and optional memory mem? both have the same syntax inWasm-prechk as in Wasm.Definition 5. erasemodule(module) =module54erasemodule(module f∗ glob∗ tab? mem?) = module erasef (f)∗glob∗erasetab(tab)?mem?We show that erasing a well-typed Wasm-prechk module yields a well-typed Wasm module.Theorem 1. Sound Module ErasureIf ` module f∗ glob∗ (n, tfin)? mem?,then `module erasef (f)∗glob∗n?mem?Proof. Note that the globals glob∗ and memory mem? are not affected byerasure, and have the same module typing rules in Wasm as in Wasm-prechk.Thus, we only need to reason about the functions f∗ and table tab?.Then, by Lemma Sound Function Typing Erasure and LemmaSound Table Erasure, we have that `module erasef (f)∗glob∗n?mem?.Erasing a table definition table n in does nothing, since a table definitionhas the same syntax in Wasm-prechk and in Wasm. However, erasing animported table declaration table (n, tfin) im must get rid of the indexedfunction types tfin. We do not use or care about the exports, since they areunchanged and only used for linking, so we omit them.Definition 6. erasetab(tab) = tabtable n in = table n intable (n, tfin) im = table n imWe show that erasure on well typed Wasm-prechk tables tab is soundwith respect to Wasm’s type system. This proof relies on the definition oferaseC(C): Definition 10.55Lemma 1. Sound Table ErasureIf C ` tab,then eraseC(C) ` erasetab(tab)Proof. By case analysis on erasetab(tab).• Case: tab = table n inWe know (Cfunc(i) = tfi)n because it is a premise of Rule Table.Then, (eraseC(C)func(i) = tfi)n by definition of eraseC(C).Therefore, eraseC(C) ` table n in because Wasm accepts any moduletype context in that rule.• Case: tab = table (n, tfin) imTrivially eraseC(C) ` table n im because Wasm accepts any moduletype context and imported table.To erase a function definition f , we erase both the type declarationti∗1; l1; φ1 → ti∗2; l2; φ2 and the body e∗. We can also erase an importedfunction by erasing the declared type tfi.Definition 7. erasef (f) = ferasef (func ti∗1; l1; φ1→ ti∗2; l2; φ2local t∗ e∗)= func erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)local t∗ erasee∗(e∗)erasef (func ti∗1; l1; φ1→ ti∗2; l2; φ2im)= func erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2) imWe show that erasing a Wasm-prechk function f , that is well typed undera module type context C, produces a Wasm function erasef (f) that is welltyped under the erased module type context eraseC(C). This is useful notjust for erasing the surface syntax, but also because functions are a part of56closures which are used at run time (as part of module instances and tables).The proof relies on Lemma Sound Static Typing Erasure to prove thatthe body is still well typed. The case of imported functions is trivial becausean imported function is well typed under absolutely any context and withany function type, so it is omitted.Lemma 2. Sound Function Typing ErasureIfC ` func (t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2local t∗ e∗ : ex∗ (t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2theneraseC(C) ` erasef (func erasetfi((t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2)local t∗ erasee∗(e∗)): ex∗ erasetfi((t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2)Proof. We must show thateraseC(C, local(t∗1 t∗), label((t2 a2); l2; φ2), return((t2 a2); l2; φ2))` erasee∗(e∗): erasetfi((t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2)since it is the only premise of typechecking a function definition in Wasm.We know the following because it is a premise of Rule Func which wehave assumed to hold.C, local(t∗1 t∗), label((t2 a2); l2; φ2), return((t2 a2); l2; φ2)` e∗: (t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2Then, by Lemma Sound Static Typing Erasure, we have thateraseC(C, local(t∗1 t∗), label((t2 a2); l2; φ2), return((t2 a2); l2; φ2))` erasee∗(e∗): erasetfi((t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2)57Erasing an indexed type function keeps only the primitive Wasm types (t∗1and t∗2) from the indexed types representing the stack ((t1 a1)∗ and (t2 a2)∗),and discards everything else.Definition 8. erasetfi(tfi) = tferasetfi((t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2) = t∗1 → t∗2Erasing instructions involves erasing the indexed function types for everyinstruction that includes it as part of their syntax (blocks and indirect functioncalls). We must also remove the prechk tag from prechk-tagged instructionsto turn them into instructions that exist in Wasm.58Definition 9. erasee∗(e) = eerasee∗(block tfi e∗ end) = block erasetfi(tfi)erasee∗(e∗)enderasee∗(loop tfi e∗ end) = loop erasetfi(tfi)erasee∗(e∗)enderasee∗(if tfi e∗1 e∗2 end) = if erasetfi(tfi)erasee∗(e∗1)erasee∗(e∗2)enderasee∗(labeln {e∗0} e∗ end) = labeln {erasee∗(e∗0)}erasee∗(e∗)enderasee∗(localn {i; v∗} e∗ end) = localn {i; v∗}erasee∗(e∗)enderasee∗(call indirect tfi) = call indirect erasetfi(tfi)erasee∗(t.divprechk) = t.diverasee∗(t.call indirectprechk ) = t.call indirecterasee∗(t.storeprechk tp? align o) = t.store tp? align oerasee∗(t.loadprechk (tp_sx)? align o) = t.load (tp_sx)? align oerasee∗(e) = e, otherwiseerasee∗(e∗) = erasee∗(e)∗Erasing Typing Constructs Here, we prove that erasing a Wasm-prechkstatic typing derivation is sound with respect to Wasm’s type system. Thismeans that erasure on the Wasm-prechk static typing judgment is soundwith respect to Wasm’s type system. Specifically, a Wasm-prechk instructionsequence e∗, that is well typed under a module type context C, produces aWasm instruction sequence e′∗ = erasee∗(e∗) that is well typed under theerased module type context C ′ = eraseC(C).59Lemma 3. Sound Static Typing ErasureIf C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,then eraseC(C) ` erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)Proof. We proceed by induction over typing derivations. Most proof casesare omitted as they are simple, but we provide a few to give an idea of whatthe proofs look like. Intuitively, we want to show that erasing the typingderivation produces a valid Wasm typing derivation.For most of the cases, the sequence of instructions e∗ contains only a singleinstruction e2, so we elide the step of turning erasee∗(e∗) into erasee∗(e2).We present one Case below, the rest are in the appendix ( B.1).• Case: C ` t.binop : (t a1) (t a2); l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (binop a1 a2))We want to show thateraseC(C) ` erasee∗(t.binop): erasetfi((t a1) (t a2); l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (binop a1 a2)))By the definition of erasee, we want to show that eraseC(C) ` t.binop :t t→ t is valid in Wasm.Trivially, we have eraseC(C) ` t.binop : t t→ t by Rule Wasm-Binop,since Rule Wasm-Binop works under any module type context.To erase a module type context, we must erase all of the function typestfi∗, the table type (n, tfi∗2) if one is present, and the postconditions in thelabel stack ((t1 a1)∗; l1; φ1)∗ and the return stack ((t2 a2)∗; l2; φ2)?. We erasepostconditions the same way we erase the postconditions of indexed functiontypes: by keeping only the primitive Wasm types (t∗1 in the case of a labelpostcondition). Recall that erasing a table type means discarding the typeinformation about the functions in the table.60Definition 10. eraseC(C) = CeraseC({func tfi∗, global tg∗,table (n, tfi∗2)?,memory m?, local t∗,label ((t1 a1)∗; l1; φ1)∗,return ((t2 a2)∗; l2; φ2)?})= {func erasetfi(tfi∗),global tg∗, table n?,memory m?, local t∗,label (t∗1)∗, return (t∗2)?}Erasing Programs Defining and erasure for programs relies on the erasureof the store and its various structures, as well as the erasure of instructionswhich we have already defined and proven. Remember, the proofs of sounderasure work over the typing rules for these constructs, so we have to showsound erasure for all of the various typing rules that Rule Program relieson.Now we will show that erasing a well-typed Wasm-prechk program inreduction form (s; v∗; e∗) is sound with respect to Wasm’s type system.Intuitively, we accomplish this by showing that erasing typing derivations ofthe Rule Program judgment produce valid Wasm typing derivations, like inLemma Sound Static Typing Erasure. To do so, we must show sounderasure for Rule Code, as it is a premise of Rule Program; this is done byLemma Sound Code Typing Erasure. Erasing programs involves erasingmany run-time data structures, including the store s and store context S, aswell as modules instances inst∗ in s, and closures cl in modules instances andthe optional table. Erasing the store is shown to be safe by Lemma SoundStore Erasure.Theorem 2. Sound Program Typing ErasureIf `i s; v∗ e∗ : (t2 a2)∗; l2; φ2,then `i erases(s); v∗; erasee∗(e∗) : t∗2Proof. We must show that ` erases(s) : S for some Wasm store context S,and that eraseS(S); `i erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2).We have ` s : S′, where S′ is a Wasm-prechk store context, because it isa premise of Rule Program which we have assumed to hold.61Then, ` erases(s) : eraseS(S′) is valid by Lemma Sound Store Era-sure. Since eraseS(S′) is a Wasm store context, we have that ` erase(s) : §for some Wasm store context S where S = eraseS(S′).We also have S; `i v∗ e∗ : ; l1; φ1 → (t2 a2)∗; l2; φ2 as a premise of RuleProgram.In which case we have eraseS(S); `i erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 →ti∗2; l2; φ2) by Lemma Sound Code Typing Erasure.The sound erasure of Rule Code is used in the sound erasure of programs.Thus, we only prove the case when the optional return stack ((t2 a2)∗; l2; φ2)?is empty because we are only proving this to use later in Rule Program,which never uses the return stack. Lemma Sound Code Typing Erasurerelies on Lemma Sound Admin Typing Erasure, which shows a similarproperty, but for the administrative typing judgment S; C ` e∗ : tfi.Lemma 4. Sound Code Typing ErasureIf S; `i v∗ e∗ : ; l1; φ1 → (t2 a2)∗; l2; φ2,then eraseS(S); `i erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)Proof. We must show that (` v : tv)∗ anderaseS(S); eraseC(Sinst(i), local t∗v` erasee∗(e∗): erasetfi(; l1; φ1 → (t2 a2)n; l2; φ2)We have (` v : tv)∗ trivially since it is a premise of Rule Code which wehave assumed to hold.We also have S; Sinst(i), local t∗v ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2 because ittoo is a premise of Rule Code.Then, by Lemma Sound Admin Typing Erasure, we have thateraseS(S); eraseC(Sinst(i), local t∗v` erasee∗(e∗): erasetfi(; l1; φ1 → (t2 a2)n; l2; φ2)62Lemma Sound Admin Typing Erasure builds on Lemma SoundStatic Typing Erasure by adding the store context S and typing rulesfor administrative instructions. It is necessary to add these rules and extrainformation because they are used for typechecking programs. Note thatwhile we add S to the judgment used in Lemma Sound Static TypingErasure to get S; C ` e∗; tfi, none of the rules previously proven referenceS in any way, they simply match any store context.Lemma 5. Sound Admin Typing ErasureIf S; C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,then eraseS(S); eraseC(C) ` erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)Proof. We proceed by induction over typing rules. In addition to the priorcases from Lemma Sound Static Typing Erasure, which trivially stillhold since the value of S does not matter to those rules, we add proves for afew administrative typing rules, which may refer to S. Again, several proofcases are omitted as they are simple.We present one Case below, the rest are in the appendix ( B.1).• S; C ` labeln{e∗0} e∗ end : ; l1; φ1 → (t2 a2)n; l2; φ2We must show thateraseS(S); eraseC(C)` erasee∗(e∗0): erasetfi((t3 a3)∗; l3; φ3 → (t2 a2)n; l2; φ2)anderaseS(S); eraseC(C, label((t3 a3)∗; l3; φ3))` erasee∗(e∗): erasetfi(; l1; φ1 → (t3 a3)∗; l3; φ3)as they are the premises of typechecking a label block in Wasm.We have that S; C ` e∗0 : (t3 a3)∗; l3; φ3 → (t2 a2)n; l2; φ2 since it is apremise of Rule Label which we have assumed to hold.63Then, by the inductive hypothesis for the stored instructions e∗0 beingwell typed, we have thateraseS(S); eraseC(C)` erasee∗(e∗0): erasetfi((t3 a3)∗; l3; φ3 → (t2 a2)∗; l2; φ2)S; C, label((t3 a3)∗; l3; φ3)) ` e∗ : ; l1; φ1 → (t3 a3)∗; l3; φ3, because itis a premise of Rule Label which we have assumed to hold.By the inductive hypothesis for the body e∗ being well typed, we havethateraseS(S); eraseC(C, label((t3 a3)∗; l3; φ3))` erasee∗(e∗): erasetfi(; l1; φ1 → (t3 a3)∗; l3; φ3)We must prove safe erasure about the store s for use in Theorem 2. Firstthough, we must define erasure for s. Erasing the store erases all of themodules instances and closures in the tables inside the store. Note thatin the definition we have expanded the definition of a table instance to({inst i, func f}∗)∗ for extra clarity.Definition 11. erases(s) = serases({inst inst∗,tab ({inst i, func f}∗)∗,mem meminst∗})= {inst eraseinst(inst)∗,tab ({inst i, func erasef (f)}∗)∗,mem meminst∗}Lemma Sound Store Erasure proves that erasing a well-typed Wasm-prechk store results in a well-typed Wasm store.Lemma 6. Sound Store ErasureIf ` s : S, then ` erases(s) : eraseS(S)64Proof. Note thats = {inst inst∗, tab ({inst i, func f}∗)∗, mem meminst∗} andS = {inst C∗, tab (n, tfi∗)∗, mem m∗}Then,eraseS(S) = {func erasetfi(tfi)∗, global tg∗, table n, memory n?, ...}by the definition of eraseC .Then, we must prove the following properties, as they are the premises of` erases(s) : eraseS(S):1. (eraseS(S) ` eraseinst(inst) : eraseC(C))∗We have that (S ` inst : C)∗, because it is a premise of Rule Storethat we have assumed to hold.Then, we have eraseS(S) ` eraseinst(inst) : eraseC(C))∗ by LemmaSound Instance Typing Erasure.2. ((eraseS(S) ` {inst i, func erasef (f)} : erasetfi(tfi))∗)∗We have ((S ` cl : tfi)∗)∗), because it is a premise of Rule Store thatwe have assumed to hold.Then, ((eraseS(S) ` {inst i, func erasef (f)} : erasetfi(tfi))∗)∗ byLemma Sound Closure Typing Erasure3. (n ≤ |{inst i, func erasef (f)}|)∗We have that (n ≤ |{inst i, func f}|)∗, because it is a premise of RuleStore that we have assumed to hold.Because the number of closures is not affected by erasure, we can thensay that (n ≤ |{inst i, func erasef (f)}|)∗4. (m ≤ |b∗|)∗Trivially, we have that (m ≤ |b∗|)∗, because it is a premise of RuleStore that we have assumed to hold.65Erasing a module instance erases all of the functions f in the closures(which we have expanded inline to {inst i, func f}) within the module in-stance.Definition 12. eraseinst(inst) = insteraseinst({func {inst i, func f}∗,global v∗, table i?,memory j?})= {func {inst i, func erasef (f)}∗,global v∗, table i?,memory j?}We now prove that if a Wasm-prechk module instance inst has type Cunder the store context S, then the erased Wasm instance eraseinst(inst) willhave the erased type erasec(C) under the erased store context eraseS(S). Todo this, we rely on the above lemmas to safely erase index information fromfunction declarations and table declarations (globals and memory have thesame type information in both Wasm-prechk and Wasm). This will be usefulfor proving that a well-typed Wasm-prechk store s erases to a well-typedWasm store erases(s) since stores contain many instances. To do this, we relyon the above lemmas to safely erase index type information about closuresand tables (globals and memory have the same type information in bothWasm-prechk and Wasm).Lemma 7. Sound Instance Typing Erasure If S ` inst : C, theneraseS(S) ` eraseinst(inst) : eraseC(C)Proof. Note thatS = {inst C∗, tab (n, tfi∗)∗, mem m∗}inst = {func {inst i, func f}∗, global v∗, table i?,memory j?}C = {func tfi∗, global tg∗, table (n, tfi2)?, memory n?, . . . }Then,eraseC(C) = {func erasetfi(tfi)∗, global tg∗, table n, memory n?, ...}by the definition of eraseC .Then, we must prove the following properties, as they are the premises oferaseS(S) ` eraseinst(inst) : eraseC(C):661. eraseS(S) ` {inst i, func f} : erasetfi(tfi))∗We have that S ` {inst i, func f} : tfi, because it is a premise of RuleInstance that we have assumed to hold.Then, we have eraseS(S) ` {inst i, func f} : erasetfi(tfi))∗ by LemmaSound Closure Typing Erasure.2. (` v : tg)∗Trivially, this is a premise of S ` inst : C and is not affected by erasure,so therefore it holds.3. eraseS(S)tab(i) = neraseS(S)tab(i) = n by definition of eraseS .Therefore, eraseS(S)tab(i) = n.4. eraseS(S)mem(i) = n?Trivially, this is a premise of S ` inst : C and is not affected by erasure,so therefore it holds.We erase store contexts by erasing all of the module type instances C∗and table types (n, tfi∗)∗ within.Definition 13. eraseS(S) = SeraseS({inst C∗,tab (n, tfi∗)∗, mem m∗})= {inst erasec(C)∗,tab n∗,mem m∗}Finally, we prove that if a Wasm-prechk closure is well typed than theerased closure is well typed.Lemma 8. Sound Closure Typing ErasureIf S ` {inst i, func f}∗ : tfi,then eraseS(S) ` {inst i, func erasef (f)}∗ : erasetfi(tfi)67Proof. We must show that eraseS(S)inst(i) ` erasef (f) : erasetfi(tfi).We have Sinst(i) ` f : tfi since it is a premise of Rule Closure whichwe have assumed to hold.Then, eraseS(S)inst(i) ` erasef (f) : erasetfi(tfi) by Lemma SoundFunction Typing Erasure.4.3 Type SafetyType safety is the property that a well-typed program either reduces to anotherwell-typed program, is an intentionally irreducible expression (in the case ofWasm-prechk, a sequence of values), or throws an error (trap, in the case ofWasm-prechk). Thus, type safety assures us that the behavior of a well-typedprogram is always well defined. The type safety of Wasm guarantees a numberof important properties, including memory safety. Proving the type safety ofWasm-prechk gives us a high degree of assurance that it has the same levelof safety as Wasm.4.3.1 Subject ReductionSubject reduction, also sometimes referred to as “type preservation”, ensuresthat if a program has a specific type, then the program will have the sametype after a reduction step. Before we present the subject reduction proof,we first introduce a number of useful lemmas.Lemma Inversion tells us what typing rules can apply to a given Wasm-prechk instruction sequence, and therefore lets us reason about what thetype of that sequence looks like. For example, if we have a typing derivation,D for S; C ` t.const c : ti∗1; l1; φ1 → ti∗2; l2; φ2, then we know that D musthave at its base Rule Const, because that is the only way we have of typingconstant instructions. D can also include any number of applications of RuleSubtyping and Rule Stack-Poly, because they can be applied to anywell-typed sequence of instructions.We do not know the exact types of instructions just from them being welltyped, since the typing rules are non-deterministic. However, we can reason68about the general shape of the types given the base type on top of whichRule Subtyping and Rule Stack-Poly get applied. Additionally, RuleComposition can be used with the empty sequence and any well-typed singleinstruction. The addition of Rule Composition with the empty sequence istrivial because the postcondition of an empty instruction sequence must beimmediately reachable from the precondition. Therefore the stack and localindex store must be the same in both the precondition and postconditionof the empty sequence in the above case, and the postcondition index typecontext must be reachable from the precondition index type context.Most cases of Lemma Inversion are omitted. The complete definitioncan be found in the appendix (section B.2).Lemma 9. Inversion• If S; C ` t.const c : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 (t a), l1 = l2,and φ1, (t a), (= a (t c)) =⇒ φ2.• If S; C ` t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (t a1) (t a2),ti∗2 = ti∗ (t a3), l1 = l2, and φ1, (t a3), (= a3 (binop a1 a2)) =⇒ φ2.• If S; C ` block (ti∗3; l3; φ3 → tim4 ; l4; φ4)e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2then ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 tim4 , l1 = l3, l2 = l4, φ1 =⇒ φ3, φ4 =⇒ φ2,and S; C, label(tim4 ; l4; φ4) ` e∗ : ti∗3; l3; φ3 → tim4 ; l4; φ4.• If S; C ` br i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗3 ti∗, Clabel(i) =ti∗; l1; φ3, and φ1 =⇒ φ3.• If S; C ` call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4 : ti∗1; l1; φ1 → ti∗2; l2; φ2,then ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 ti∗4, l2 = l1, φ1 =⇒ φ3, and φ3, φ4 =⇒ φ2.• If S; C ` e∗1 e2 : ti∗1; l1; φ1 → ti∗3; l3; φ3, then S; C ` e∗1 : ti∗1; l1; φ1 →ti∗2; l2; φ2, and S; C ` e2 : ti∗2; l2; φ2 → ti∗3; l3; φ3.Proof. Proof omitted, but follows from induction over typing derivations.69The next lemma, Lemma Lift-Consts, shows that if a sequence ofconstants, vn, has a certain postcondition within a nested context, Lj , thenit has the same postcondition outside of that context with the preconditionof the context. We use this rule for branching and returning when we havesome values vn inside a reduction context Lj .The intuition for the proof is that the nature of nested contexts are suchthat all of the instructions preceding vn are values and therefore only addfresh index variables which are constrained to be equal to constants. Thus,we can pull vn outside of the nested context and know that we can still getto the postcondition because we can add back in, using implication, all of thefresh index variables that we would have added from the values preceding.Lemma 10. Lift-ConstsIf S; C ` vn : ; l3; φ3 → tin; l3; φ4 is a subderivation of S; C ` Lj [vn] :s1; l1; φ1 → s2; l2; φ2,then S; C ` vn : ; l1; φ1 → tin; l3; φ4 after reductionProof. By induction on j.• Base case: j = 0We want to show that S; C ` vn : ; l1; φ1 → tin; l3; φ4 after reduction.We have S; C ` v∗0 vn e∗ end : s1; l1; φ1 → s2; l2; φ2 for some v∗0 and e∗by expanding L0.Then, S; C ` (t.const c)∗ : ; l1; φ0 → (t a)∗; l1; φ0, (t a)∗, (eq a (t c))where v∗0 = (t.const c)∗ and φ1 =⇒ φ0 by Lemma Inversion on RuleConst.Further, S; C ` vn : ; l3; φ0, (t a)∗, (eq a (t c))→ (t a)∗ tin; l3; φ4, byLemma Inversion on Rule Const.We now have all the information we need to show what we want toshow.We know φ0, (t a)∗, (eq a (t c)) =⇒ φ3.70Recall that S; C ` vn : ; l3; φ0, (t a)∗, (eq a (t c)) → (t a)∗ tin; l3; φ4,thenS; C ` vn : (t a)∗; l3; φ0, (t a)∗, (eq a (t c))→ (t a)∗, (t a)∗ tin; l3; φ4by Rule Subtyping.If v∗0 are not executed (i.e., they are not part of the reduced expression),then a∗ are fresh, so φ0 =⇒ φ0, (t a)∗, (eq a (t c)), and thereforeS; C ` vn : ; l1; φ0 → tin; l1; φ4 by Rule Subtyping and since l1 = l3.Then, S; C ` vn : ; l1; φ1 → tin; l1; φ4 by subtyping.• Induction case: j = k + 1We want to show that S; C ` vn : ; l1; φ1 → tin; l3; φ4 after reduction.We have S; C ` labeln{e∗0} v∗0 Lk[vn] e∗1 end : s1; l1; φ1 → s2; l2; φ2 forsome v∗0, e∗0, and e∗1 by expanding Lj .Then, S; C ` (t.const c)∗ : ; l1; φ0 → (t a)∗; l1; φ0, (t a)∗, (eq a (t c))where v∗0 = (t.const c)∗ and φ1 =⇒ φ0 by Lemma Inversion on RuleConst.Further, S; C ` Lk[vn] : (t a)∗; l1; φ0, (t a)∗, (eq a (t c)) → s5; l5; φ5for some s5; l5; φ5 by Lemma Inversion on Rule Label.Now we can prove want we wanted to show.We know S; C ` vn : ; l1; φ0, (t a)∗, (eq a (t c)) → tin; l1; φ4 by theinductive hypothesis.If v∗0 are not executed (i.e., after one reduction step), a∗ are fresh,so φ0 =⇒ (t a)∗, (eq a (t c)), and therefore S; C ` vn : ; l1; φ0 →(t a)∗ tin; l3; φ5 by Rule Subtyping and since l1 = l3.Then, S; C ` vn : ; l1; φ1 → (t a)∗ tin; l3; φ3 by Rule Subtyping.Theorem 3. Subject ReductionIf `i s; v∗; e∗ : ti∗; l; φ and s; v∗; e∗ ↪→i s′; v′∗; e′∗ then `i s′; v′∗; e′∗ :ti∗; l; φ.71Proof. We have ` s : S and S;  `i v∗; e∗ : ti∗; l; φ because they are premisesof Rule Program.Then, by Lemma Subject Reduction for Code, we have that ` s′ : Sand S;  `i v′∗; e′∗ : ti∗; l; φ.Thus, ` s′; v′∗; e′∗ : ti∗; l; φ by Rule Program.Lemma Subject Reduction for Code proves subject reduction of theRule Code typing rule. That is, it proves that if a sequence of instructionse∗ and local variables v∗ is typed by the Rule Code typing rule, then aftera step of reduction the reduced instructions e′∗ and locals v′∗ will have thesame postcondition ti∗; l; φ. Further, if reduction modifies the store s, thanthe modified store s′ will have the same type S.In many reduction cases, there are values on the stack that get consumedby reducing an instruction. This creates a bit of a problem because thosevalues represent intermediate state, and as such will introduce new indexvariables to the index type context in their postcondition. After reduction,the intermediate state is no longer present, so we lose those index variablesfrom the postconditions.For example, (t.const c) drop could be typed as ; l; φ→ ; l; φ, (t a), (=a (t c)) where a represent the value on the stack t.const c. This would reduceto , and then we lose the information about a in the postcondition indextype system. However, this can be solved using implication, as we know a isfresh from the Rule Const, and therefore we allow saying φ =⇒ φ, (t a), (=a (t c)) after reduction. This pattern will appear in any case of the proofthat consumes values.Lemma 11. Subject Reduction for CodeIf S; (ti; l; φ)? ` v∗; e∗ : ti; l; φ, ` s : S, (we omit this on rules that do notuse the store) and s; v∗; e∗ ↪→ s′; v′∗; e′∗, then S; (ti; l; φ)? ` v′∗; e′∗ : ti; l; φ,and ` s′ : S (we omit this on rules that do not change the store)Proof. By induction on reduction.Most proof cases are omitted, the complete proof can be found in theappendix ( B.2).72• Case: S; (ti∗; l; φ)?`i vj1 (t.const c) vk2 ; (t.const c′) (set local j): ti∗; l; φ∧ vj1 (t.const c) vk2 ; (t.const c′) set local j ↪→ vj1 (t.const c′) vk2 ; We want to show thatS; (ti∗; l; φ)? `i vj1 (t.const c′) vk2 ; (t.const c′) (set local j) : ti∗; l; φWe know ` (t.const c) : (t a); (◦, (t a), (= a (t c))), S; Sinst(i) `(t.const c′) (set local j) :  : l1; φj1, (◦, (t a), (= a (t c))), φk2 → ti∗; l; φ,and l1(j) = (t a), and Clocal(j) = t because they are premises of RuleCode that we have assumed to hold.By Lemma Inversion on Rule Composition, S; Sinst(i) ` (t.const c′) :; l1; φj1, (◦, (t a), (= a (t c))), φk2 → ti∗3; l3; φ3, S; Sinst(i) ` set local j :ti∗3; l3; φ3 → ti∗; l; φ.Recall that t = Clocal(j), then by Lemma Inversion on Rule Set-Local we have ti∗3 = ti∗ (t a′), l = l3[j := (t a′)], and φ3 =⇒ φ.Then, by Lemma Inversion on Rule Const, ti∗ = , l1 = l3, andφj1, (◦, (t a), (= a (t c))), φk2, (t a′), (= a′ (t c′)) =⇒ φ3.Now we have all the information we need to derive the same type for(t.const c′)We have S; Sinst(i) `  : ; l; φ→ ; l; φ by Rule Empty.Then, S; Sinst(i) `  : ; l; φj1, (◦, (t a), (= a (t c))), φk2, (t a′), (=a′ (t c′))→ ; l; φ by Rule Subtyping.Since a is fresh, φj1, φk2, (t a′), (= a′ (t c′)) =⇒ φj1, (◦, (t a), (=a (t c))), φk2, (t a′), (= a′ (t c′)).Then, S; Sinst(i) `  : ; l; φj1, φk2, (t a′), (= a′ (t c′)) → ; l; φ by RuleSubtyping.Further, ` (t.const c′) : (t a′); ◦, (t a′), (= a′ (t c′)) by Rule Admin-Const.Therefore, S; (ti∗; l; φ)? `i vj1 (t.const c′) vk2 ;  : ti∗; l; φ by Rule Code.73• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.load align o) : ti∗; l; φ∧ s; (i32.const k) (t.load align o) ↪→i t.const constt(b∗),where smem(i, k + o, |t|) = b∗We want to show that S; (ti∗; l; φ)? `i v∗; (t.const constt(b∗)) : ti∗; l; φWe know (` v : tiv; φv)∗ and S; C ` (i32.const k) (t.load align o) :; ti∗v; φ∗v → ti∗; l; φ because they are premises of Rule Code which wehave assumed to hold.Then, by Lemma Inversion on Rule Composition, Rule Const,Rule Mem-Load, we know ti∗ = (t a), ti∗v = l, and φ∗v, (t a) =⇒ φ.We haveS; Sinst(i)` t.const constt(b∗): ; ti∗v; φ∗v → (t a); l; φ∗v, (t a), (= a (t c))by Rule Const.Then, S; Sinst(i) ` (t.const constt(b∗)) : ; ti∗v; φ∗v → (t a); l; φ by RuleSubtyping.Recall (` v : tiv; φv)∗, then S; (ti∗; l; φ)? `i v∗; t.const constt(b∗) :ti∗; l; φ by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.const c) (t.store align o) :ti∗; l; φ∧ s; (i32.const k) (t.const c) (t.store align o) ↪→i s′; , where s′ =s with mem(i, k + o, |t|) = bits|t|t (c)We know (` v : tiv; φv)∗ andS; Sinst(i)` (i32.const k) (t.const c) (t.store align o): ; ti∗v; φ∗v → ti∗; l; φbecause they are premises of Rule Code which we have assumed tohold.Then, by Lemma Inversion on Rule Composition, Rule Const,74and Rule Mem-Store, we have ti∗ = , tiv = l, and φ∗v, (i32 a1), (=a1 (i32 k)), (t a2), (= a2 (t c)) =⇒ φ.Since a1 and a2 are fresh, φ∗v =⇒ φ.We have S; Sinst(i) `  : ; l; φ∗v → ; l; φ∗v by Rule Empty.Then, S; Sinst(i) `  : ; tiv; φ∗v → ; l; φ by Rule Subtyping.Recall that (` v : tiv; φv)∗. Therefore, S; (ti∗; l; φ)? `i v∗;  : ti∗; l; φby Rule Code.Now we must ensure that the new store s′ is well typed: ` s′ : S.Recall ` s : S, then Smem(i) = n and smem(i) = b∗ where n ≤ |b∗|because it’s a premise of Rule Store.Since s′ = s with mem(i, k + o, |t|) = bits|t|t (c), then |s′textmem(i) |=|stextmem(i)|, and therefore n ≤ |s′textmem(i)|, so s′ : S by RuleStore.• Otherwise: we have (` (t.const c) : (t a); (◦, (t a), (= a (t c))))∗, andS, Sinst(i) ` e∗ : ; (t a)∗; (◦, (t a), (= a (t c)))∗ → ti; l; φBy Lemma Subject Reduction Without Effects, we haveS, Sinst(i) ` e′∗ : ; (t a)∗; (◦, (t a), (= a (t c)))∗ → ti; l; φ.Then, S; (ti∗; l; φ)? ` v∗; e′∗ : ti; l; φLemma Subject Reduction Without Effects is used in the subjectreduction proof to separate out cases that do not modify state since itsimplifies the reasoning. Further, by separating these cases, we can abstractout the common pattern of building back up to Rule Program from theinstruction typing judgment S; C ` tfi. To avoid needing to do mutualinversion, we do not include the local block case here. We do not include anyinstructions here that modify state, such as set local or storeprechk , meaningthat this is non-exhaustive. That is on purpose because we are using thislemma to handle simple cases, and more complex cases are handled separately.We show that if a sequence of instructions e∗ reduces to another sequence of75instructions e′∗, and the reduction does not modify the program state (thestore s or the locals v∗), then e′∗ has the same precondition ti∗1; l1; φ1 andpostcondition ti∗2; l2; φ2 as e∗.Lemma 12. Subject Reduction Without EffectsIf S; C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,` s : S (note: we omit this for cases which do not use s),and s; v∗; e∗ ↪→ s; v∗; e′∗,then S; C ` e′∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2Proof. By case analysis on the reduction rules.Most proof cases are omitted, the complete proof can be found in theappendix ( B.2).• S; C ` L0[trap] : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ L0[trap] ↪→ trapThis case is trivial since trap accepts any precondition and postcondition.Thus, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• S; C ` (t.const c1) (t.const c2) t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) t.binop ↪→ t.const c where c = binop(c1, c2)We want to show that S; C ` t.const c : ti∗1; l1; φ1 → ti∗2; l2; φ2.We begin by reasoning about the type of the original instructions(t.const c1) (t.const c2) t.binopBy Lemma Inversion on Rule Composition, Rule Const, and RuleBinop, we know that ti∗2 = ti∗1(t a3), l2 = l1, and thatφ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(t a3), (= a3 (binop a1 a2))=⇒ φ2Now we will show that t.const c has the appropriate type.By const, S; C ` t.const c : ; l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (t c)).76Because c = binopt(c1, c2), then by =⇒ ,φ1, (t a), (= a (t c)) =⇒ φ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(t a3), (= a3 (binop a1a2))Therefore, S; C ` (t.const c) : ti∗1; l1; φ1 → ti∗1 (t a3); l1; φ2, by RuleStack-Poly and Rule Subtyping.• C ` (t.const c1) (t.const c2) t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) t.binop ↪→ trapThis case is trivial since trap accepts any precondition and postcondition.Thus, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• Case: S; C ` (t.const c1) (t.const c2) (i32.const 0) select: ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) (i32.const 0) select ↪→ (t.const c2)We want to show that S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗2; l2; φ2.First, we reason about what the original type must look like.By Lemma Inversion on Rule Composition, Rule Const, and RuleSelect, we know that ti∗2 = ti∗1 (a3 ), l2 = l1, andφ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(i32 a), (= a (i32 0)),(t a3), (if (= a (i32 0)) (= a3 a2) (= a3 a1))=⇒ φ2Now we show that (t.const c2) has the appropriate type.By Rule Const,C ` (t.const c2) : ; l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (t c2))77Then, S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗1 (t a3); l1; φ1, (t a3), (=a3 (t c2)) by Rule Stack-Poly.By =⇒ , we haveφ1, (t a3), (= a3 (t c2)) =⇒ φ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(i32 a), (= a (i32 0)),(t a3), (if (= a (i32 0))(= a3 a2)(= a3 a1))Therefore, S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗2 (t a3); l1; φ2 by sub −typing• Case: S; C ` (t.const c)n block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end :ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c)n block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end↪→ labelm{} (t.const c)n e∗ endWe want to show that labelm{} (t.const c)n e∗ end : ti∗1; l1; φ1 →ti∗2; l2; φ2.First, we reason about ti∗1; l1; φ1 → ti∗2; l2; φ2.We know S; C` block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end: ti∗1 (t a)n; l1; φ1, (t a)n, (= a (t c))n → ti∗2; l2; φ2by Lemma Inversion on Rule Composition and Rule Const.By Lemma Inversion on Rule Block, l1 = l3 and l2 = l4. We willuse l1, l2 in place of l3, l4, respectively, for the remainder of the case.Then, S; C, label(tm4 ; l2; φ4) ` e∗ : (t a)n; l1; φ3 → tim4 ; l2; φ4 becauseit is a premise of Rule Block which we have already assumed to hold.Also, (t a)n = tin3 , ti∗2 = ti∗1 tim4 , φ1, (t a)n, (= a (t c))n =⇒ φ3, andφ4 =⇒ φ2 by Lemma Inversion on Rule Block.Now we have all the information we need to show thatlabelm{} (t.const c)n e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2.78Remember that Rule Label uses the types of both the body(t.const c)n e∗ and the stored instructions .First, we show the type of the body.We haveS; C, label(tm4 ; l2; φ4) ` (t.const c)n : ; l1; φ1→ (t a)n; l1; φ1, (t a)n, (= a (t c))nby Rule Const.Then, since φ1, (t a)n, (= a (t c))n =⇒ φ3, we haveS; C, label(tn3 ; l1; φ3) ` (t.const c)n : ; l1; φ1 → (t a)n; l1; φ3by Rule Subtyping.Recall we have S; C, label(tm4 ; l2; φ4) ` e∗ : (t a)n; l1; φ3 → tim4 ; l2; φ4.Then S; C, label(tm4 ; l2; φ4) ` (t.const c)n e∗ : ; l1; φ1 → tim4 ; l2; φ4 byRule Composition.We have the type we want from the body. Now we get the type wewant of the stored instructions. We already have the postcondition wewant, tm4 ; l2; φ4, in the label stack, so we want the stored instructionto just pass the information through. Since the stored instructions is ,this is simple to show: we have S; C `  : tim2 ; l2; φ4 → tim2 ; l2; φ4 byRule Empty and Rule Stack-Poly.Therefore, C ` labelm{} (t.const c)n e∗ end : ; l1; φ1 → tim2 ; l2; φ4 bylabel.Finally, since φ4 =⇒ φ2, S; C ` labelm{} (t.const c)n e∗ end :ti∗1; l1; φ1 → ti∗1 tim4 ; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` labeln{e∗} Lj [(t.const c)n (br j)] end : ti∗1; l1; φ1 →ti∗2; l2; φ2∧ labeln{e∗} Lj [(t.const c)n (br j)] ↪→ (t.const c)n e∗We want to show that vn e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2.79Intuitively, this proof works because the premise of Rule Br assumesthat Clabel(i) is the precondition (tin1 ; l3; φ5, as we will soon see) of thestored instructions e∗ in the i + 1th label, and the postcondition ofthe label block is immediately reachable from the postcondition of e∗.Meanwhile, that assumptions is ensured by Rule Label, which ensuresthat e∗ has the same precondition as the i+1th branch postcondition onthe label stack and the same postcondition as the label block instruction.By Lemma Inversion on Rule Label, ti∗2 = ti∗1 ti∗4 for some ti∗4.Also, S; C, label(tin1 ; l3; φ5)j ` (t.const c)n (br j) : ; l3; φ3 → ti∗∅; l∅; φ∅for some l3 and φ3, where φ5 = φ3, (t a)n, (= a (t c))n, by LemmaInversion on Rule Label and Rule Br.Then, S; C, label(tin1 ; l3; φ5)j ` (br j) : tin1 ; l3; φ5 → ti∗∅; l∅; φ∅, byLemma Inversion on Rule Composition and Rule Const.Then, S; C, label(tin1 ; l3; φ5)j ` (t.const c)n : ; l3; φ3 → tin1 ; l3; φ5since it is a premise of composition which we have assumed to hold.Further, S; C ` e∗ : tin1 ; l3; φ5 → ti∗2; l2; φ4 since it is a premise of RuleLabel which we have assumed to hold, and φ4 =⇒ φ2 by LemmaInversion on Rule Label.Then, S; C ` (t.const c)n e∗ : ; l1; φ1 → ti∗2; l2; φ4 by Lemma Lift-Consts and Rule Composition.Finally, C ` (t.const c)n e∗ : ti∗1; l1; φ1 → ti∗1 ti∗4; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` (i32.const j) call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4: ti∗1; l1; φ1 → ti∗2; l2; φ2∧ s; (i32.const j) call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4 ↪→i call stab(i, j)where stab(i, j)code = (func tfi0 local t∗ e∗) and tfi0 <: ti∗3; l3; φ3 →ti∗4; l4; φ4We want to show that call stab(i, j) : ti∗1; l1; φ1 → ti∗2; l2; φ2.By Lemma Inversion on Rule Composition, Rule Const, and RuleCall-Indirect, we know that ti∗1 = ti∗0 ti∗3 and ti∗2 = ti∗0 ti∗4 for some80ti∗0, l1 = l)2, φ1 =⇒ φ3, and φ4 =⇒ φ2.We know S ` stab(i, j) : tfi0 since it is a premise of ` s : S which wehave assumed to hold.Then, S; C ` call stab(i, j) : tfi0 by Rule Call-Cl.S; C ` call stab(i, j) : ti∗3; l1; φ3 → ti∗4; l2; φ4 by Rule Subtyping.Therefore, S; C ` call stab(i, j) : ti∗0 ti∗1; l1; φ1 → ti∗0 ti∗1; l2; φ2 by RuleStack-Poly.4.3.2 ProgressProgress ensures that if a program is well typed then it either: entirely consistsof values, traps, or is reducible (i.e., there exists another program that itreduces to). Proving progress for Wasm-prechk is the key metatheoreticproperty that ensures that our claim that Wasm-prechk is as safe as Wasm isvalid. This is because it connects the static guarantees of the type systemto the dynamic assumptions of prechk-tagged instructions. By proving thatwell-typed prechk-tagged instructions will always be reducible, we prove thatthe static guarantees are sufficient to ensure that they will not trap andtherefore the dynamic checks are unnecessary.Since most Wasm-prechk instructions have the same semantics as inWasm, and every Wasm-prechk type includes all the information of a Wasmtype, we can reuse the Wasm proof for those instructions by using the erasurefunction from Section 4.2.2. The intuition for this is that the Wasm-prechkindexed type system provides strictly more information than the Wasm typesystem. However, for Wasm-prechk instructions that do not have the samesemantics as in Wasm, specifically prechk-tagged instructions, we still mustprove those cases.Theorem 4. Progress If `i s; v∗; e∗ : ti∗; l; φ then either e∗ = v′∗, e∗ = trap,or s; v∗; e∗ ↪→i s′; v′∗; e′∗.Proof. We proceed by induction on `i s; v∗; e∗ : ti∗; l; φ.81Because `i s; v∗; e∗ : ti∗; l; φ, we know that ` s : S for some S, and thatS;  `i v∗; e∗ : ti∗; l; φ because they are premises of Rule Program whichwe have assumed to hold.Then we know that (` v : (tv av); φv)∗ and S; Sinst(i), local t∗v ` e∗ :; (tv av)∗; φ∗v → ti∗; l; φ because they are premises of Rule Code which wehave assumed to hold.• Case: `i s; v∗; (t.const c1) (t.const c2) t.divprechkWe must show that (t.const c1) (t.const c2) t.divprechk ↪→ e′∗ for somee′∗.We have S; () `i v∗; (t.const c1) (t.const c2) t.divprechk : ti∗; l; φ forsome ti∗, l, and φ because it is a premise of Rule Program which wehave assumed to hold.Then, (` v : (tv av); φv)∗ for some (tv av)∗ and φ∗v, since it is a premiseof Rule Code which we have assumed to hold.It is important to note that φ∗v cannot contain a contradiction becauseit contains a single equality constraint per fresh index variable (seeRule Admin-Const).Further,S; Sinst(i), local t∗v ` (t.const c1) (t.const c2) t.divprechk: ; (tv av)∗); φ∗v → ti∗; l; φbecause it too is a premise of Rule Code.Then,Sinst(i)` (t.const c1) (t.const c2): ; (tv av)∗); φ∗v→ (t a1) (t a2); (tv av)∗); φ∗v, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2))where φ∗v, (t a1), (= a1 (t c1)), (t a2), (= a2 (t c2)) =⇒ ¬(= a2 (t 0))by Lemma Inversion on Rule Composition and Rule Div-Prechk.82Therefore, it must be the case that c2 6= 0, and therefore there mustexist some c3 such that c3 = div(c1, c2) since div(c1, c2) is well-definedwhen c2 is non-zero. Then, s; (t.const c1) (t.const c2) t.divprechk ↪→i(t.const c3).• Case: `i s; v∗; (i32.const k) (t.loadprechk (tp_sx) align o)We must show that s; (i32.const k) (t.loadprechk (tp_sx) align o) ↪→ e′∗for some e′∗.We have S;  `i v∗; (i32.const k) (t.loadprechk (tp_sx) align o) : ti∗; l; φfor some ti∗, l, and φ because it is a premise of Rule Program whichwe have assumed to hold.We also have that ` s : S, and therefore (n ≤ |b∗|)∗ where Stab = n∗and smem = (b∗)∗.Then, (` v : (tv av); φv)∗ for some (tv av)∗ and φ∗v, since it is a premiseof Rule Code which we have assumed to hold.It is important to note that φ∗v cannot contain a contradiction becauseit contains a single equality constraint per fresh index variable (seeRule Admin-Const).Further, we have thatS; Sinst(i), local t∗v ` (i32.const k) (t.loadprechk (tp_sx) align o): ; (tv av)∗; φ∗v → ti∗; l; φbecause it too is a premise of Rule Code.Then,Sinst(i) ` (i32.const k) : ; (tv av)∗; φ∗v→ (i32 a); (tv av)∗; φ∗v, (i32 a), (= a (i32 k))83whereφ∗v, (i32 a), (= a (i32 k)) =⇒ (ge (add a (i32 o))(i32 0)),(le (add a (add (i32 o+ width)))(i32 n2 ∗ 64Ki))and n2 ∗ 64Ki = Smem(i, j) by Lemma Inversion on Rule Composi-tion and Rule Store-Prechk.Because we haveφ∗v, (i32 a), (= a (i32 k)) =⇒ (ge (add a (i32 o))(i32 0)),(le (add a (add (i32 o+ width)))(i32 n2 ∗ 64Ki)), then we must have k + o ≥ 0 and k + o+ |tp| ≤ n2 ∗ 64Ki.Recall ` s : S. Then, since n2 ∗64Ki = Smem(i, j), we have smem(i, j) =b∗2 where n2 ∗ 64Ki ≤ |b∗2|.Therefore, it must be the case that k + o ≥ 0 and k + o+ |tp| < |b∗2|,and therefore smem(i, k + o, |tp|) = b∗3 for some b∗3 that is a subse-quence of b∗2. Then, s; (i32.const k) (t.loadprechk (tp_sx) align o) ↪→it.const constsxt (b∗3).• Case: `i s; v∗; (i32.const k) t.loadprechk align oSame as above, except with |t| replacing |tp| and constt(b∗3) instead ofconstsxt (b∗3).• Case: `i s; v∗; (i32.const k) (t.const c) (t.storeprechk tp align o)We must show that s; (i32.const k) (t.storeprechk tp align o) ↪→ e′∗ forsome e′∗.We haveS; () `i v∗; (i32.const k) (t.storeprechk (tp_sx) align o) : ti∗; l; φ84for some ti∗, l, and φ because it is a premise of Rule Program whichwe have assumed to hold.We also have that ` s : S, and therefore (n ≤ |b∗|)∗ where Stab = n∗and smem = (b∗)∗.Then, (` v : (tv av); φv)∗ for some (tv av)∗ and φ∗v, since it is a premiseof Rule Code which we have assumed to hold.It is important to note that φ∗v cannot contain a contradiction becauseit contains a single equality constraint per fresh index variable (seeRule Admin-Const).Further, we have thatS; Sinst(i), local t∗v ` (i32.const k) (t.storeprechk tp align o): ; (tv av)∗; φ∗v → ti∗; l; φbecause it too is a premise of Rule Code.Then,Sinst(i) ` (i32.const k) (t.const c) :; (tv av)∗; φ∗v→ (i32 a) (t a2); (tv av)∗; φ∗v, (i32 a), (= a (i32 k)),(t a2), (= a2 (t c))whereφ∗v, (i32 a), (= a (i32 k)),(t a2), (= a2 (t c))=⇒ (ge (add a (i32 o))(i32 0)),(le (add a (add (i32 o+ width)))(i32 n2 ∗ 64Ki))and n2 ∗ 64Ki = Smem(i, j) by Lemma Inversion on Rule Composi-tion and Rule Load-Prechk.85Because we have(i32 a), (= a (i32 k)),(t a2), (= a2 (t c))=⇒ (ge (add a (i32 o))(i32 0)),(le (add a (add (i32 o+ width)))(i32 n2 ∗ 64Ki)), then we must have k + o ≥ 0 and k + o+ |tp| ≤ n2 ∗ 64Ki.Recall ` s : S. Then, since n2 ∗64Ki = Smem(i, j), we have smem(i, j) =b∗2 where n2 ∗ 64Ki ≤ |b∗2|.It must be the case that k+ o ≥ 0 and k+ o+ |tp| < |b∗2|, and thereforesmem(i, k + 0, |tp|) = b∗3 for some b∗3 that is a subsequence of b∗2 Then,we can construct s′ = s with s′mem(i, k + o, |tp|) = bits|tp|t (c) because|bits|tp|t (c) |= |b∗3|. Then,s; (i32.const k) (i32.const c) (t.storeprechk tp align o) ↪→i s′; • Case: `i s; v∗; (i32.const c) (t.storeprechk align o)Same as above, except with |t| replacing |tp|.• Case: `i (i32.const c) call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2We must show that (i32.const c) call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2 ↪→e′∗ for some e′∗.We have S; () `i v∗; (i32.const c) call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2 :ti∗; l; φ for some ti∗, l, and φ because it is a premise of Rule Programwhich we have assumed to hold.We also have that ` s : S, and therefore Stab(i) = (n, tfin) and(S ` cl : tfi)∗ where stab(i) = cl∗ and n ≤ |cl∗|.Then, (` v : (tv av); φv)∗ for some (tv av)∗ and φ∗v, since it is a premiseof Rule Code which we have assumed to hold.It is important to note that φ∗v cannot contain a contradiction becauseit contains a single equality constraint per fresh index variable (seeRule Admin-Const).86Then,Sinst(i) ` (i32.const c) :; (tv av)∗; φ∗v→ (i32 a); (tv av)∗; φ∗v, (i32 a), (= a (i32 c))where φ∗v, (i32 a), (= a (i32 c)) =⇒ (gt n a) ∧ (le (i32 0) a) by LemmaInversion on Rule Composition and Rule Call-Indirect-Prechk.We have∀i. (φ =⇒ ¬(= (i32 i) a)) ∨ tfis(i) <: ti∗1; l1; φ1 → ti∗2; l2; φ2where tfis = tfin, because it is a premise of Rule Call-Indirect-Prechk which we have assumed to hold by Lemma Inversion. Since(i32 a); (tv av)∗; φ∗v, (i32 a), (= a (i32 c)) =⇒ (= (i32 c) a), then it hasto be the case that tfis(c) <: ti∗1; l1; φ1 → ti∗2; l2; φ2.Let, {inst j, func f} = stab(i, c). Recall from before that (S ` cl : tfi)∗.Then, S ` {inst j, func f} : tfi2 for some tfi2.Sinst(j) ` f : tfi2, as it is a premise of S ` {inst j, func f} : tfi2.Then, we know that f = func tfi2 local . . . because it is a premise ofSinst(j) ` f : tfi2, and we know that tfi2 <: ti∗1; l1; φ1 → ti∗2; l2; φ2.Thus, s; (i32.const c) call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2↪→ call {inst j, func f}.• Otherwise, we reuse the Wasm proof, which we can do thanks toTheorem 2.87Chapter 5ImplementationTo ensure the feasibility of implementing the Wasm-prechk language weimplemented a reference implementation 1 in Redex [2]. We were able tohandle the entirety of the type system and use the reference implementationto typecheck several test programs, including test programs for each prechk-tagged instruction, and negative results that ensure illegal prechk-taggedinstructions are not well-typed. Further, our reference implementation is ableto implement constraint solving and implication.5.1 Reference ImplementationWe developed the reference implementation of Wasm-prechk in Redex bycreating a reference implementation of Wasm and extending it with theWasm-prechk syntax and type system. This ensured that our model workson silicon and not just in set theory, and made it possible to quickly testout various approaches. The syntactic representation we used in the Redexmodel differs a bit from the syntactic representation provided here, as it iss-expression based.However, we have only implemented a typechecker in the Redex model.Thus, we must manually construct derivations and ask if they are valid. Thismay be solvable using a bi-directional type system approach, or by otherwise1https://zenodo.org/record/399511488coming up with a type inference algorithm.We implemented the static typing judgment (` C (e ...) tfi), wheree ... is Redex for e∗. Here is Rule Const in Redex. Note that it isessentially the same, minus a few syntactic differences.[(` C ((t const c))((() l φ)-> (((t a)) l ((φ (t a)) (= a (t c))))))]There is an extra set of parentheses around (t const c) because thejudgment works over sequences of instructions (e ...), where e ... =(t const c) here. Also, there’s no dot between the type t and the con-stant instruction keyword const because that is not necessary in Redex’ss-expressions.In the above example, there is no requirement about the freshness ofa. Redex does not support freshness requirements in judgments. However,because we use the typing judgment to check manually constructed derivations,we are simply careful in writing the derivations to ensure that this propertyis true.5.2 Constraint Solving in PracticeIn our implementation, we reason about constraints using the Z3 theoremprover [1].5.2.1 Translation of Constraints to Z3Constraint solving and implication involves translating various parts of theWasm-prechk index language into Z3 constraints. We use Z3 bitvectors torepresent index variables. Z3 bitvectors are integers with a fixed-width bitstring representation, like Wasm-prechk’s i32 and i64, that Z3 can reason aboutusing standard operations (addition, multiplication, shift left, etc...), andhandle overflow (which can occur in Wasm). Further, fixed-width bitvectorsare a finite domain that has more efficient reasoning and decidability comparedto the natural numbers. Since bitvectors have similar operations to the Wasm-89compilez3(x).= SMTa.= a(i32 c) .= (_ bvc 32)(i64 c) .= (_ bvc 64)(binop x y) .= (bvbinop compilez3(x) compilez3(y))(relop x y) .= (bvrelop compilez3(x) compilez3(y))compilez3(P ).= SMT(= x y).= (= compilez3(x) compilez3(y))(ifP1 P2 P3).= (ite compilez3(P1) compilez3(P2) compilez3(P3))¬P .= (not compilez3(P ))P1 ∧ P2 .= (and compilez3(P1) compilez3(P2))P1 ∨ P2 .= (or compilez3(P1) compilez3(P2))compilez3((t a)).= SMT(i32 a) .= (declare-const a (_BitVector32))(i64 a) .= (declare-const a (_BitVector64))Figure 5.1: Translation of Wasm-prechk Index Language to Z3prechk index language, translating an index x to Z3 only requires changingthe name of operations (for example, add becomes bv_add). Translatingpropositions to Z3 is also straightforward because Z3 has support for all ofthe first-order logic constructs we use to build and combine propositions.To test whether the satisfiability of one index type context φ1 implies thatsome other index type context φ2 is satisfiable, we first generate bitvectors torepresent all of the index variables. Z3 constraints are generated based on thepropositions in both contexts. We assert that the constraints generated forthe first context must hold. Finally, we ask Z3 to find an assignment to thevariables declared in the type index contexts where the constraints from thesecond context do not hold (a counterexample). If a counterexample cannotbe found, then the implication must hold, otherwise, it does not hold.90(declare-const a (_ BitVec 32))(declare-const b (_ BitVec 32))(declare-const c (_ BitVec 32))(declare-const d (_ BitVec 32))(define-fun satisfies () Bool(=> (and (= c (_ bv1 32))(ite (= b (_ bv0 32))(= d c)(= d b))(and (not (= d (_ bv0 32))))))(assert (not satisfies ))(check-sat)(get-model)Figure 5.2: Example of a Z3 query for constraint satisfactionWe define the translations for certain parts of the index language to SMT(the Z3 constraint language) used in the reference interpreter in Figure 5.1.One key thing to note in the translation is that we use a slightly differentrepresentation of relop and testop within the reference implementation. Withrelop, the Z3 versions of the Wasm-prechk index language relation operatorsreturns booleans, not bitvectors, so we convert every use of relop from(= a (relop x y)) to(if (= (t 1) (relop x y)) (= a (t 1)) (= a (t 0))), where t is the primitive Wasm type of a from the type declaration of a inφ. We do the same for testop, except we first convert (eqz x) (the only testoperator) to (= (t 0) x), so then (= a (eqz x)) becomes(if (= (t 0) x) (= a (t 1)) (= a (t 0)))We also include an example of a complete Z3 query in Figure 5.2. It isthe Z3 query for testing the implication in the divprechk rule in the examplein section 3.3.2.91How we implement the table in Z3 Recall from subsection 3.3.2 thatfor call indirectprechk tfi, we have to reason about which functions in a tablecan be called. In practice, we construct a Z3 array (intuitively similar to anormal array) that is the same size as the table (we chose Z3 arrays becausethey have a similar abstraction to tables). We fill the array with booleanvalues, which are true if the function at the table index is a suitable functiontype (a subtype of the expected type tfi), and false otherwise. Finally, weassert all of the translated constraints from the index type context about thetable index, and then make sure that reading from the array using the tableindex returns true. We do not show here how we generate Z3 constraints fortables, but it can be found in the Redex model.5.2.2 Impact of Using Z3Our choice of using Z3 has impacted Wasm-prechk in several ways.Floating Point Values and Integer Bit Operations We currently donot support floating point values because Z3 is unable to reason about them.In addition, the Wasm unary operators (ctz, clz, and popcnt, which providebit-level information) and certain binary operators (rotr and rotl) would bedifficult and inefficient to reason about using Z3 due to their non-linearity, sowe do not currently support them in Wasm-prechk. However, we treat theseoperators (and floating point values), like memory operations and simplyassume nothing about them.Type Annotations in Constraints The requirement of adding explicittype annotations for index variables and constants that appear in type indicescomes from needing to know what width the variable will be when we convertit to a Z3 bitvector. Without these type annotations, we would not knowwhether a constant c should be represented using a 32-bit or 64-bit vector(depending on if it is an i32 or i64).Performance Concerns There are performance concerns when using anSMT solver. Our small examples programs have been near instantaneous to92typecheck (usually involving only one Z3 invocation with a few constraints).For example, the query in Figure 5.2, is very small and takes millisecondsto run. However, it is likely that we will see a slowdown due to significantlylarger constraint sets when typechecking large Wasm programs. This wouldrequire a clever approach to reducing the size of the constraint set (perhapsusing a form of type-level garbage collection on constraints on index variablesthat cannot be referred to). Also, we would want to make sure when writing atypechecker/synthesizer that we invoke Z3 as little as possible, by minimizingthe amount of reasoning we do about the constraints.93Chapter 6DiscussionBy creating Wasm-prechk, we have taken the first step towards creating apractical system in which an expressive type system is used with an existingand widely low-level language for safety and performance. Wasm-prechkprovides concrete ways to use type information for compiler optimization atthe assembly language level. This is a first step in the sense that it providesthe scaffolding to build such a system that could be part of the infrastructureof the internet: unlike prior work, it is backwards compatible with a commonlyused language, Wasm, supported by many major browsers. However, thereare still a number of unanswered questions. We have a number of futureideas for this work some based on what we think is necessary to realize oureventual goal of making Wasm-prechk practical in the real-world, and othersbased on problems identified during the course of the project so far.Support for Streaming Compilation The format of Wasm code allowscompilation and execution to begin with only part of the program downloaded.Similar streaming compilation is theoretically possible with Wasm-prechk,but there are unanswered questions about how to perform typechecking insuch a compilation pipeline. Here are two examples of problems that weexpect to face implementing such a system. First of all, we must make suresuch a system is safe, which is complicated by the fact that we may beginexecuting code before we have finished typechecking. This should not be94too much of an issue as long as we ensure code is typechecked before we canexecute it, so we only execute well-typed code and if we come across codethat is not well typed we halt execution and throw a type error. Second of all,this will require highly efficient typechecking, preferably performed in parallelto typecheck many functions at one. We could also try to be clever andprioritize typechecking on functions that we expect to be executed sooner.More Optimizations There is the potential to find other optimizationswe can perform with the additional type information. For example, rememberfrom section 3.3 that an if may have a contradiction in the index type contextin one of its branches. In this case, that branch will never be executed, andtherefore the other branch must always be taken, so we can safely replace theif instruction with the other branch. We can do similar optimizations withbr if and select.6.1 Future WorkEmpirical Evaluation The first step would involve testing the actualperformance costs of dynamic checks. We could then implement a type-checker and compiler for Wasm-prechk so we are able to perform experimentsand measure the real performance benefit provided by Wasm-prechk. Thiswould allow us to empirically test whether Wasm-prechk actually improvesperformance. Our plan is to implement Wasm-prechk in Rust building onthe CraneLift compilier.Better Type Annotations in Embedding Recall that the embedding ofWasm into Wasm-prechk from subsection 4.2.1 does not take advantage of thepossibility of using type annotations on functions and blocks to check strongerguarantees about programs. This means that we could potentially missopportunities to remove dynamic checks by using prechk-tagged instructionsbecause we have less type information to work with. Type annotations can beadded by the developer, who will then get stronger guarantees of correctnessalong with the potential for more optimizations. However, we would prefer95for the developer not to have to hand-annotate compiled Wasm. Instead,we could use static analysis to try to find the weakest preconditions thatguarantee the safety of prechk-tagging instructions. We could also attempt tohave have a compiler from a higher-level language to Wasm add annotationsas a form of type preserving compilation similar to System F to TypedAssembly Language [5].6.2 LimitationsReasoning About Global Variables Reasoning about global variables ismade difficult because static typechecking is restricted to within the modulewe are checking, this restricts the reasoning ability of Wasm-prechk and againcould cause us to miss opportunities for optimizations. Thus, it is difficultto reason about global variables imported from another module. Concretely,imagine, in the jth module calling a function f that was imported fromthe ith module. The call instruction will be reduced to call {inst i, func f}where i is the module index for the module instance where f is defined.Theoretically, f should not change the global variables in the jth module.However, it may call a function in the jth module which could change theglobals in the jth module, and since we do not know what the behaviorof f is statically within j, we have to assume the worst and can make noassumptions about the global variables after f returns.Handling the Dynamic Resizing of Memory While linear memorychunks are initialized with a static size, Wasm allows dynamically growingmemory using the grow memory instruction. Currently, Wasm-prechk onlysupports typechecking prechk-tagged loads and stores based on the staticsize. It should be possible to reason about the size of memory being increasedby inserting a dependency on the result of the grow memory instruction. Ifthe result is −1, we know that the memory remains the same size. Otherwise,the result will be equal to the new memory size. This would require moredependency in the type system then we currently have with indexed types,since static type values would depend on dynamic control flow.96Chapter 7ConclusionWe have introduced Wasm-prechk, a low-level language that uses an expres-sive type system to potentially improve performance via the elimination ofunnecessary run-time checks. Wasm-prechk is based on Wasm, an existingreal-world language commonly used in performance-critical and untrustedcontexts, where both safety and performance are critical. To ensure thesafety of Wasm-prechk, we have proven the type safety of the Wasm-prechklanguage as well as showing a sound type erasure to Wasm, demonstrat-ing that Wasm-prechk is at least as safe as Wasm. We have shown thatan indexed type system can be used in a low-level language to reduce thenumber of dynamic checks required, without sacrificing safety and securityguarantees or increasing the programmer’s proof burden. We built a referenceinterpreter for Wasm-prechk to demonstrate the practicality of implementinga typechecker for Wasm-prechk. This demonstrates the usefulness of usingexpressive type systems as a practical tool to improve performance and ensuresafety for low-level languages in real use cases.97Bibliography[1] L. De Moura and N. Bjørner. Z3: An efficient SMT solver. InProceedings of the Theory and Practice of Software, InternationalConference on Tools and Algorithms for the Construction and Analysis ofSystems (TACAS/ETAPS), 2008. URLhttps://dl.acm.org/doi/10.5555/1792734.1792766.[2] M. Felleisen, R. B. Findler, and M. Flatt. Semantics engineering withPLT Redex. 2009. URL https://redex.racket-lang.org/.[3] I. Goldberg, D. Wagner, R. Thomas, and E. A. Brewer. A secureenvironment for untrusted helper applications confining the Wily Hacker.In Proceedings of the Conference on USENIX Security Symposium,Focusing on Applications of Cryptography (SSYM), 1996. URLhttps://doi.org/10.5555/1267569.1267570.[4] A. Haas, A. Rossberg, D. L. Schuff, B. L. Titzer, M. Holman,D. Gohman, L. Wagner, A. Zakai, and J. F. Bastien. Bringing the webup to speed with WebAssembly. In Proceedings of the ACM SIGPLANConference on Programming Language Design and Implementation(PLDI), 2017. URL https://doi.org/10.1145/3062341.3062363.[5] J. G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F toTyped Assembly Language. ACM Transactions on ProgrammingLanguages and Systems, 21(3), 1999. URLhttps://doi.org/10.1145/319301.319345.[6] G. C. Necula. Proof-carrying code. In Proceedings of the ACMSIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages (POPL), POPL ’97, 1997. URLhttps://doi.org/10.1145/263699.263712.[7] C. Reis, A. Moshchuk, and N. Oskov. Site isolation: Process separationfor web sites within the browser. In USENIX Security Symposium98(USENIX Security), 2019. URL https://www.usenix.org/conference/usenixsecurity19/presentation/reis.[8] D. Tarditi, J. G. Morrisett, P. Cheng, C. A. Stone, R. Harper, andP. Lee. TIL: A type-directed optimizing compiler for ML. In Proceedingsof the ACM SIGPLAN Conference on Programming Language Designand Implementation (PLDI), 1996. URLhttps://doi.org/10.1145/231379.231414.[9] H. Xi and R. Harper. A dependently typed assembly language. InProceedings of the ACM SIGPLAN International Conference onFunctional Programming (ICFP), 2001. URLhttps://doi.org/10.1145/507635.507657.99Appendix AComplete Wasm-prechk TypingJudgment Definitiontfi <: tfiφ0 =⇒ φ1 φ2 =⇒ φ3ti∗1; l1; φ1 → ti∗2; l2; φ2 <: ti∗1; l1; φ0 → ti∗2; l2; φ3Implies100C ` e∗ : tfiC ` unreachable : ti∗1; l1; φ1 → ti∗2; l2; φ2UnreachableC ` nop : ; l; φ→ ; l; φNopC ` drop : (t a); l; φ→ ; l; φDropa 6∈ φC ` t.const c : ; l; φ→ (t a); l; φ, (t a), (= a(t c))Consta3 6∈ φC ` t.binop : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖binop‖ a1 a2))Binopa3 6∈ φC ` t.testop : (t a1) l; φ→ (i32 a2); l; φ, (t a2), (= a2 (‖testop‖ a1))Testopa3 6∈ φC ` t.relop : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖relop‖ a1 a2))Relopa3 6∈ φC ` select : (t a1) (t a2) (i32 a); l; φ→ (t a3); l; φ, (t a3),(if (= a (i32 0)) (= a3 a2) (= a3 a1))SelectC2, label (ti∗2; l2; φ2) ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` block (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2Block101C2, label (ti∗1; l1; φ1)∗ ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` loop (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2LoopC2, label (ti∗2; l2; φ2) ` e∗1 : ti∗1; l1; φ1,¬(= a (i32 0))→ ti∗2; l2; φ2C2, label (ti∗2; l2; φ2) ` e∗2 : ti∗1; l1; φ1, (= a (i32 0)))→ ti∗2; l2; φ2C ` if (ti∗1; l1; φ1 → ti∗2; l2; φ2) e∗1 else e∗2 end : ti∗1; l1; φ1 → ti∗2; l2; φ2IfClabel(i) = ti∗; l1; φ1C ` br i : ti∗1 ti∗; l1; φ1 → ti∗2; l2; φ2BrCreturn = ti∗; l1; φ1C ` return : ti∗1 ti∗; l1; φ1 → ti∗2; l2; φ2ReturnClabel(i) = ti∗; l1; φ1,¬(= a (i32 0))C ` br if i : ti∗ a; l1; φ1 → ti∗; l1; φ1, (= a (i32 0))Br-If(Clabel(i) = ti∗; l1; φi)+ (φ1 =⇒ φi)nC ` br table i+ : ti∗1 ti∗ a; l1; φ1 → ti∗2; l2; φ2Br-TableCfunc(i) = ti∗1; l1; φ1 → ti∗2; l2; φ2C ` call i : ti∗1; l; φ1 → ti∗2; l; φ1, φ2CallCtable(i) = (j, tfi∗2)C ` call indirect ti∗1; l1; φ1 → ti∗2; l2; φ2: ti∗1 (i32 a); l; φ1 → ti∗2; l; φ1, φ2Call-IndirectClocal(i) = t l(i) = (t a) a2 6∈ φC ` get local i : ; l; φ→ (t a2); l; φ, (t a2), (= a2 a)Get-LocalClocal(i) = t l2 = l1[i := (t a)]C ` set local i : (t a); l1; φ→ ; l2; φSet-Local102Clocal(i) = t l2 = l1[i := (t a)] a2 6∈ φC ` tee local i : (t a); l1; φ→ (t a2); l2; φ, (t a2), (= a2 a)Tee-LocalCglobal(i) = mut? t a 6∈ φC ` get global i : ; l; φ→ (t a); l; φ, (t a)Get-GlobalCglobal(i) = mut tC ` set global i : (t a); l; φ→ ; l; φSet-GlobalCmemory = n 2align ≤ (|tp| <)?|t| a2 6∈ φC ` t.load (tp_sx)? align o : (i32 a1); l; φ→ (t a2); l; φ, (t a2)Mem-LoadCmemory = n 2align ≤ (|tp| <)?|t|C ` t.store tp? align o : (i32 a1) (t a2); l; φ→ ; l; φMem-StoreCmemory = n a 6∈ φC ` current memory : ; l; φ→ (i32 a); l; φ, (i32 a)Current-MemoryCmemory = n a2 6∈ φC ` grow memory : (i32 a1); l; φ→ (i32 a2); l; φ, (i32 a2)Grow-MemoryC `  : ; l; φ→ ; l; φEmptyC ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e∗ : ti∗ ti∗1; l1; φ1 → ti∗ ti∗2; l2; φ2Stack-Poly103C ` e∗1 : ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e2 : ti∗2; l2; φ2 → ti∗3; l3; φ3C ` e∗1 e2 : ti∗1; l1; φ1 → ti∗3; l3; φ3Compositionti∗1; l1; φ1 → ti∗2; l2; φ2 <: ti∗1; l1; φ0 → ti∗2; l2; φ3C ` e∗ → ti∗1; l1; φ1 → ti∗2; l2; φ2C ` e∗ → ti∗1; l1; φ0 → ti∗2; l2; φ3Subtypingφ =⇒ ¬(= a2 0) a3 6∈ φC ` t.divprechk : (t a1) (t a2); l; φ→ (t a3); l; φ, (t a3), (= a3 (‖div‖ a1 a2))Div-PrechkCmemory = n 2align ≤ (|tp| <)?|t| a3 6∈ φφ =⇒ (ge (add a1 (i32 o))(i32 0)),(le (add a1 (add (i32 o+ width))) (i32 n ∗ 64Ki))C ` t.loadprechk (tp_sx)? align o : (i32 a1); l; φ→ (t a2); l; φ, (t a2)Load-PrechkCmemory = n 2align ≤ (|tp| <)?|t|φ =⇒ (ge (add a1 (i32 o)) (i32 0)),(le (add a1 (add (i32 o+ width))) (i32 n ∗ 64Ki))C ` t.storeprechk tp? align o : (i32 a1) (t a2); l; φ→ ; l; φStore-PrechkCtable(i) = (n, (tfi2...))φ =⇒ (gt n a) ∧ (le (i32 0) a)tfis = (tfi2...) tfi = ti∗1; l1; φ1 → ti∗2; l2; φ2∀0 < i ≤ n. (φ =⇒ ¬(= (i32 i) a)) ∨ tfis(i) <: tfiC ` call indirectprechk tfi : ti∗1 (i32 a); l; φ1→ ti∗2; l; φ1, φ2Call-Indirect-Prechk104Appendix BMetatheory ProofsB.1 Sound Erasure ProofsLemma 13. Sound Static Typing ErasureIf C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,then eraseC(C) ` erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)Proof. We proceed by induction over typing derivations. Most proof casesare omitted as they are simple, but we provide a few to give an idea of whatthe proofs look like. Intuitively, we want to show that erasing the typingderivation produces a valid Wasm typing derivation.For most of the cases, the sequence of instructions e∗ contains only a singleinstruction e2, so we elide the step of turning erasee∗(e∗) into erasee∗(e2).• Case: C ` t.binop : (t a1) (t a2); l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (binop a1 a2))We want to show thateraseC(C) ` erasee∗(t.binop): erasetfi((t a1) (t a2); l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (binop a1 a2)))By the definition of erasee, we want to show that eraseC(C) ` t.binop :t t→ t is valid in Wasm.105Trivially, we have eraseC(C) ` t.binop : t t→ t by Rule Wasm-Binop,since Rule Wasm-Binop works under any module type context.• Case: C ` block (t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2e∗ end : (t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2We want to show thateraseC(C) ` erasee(block (t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2e∗ end : (t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2)By the definition of erasee and erasetfi (we also perform the step oferasing indexed function types here to avoid an extra step), we wantto show that eraseC(C) ` block t∗1 → t∗2e∗ end : t∗1 → t∗2 is a validWasm judgment.This proof is slightly more involved, since the derivation for this ruleincludes a premise thatC, label((t2 a2)∗; l2; φ2) ` e∗ : (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2By the inductive hypothesis for the well-typedness of e∗, we have thateraseC(C, label((t2 a2)∗; l2; φ2)) ` erasee∗(e∗): erasetfi((t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2)Then we have eraseC(C), label(t∗2) ` erasee∗(e∗) : t∗1 → t∗2 by definitionof eraseC and erasetfi.Now that we have satisfied the premise,eraseC(C) ` block t∗1 → t∗2e∗ end : t∗1 → t∗2106by Rule Wasm-Block.• Case: C ` br i : (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2We want to show thateraseC(C) ` erasee(br i): erasetfi((t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2)We have to reason about eraseC(C) because the typing judgment relieson the label stack from C.From C ` br i : (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2, we have thatClabel(i) = (t1 a1)∗; l1; φ1, since it is a premise.Then eraseC(C)label(i) = t∗1, by the definition of eraseC .eraseC(C) ` erasee(br i): erasetfi((t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2)= eraseC(C) ` br i : t∗1 → t∗2Recall that eraseC(C)label(i) = t∗1 → t∗2, then eraseC(C) ` br i : t∗1 →t∗2 by Rule Wasm-Br.• Case: C ` call i : (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2We want to show thateraseC(C) ` erasee(call i): erasetfi((t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2)We again have to reason about eraseC(C) because the typing judgmentrelies on the function type from C.From C ` call i : (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2, we have thatCfunc(i) = (t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2, since it is a premise.107Then, eraseC(C)func(i) = erasetfi((t1 a1)∗; l1; φ1 → (t2 a2)∗; l2; φ2) =t∗1 → t∗2, by the definition of eraseC .eraseC(C) ` erasee(call i): erasetfi((t1 a1)∗; l1; φ1→ (t2 a2)∗; l2; φ2)= eraseC(C) ` call i : t∗1 → t∗2Recall that eraseC(C)func(i) = t∗1 → t∗2.Then eraseC(C) ` call i : t∗1 → t∗2 by Rule Wasm-Call.• Case: C ` set local i : (t a); l1; φ1 → ; l1[i := a]; φ1We want to show thateraseC(C) ` erasee(set local i): erasetfi((t a); l1; φ1 → ; l1[i := a]; φ1)We again have to reason about eraseC(C) because the typing judgmentrelies on the local variable types from C.From C ` set local i : (t a); l1; φ1 → ; l1[i := a]; φ1, we have thatClocal(i) = t, since it is a premise.Then, we have that eraseC(C)local(i) = t, by the definition of eraseC .eraseC(C) ` erasee(set local i): erasetfi((t a)∗; l1; φ1→ ; l1[i := a]; φ1)= eraseC(C) ` set local i : t→ Recall that eraseC(C)local(i) = t → , then eraseC(C) ` set local i :t→  by Rule Wasm-Set-Local.• Case: C ` e∗1 e2 : (t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2108We want to show thateraseC(C) ` erasee(e∗1 e2): erasetfi((t1 a1)∗; l1; φ1 → (t2 a2); l2; φ2)For this typing rule, we must invoke the inductive hypothesis twice:one on the sequence e∗1 and once on the instruction e2. Then we mustshow that we can compose the erased subsequence together to get awell-typed sequence.We know that C ` e∗1 : (t1 a1)∗; l1; φ1 → (t3 a3); l3; φ3 and thatC ` e2 : (t3 a3)∗; l3; φ3 → (t2 a2); l2; φ2 because they are premieses ofRule Composition which we have assumed to hold.eraseC(C) ` erasee∗(e∗1) : erasetfi((t1 a1)∗; l1; φ1 → (t3 a3); l3; φ3) bythe inductive hypothesis on e∗1.eraseC(C) ` erasee∗(e∗1) : t∗1 → t∗3 by definition of erasetfi.eraseC(C) ` erasee∗(e2) : erasetfi((t3 a3)∗; l3; φ3 → (t2 a2); l2; φ2),by the inductive hypothesis on e2.eraseC(C) ` erasee∗(e∗2) : t∗3 → t∗2 by definition of erasetfi.eraseC(C) ` erasee∗(e∗1 e2): erasetfi((t1 a1)∗; l1; φ1→ (t2 a2); l2; φ2)= eraseC(C)` erasee∗(e∗1)erasee∗(e2): t∗1 → t∗2Recall that we have eraseC(C) ` erasee∗(e∗1) : t∗1 → t∗3 and thateraseC(C) ` erasee∗(e∗2) : t∗3 → t∗2 by definition of erasetfi.Then, eraseC(C) ` erasee∗(e∗1) erasee∗(e2) : t∗1 → t∗2 by Rule Wasm-Composition.Lemma 14. Sound Admin Typing Erasure109If S; C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,then eraseS(S); eraseC(C) ` erasee∗(e∗) : erasetfi(ti∗1; l1; φ1 → ti∗2; l2; φ2)Proof. We proceed by induction over typing rules. In addition to the priorcases from Lemma Sound Static Typing Erasure, which trivially stillhold since the value of S does not matter to those rules, we add proves for afew administrative typing rules, which may refer to S. Again, several proofcases are omitted as they are simple.• S; C ` labeln{e∗0} e∗ end : ; l1; φ1 → (t2 a2)n; l2; φ2We must show thateraseS(S); eraseC(C)` erasee∗(e∗0): erasetfi((t3 a3)∗; l3; φ3 → (t2 a2)n; l2; φ2)anderaseS(S); eraseC(C, label((t3 a3)∗; l3; φ3))` erasee∗(e∗): erasetfi(; l1; φ1 → (t3 a3)∗; l3; φ3)as they are the premises of typechecking a label block in Wasm.We have that S; C ` e∗0 : (t3 a3)∗; l3; φ3 → (t2 a2)n; l2; φ2 since it is apremise of Rule Label which we have assumed to hold.Then, by the inductive hypothesis for the stored instructions e∗0 beingwell typed, we have thateraseS(S); eraseC(C)` erasee∗(e∗0): erasetfi((t3 a3)∗; l3; φ3 → (t2 a2)∗; l2; φ2)S; C, label((t3 a3)∗; l3; φ3)) ` e∗ : ; l1; φ1 → (t3 a3)∗; l3; φ3, because itis a premise of Rule Label which we have assumed to hold.110By the inductive hypothesis for the body e∗ being well typed, we havethateraseS(S); eraseC(C, label((t3 a3)∗; l3; φ3))` erasee∗(e∗): erasetfi(; l1; φ1 → (t3 a3)∗; l3; φ3)• S; C ` localn{i; v∗} e∗ end : ; l1; φ1 → (t2 a2)n; l2; φ2The premise of this rule relies on Rule Code with a non-empty returnpostcondition, which we have not yet proved sound erasure for, soinstead we must derive Rule Code for the erased program.Thus, we must show that (` v : tv)∗ anderaseS(S); eraseC(Sinst(i), local t∗v, return((t2 a2)n; l2; φ2))` erasee∗(e∗): erasetfi(; l1; φ1 → (t2 a2)n; l2; φ2)We have Rule Code as a premise of Rule Local, which we haveassumed to hold.Therefore, (` v : tv)∗ trivially, since neither values nor primitive typesare affected by erasure.We also know thatS; Sinst(i), local t∗v, return((t2 a2)n; l2; φ2))` e∗ end: ; l1; φ1 → (t2 a2)n; l2; φ2Therefore, by the inductive hypothesis of the well-typedness of e∗, wehave thateraseS(S); eraseC(Sinst(i), local t∗v, return((t2 a2)n; l2; φ2))` erasee∗(e∗): erasetfi(; l1; φ1 → (t2 a2)n; l2; φ2)111B.2 Subject Reduction Lemmas and ProofsLemma 15. Inversion1. If S; C ` t.const c : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 (t a), l1 = l2,and φ1, (t a), (= a (t c)) =⇒ φ2.2. If S; C ` t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (t a1) (t a2),ti∗2 = ti∗ (t a3), l1 = l2, and φ1, (t a3), (= a3 (binop a1 a2)) =⇒ φ2.3. If S; C ` t.testop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (t a1),ti∗2 = ti∗ (i32 a2), l1 = l2, and φ1, (i32 a2), (= a2 (testop a1)) =⇒ φ2.4. If S; C ` t.relop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (t a1) (t a2),ti∗2 = ti∗ (i32 a3), l1 = l2, and φ1, (i32 a3), (= a3 (relop a1 a2)) =⇒φ2.5. If S; C ` nop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗2, l1 = l2, andφ1 =⇒ φ2.6. If S; C ` drop : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗0 (t a), ti∗2 = ti∗0,l1 = l2, and φ1 =⇒ φ2.7. If S; C ` select : ti∗1; l1; φ1 → ti∗2; l2; φ2,then ti∗1 = ti∗0 (t a1) (t a2) (i32 a3), ti∗2 = ti∗0; (t a), l1 = l2, andφ1, (t a), (if(= a3 (i32 0)) (= a1 a) (= a2 a)) =⇒ φ2.8. If S; C ` block (ti∗3; l3; φ3 → tim4 ; l4; φ4)e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2then ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 tim4 , l1 = l3, l2 = l4, φ1 =⇒ φ3, φ4 =⇒ φ2,and S; C, label(tim4 ; l4; φ4) ` e∗ : ti∗3; l3; φ3 → tim4 ; l4; φ4.9. If S; C ` loop (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2,then ti∗1 = ti∗0 tin3 , ti∗2 = ti∗0 tim4 , l1 = l3, l2 = l4, φ1 =⇒ φ3, φ4 =⇒ φ2,and S; C, label(tin3 ; l3; φ3) ` e∗ : tin3 ; l3; φ3 → tim4 ; l4; φ4.11210. If S; C ` if (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗1 else e∗2 end : ti∗1; l1; φ1 →ti∗2; l2; φ2, then ti∗1 = ti∗0 tin3 (i32 a), ti∗2 = ti∗0 tim4 , l1 = l3, l2 = l4,φ1 =⇒ φ3, φ4 =⇒ φ2, S; C, label(tim4 ; l4; φ4) ` e∗1 : tin3 ; l3; φ3,¬(=a (i32 0))→ tim4 ; l4; φ4, and S; C, label(tim4 ; l4; φ4) ` e∗2 : tin3 ; l3; φ3, (=a (i32 0))→ tim4 ; l4; φ4.11. If S; C ` labeln{e∗0}e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 ti∗,S; C ` e∗0 : ti∗3; l3; φ3 → ti∗; l2; φ2, and S; C, label (ti∗3; l3; φ3) ` e∗ :; l1; φ1 → ti∗; l2; φ212. If S; C ` br i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗3 ti∗, Clabel(i) =ti∗; l1; φ3, and φ1 =⇒ φ3.13. If S; C ` br if i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗2 (i32 a), l1 =l2, Clabel(i) = ti∗2; l1; φ3,¬(= a (i32 0)), φ1 =⇒ φ3, and φ1, (=a (i32 0)) =⇒ φ2.14. If S; C ` br table i+ : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗2 (i32 a),l1 = l2, Clabel(i) = ti∗2; l1; φ3, φ1 =⇒ φ3, and φ1 =⇒ φ2.15. If S; C ` call i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 ti∗4,Cfunc(j) = ti∗3; l3; φ3 → ti∗4; l4; φ4, l2 = l1, φ1 =⇒ φ3, and φ3, φ4 =⇒φ2.16. If S; C ` call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4 : ti∗1; l1; φ1 → ti∗2; l2; φ2,then ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 ti∗4, l2 = l1, φ1 =⇒ φ3, and φ3, φ4 =⇒ φ2.17. If S; C ` call cl : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 tim4 , l2 = l1,φ1 =⇒ φ3, φ4 =⇒ φ2, and S ` cl : ; tin3 (t a)n; φ3, (t a)k, (=a (t 0))k → tim4 ; l4; φ418. If S; C ` localn{i; v∗l } e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 =ti∗1 tin, l1 = l2, S; (tin; l3; φ3) `i v∗l ; e∗ : tin; l3; φ3, and φ1, φ3 =⇒ φ2.19. If S; C ` return : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗3 ti∗, l1 = l3,Creturn = ti∗; l3; φ3, and φ1 =⇒ φ3.11320. If S; C ` get local i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 (t a),l1 = l2, l1(i) = (t a), and φ1, (t a2), (= a2 a) =⇒ φ2.21. If S; C ` set local i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗2 (t a),l2 = l1[i := (t a)], Clocal(i) = t, and φ1 =⇒ φ2.22. If S; C ` tee local i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (t a),ti∗2 = ti∗ (t a2), l2 = l1[i := (t a)], Clocal(i) = t, and φ1, (t a2), (=a2 a) =⇒ φ2.23. If S; C ` get global i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗2 = ti∗1 (t a),l1 = l2, Cglobal(i) = mut? t, and φ1, (t a) =⇒ φ2.24. If S; C ` set global i : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗2 (t a),l1 = l2, Cglobal(i) = mut t, and φ1 =⇒ φ2.25. If S; C ` t.load (tp_sx)? align o : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 =ti∗ (i32 a1), ti∗2 = ti∗ (t a2), l1 = l2, Cmemory = n, 2align ≤ (|tp| <)?|t|,and φ1, (t a2) =⇒ φ2.26. If S; C ` t.store tp? align o : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 =ti∗2 (i32 a1) (t a2), l1 = l2, Cmemory = n, 2align ≤ (|tp| <)?|t|, andφ1 =⇒ φ2.27. If S; C ` current memory : ti∗1; l1; φ1 → ti∗2; l2; φ2,then ti∗2 = ti∗1 (i32 a), l1 = l2, Cmemory = n, and φ1, (i32 a) =⇒ φ2.28. If S; C ` grow memory : ti∗1; l1; φ1 → ti∗2; l2; φ2, then ti∗1 = ti∗ (i32 a1),ti∗2 = ti∗ (i32 a2), l1 = l2, Cmemory = n, and φ1, (i32 a2) =⇒ φ2.29. If S; C ` e∗1 e2 : ti∗1; l1; φ1 → ti∗3; l3; φ3, then S; C ` e∗1 : ti∗1; l1; φ1 →ti∗2; l2; φ2, and S; C ` e2 : ti∗2; l2; φ2 → ti∗3; l3; φ3.Proof. Proof omitted, but follows from induction over typing derivations.Lemma 16. Subject Reduction for CodeIf S; (ti; l; φ)? ` v∗; e∗ : ti; l; φ, ` s : S, (we omit this on rules that do notuse the store) and s; v∗; e∗ ↪→ s′; v′∗; e′∗, then S; (ti; l; φ)? ` v′∗; e′∗ : ti; l; φ,and ` s′ : S (we omit this on rules that do not change the store)114Proof. By induction on reduction.• Case: S; (ti∗; l; φ)? `i vj1 (t.const c) vk2 ; get local j : ti∗; l; φ∧ vj1 (t.const c) vk2 ; get local j ↪→ (t.const c)We want to show that S; (ti; l; φ)? `i vj1 (t.const c) vk2 ; (t.const c) :ti∗; l; φ.We know ` (t.const c) : (t a); ◦, (t a), (= a (t c)) and S; C ` get local j :; l1; φj1, ((t a), (= a (t c))), φk2 → ti∗; l; φ, because they are premises ofRule Code that we have assumed to hold.By Lemma Inversion on Rule Get-Local, ti∗ = (t a2), l1 = l, andφj1, ((t a), (= a (t c))), φk2, (t a2), (= a2 a) =⇒ φ.Now we will reconstruct the same type for vj1 (t.const c) vk2 ; (t.const c).We have S; Sinst(i) ` (t.const c) : ; l; φj1, ((t a), (= a (t c))), φk2 →(t a2); l; φj1, ((t a), (= a (t c))), φk2, (t a2), (= a2 (t c)) by Rule Const.Further, ((t a), (= a (t c))), (t a2), (= a2 (t c)) =⇒ ((t a), (=a (t c))), (t a2), (= a2 a) by =⇒ .Then, S; Sinst(i) ` (t.const c) : ; l; φj1, ((t a), (= a (t c))), φk2 →(t a2); l; φ by Rule Subtyping.Therefore, S; (ti∗; l; φ)? `i vj1 (t.const c) vk2 ; (t.const c) : ti∗; l; φ byRule Code.• Case: S; (ti∗; l; φ)?`i vj1 (t.const c) vk2 ; (t.const c′) (set local j): ti∗; l; φ∧ vj1 (t.const c) vk2 ; (t.const c′) set local j ↪→ vj1 (t.const c′) vk2 ; We want to show thatS; (ti∗; l; φ)? `i vj1 (t.const c′) vk2 ; (t.const c′) (set local j) : ti∗; l; φWe know ` (t.const c) : (t a); (◦, (t a), (= a (t c))), S; Sinst(i) `(t.const c′) (set local j) :  : l1; φj1, (◦, (t a), (= a (t c))), φk2 → ti∗; l; φ,and l1(j) = (t a), and Clocal(j) = t because they are premises of RuleCode that we have assumed to hold.115By Lemma Inversion on Rule Composition, S; Sinst(i) ` (t.const c′) :; l1; φj1, (◦, (t a), (= a (t c))), φk2 → ti∗3; l3; φ3, S; Sinst(i) ` set local j :ti∗3; l3; φ3 → ti∗; l; φ.Recall that t = Clocal(j), then by Lemma Inversion on Rule Set-Local we have ti∗3 = ti∗ (t a′), l = l3[j := (t a′)], and φ3 =⇒ φ.Then, by Lemma Inversion on Rule Const, ti∗ = , l1 = l3, andφj1, (◦, (t a), (= a (t c))), φk2, (t a′), (= a′ (t c′)) =⇒ φ3.Now we have all the information we need to derive the same type for(t.const c′)We have S; Sinst(i) `  : ; l; φ→ ; l; φ by Rule Empty.Then, S; Sinst(i) `  : ; l; φj1, (◦, (t a), (= a (t c))), φk2, (t a′), (=a′ (t c′))→ ; l; φ by Rule Subtyping.Since a is fresh, φj1, φk2, (t a′), (= a′ (t c′)) =⇒ φj1, (◦, (t a), (=a (t c))), φk2, (t a′), (= a′ (t c′)).Then, S; Sinst(i) `  : ; l; φj1, φk2, (t a′), (= a′ (t c′)) → ; l; φ by RuleSubtyping.Further, ` (t.const c′) : (t a′); ◦, (t a′), (= a′ (t c′)) by Rule Admin-Const.Therefore, S; (ti∗; l; φ)? `i vj1 (t.const c′) vk2 ;  : ti∗; l; φ by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; get global j : ti∗; l; φ∧ s; get global j ↪→i sglob(i, j)We want to show that S; (ti∗; l; φ)? `i v∗; sglob(i, j) : ti∗; l; φWe have ` v : tiv; φv)∗ and S; Sinst(i) ` get global j : ; ti∗v; φ∗v →ti∗; l; φ because they are premises of Rule Code that we have assumedto hold.Then, by Lemma Inversion on Rule Get-Global, ti∗ = (t a), l = l1,Cglobal(j) = mut?t, and φ∗v, (t a) =⇒ φ.Recall that we assume ` s : S, then we know S ` sinst(i) : C because itis a premise of Rule Store.116Recall that Sglobal(i, j) = mut?t, then ` sglob(i, j) : (t a1); φ1 becauseit is a premise of Rule Instance that we have assumed to hold.Now, we can show that sglob(i, j) has the appropriate type.We have S; Sinst(i) ` t.const c : ; l; φ∗v → (t a); l; φ∗v, (t a), (= a (t c)),where t.const c = sglob(i, j), by Rule Const.We also know (t a), (= a (t c)) =⇒ (t a).Thus, S; Sinst(i) ` sglob(i, j) : ; l; φ∗v → (t a); l; φ by Rule Subtyping.Recall ` v : tiv; φv)∗, then S; (ti∗; l; φ)? `i v∗; sglob(i, j) : (t a); l; φ byRule Code, having assumed that the other premises hold.• Case: S; (ti∗; l; φ)? ` v∗l ; (t.const c) (set global j) : ti∗; l; φ∧ s; (t.const c) (set global j) ↪→i s′; , where s′ = s with glob(i, j) =(t.const c)We want to show that S; (ti∗; l; φ)? ` v∗l ;  : ti∗; l; φ.We have ` (v∗l : tiv; φv)∗ and S; Sinst(i) ` v (set global j) : ; ti∗v; φ∗v →ti∗; l; φ because they are premises of Rule Code that we have assumedto hold.Further, by Lemma Inversion on Rule Composition, Rule Set-Global, and Rule Const, ti∗ = , l1 = l, Cglobal(j) = mut t, andφ∗v, (t a), (= a (t c)) =⇒ φ.We have S; Sinst(i) `  : ; l; φ→ ; l; φ by Rule Empty.Since a is fresh, φ∗v =⇒ φ∗v, (t a), (= a (t c)).Thus S; Sinst(i) `  : ; l; φ∗v → ; l; φ by Rule Subtyping.Recall that ` (v∗l : tiv; φv)∗, then S; (ti∗; l; φ)? `i v∗l ;  : ti∗; l; φ byRule Code.Now we must ensure that the new store s′ is well typed: ` s′ : S.Recall ` s : S, then Sglob(i, j) = mut? t and sglob(i, j) = (t.const c′)where ` (t.const c′) : (t ag); ◦, (t ag), (= ag (t c′)) because it is a premiseof ` s : S.117We know ` (t.const c) : (t.const c) : (t ag2); ◦, (t ag2), (= ag2 (t c)), andtherefore ` s′ : S by Rule Store.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.load align o) : ti∗; l; φ∧ s; (i32.const k) (t.load align o) ↪→i t.const constt(b∗),where smem(i, k + o, |t|) = b∗We want to show that S; (ti∗; l; φ)? `i v∗; (t.const constt(b∗)) : ti∗; l; φWe know (` v : tiv; φv)∗ and S; C ` (i32.const k) (t.load align o) :; ti∗v; φ∗v → ti∗; l; φ because they are premises of Rule Code which wehave assumed to hold.Then, by Lemma Inversion on Rule Composition, Rule Const,Rule Mem-Load, we know ti∗ = (t a), ti∗v = l, and φ∗v, (t a) =⇒ φ.We haveS; Sinst(i)` t.const constt(b∗): ; ti∗v; φ∗v → (t a); l; φ∗v, (t a), (= a (t c))by Rule Const.Then, S; Sinst(i) ` (t.const constt(b∗)) : ; ti∗v; φ∗v → (t a); l; φ by RuleSubtyping.Recall (` v : tiv; φv)∗, then S; (ti∗; l; φ)? `i v∗; t.const constt(b∗) :ti∗; l; φ by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.load tpsx align o) : ti∗; l; φ∧ s; (i32.const k) (t.load tpsx align o) ↪→i s; t.const constsxt (b∗), wheresmem(i, k + o, |tp|) = b∗Similar to above case, except with |tp| replacing |t| and constsxt (b∗)instead of constt(b∗).• Case: S; (ti∗; l; φ)?`i v∗; (i32.const k) (t.load tp_sx? align o): ti∗; l; φ∧ s; (i32.const k) (t.load tp_sx? align o) ↪→i trap118We know (` v : tiv; φv)∗ because it is a premise of Rule Code whichwe have assumed to hold.We have S; Sinst(i) ` trap : ; ti∗v; φ∗v → ti∗; l; φ by Rule Trap.Then, S; (ti∗; l; φ)? `i v∗; trap by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.const c) (t.store align o) :ti∗; l; φ∧ s; (i32.const k) (t.const c) (t.store align o) ↪→i s′; , where s′ =s with mem(i, k + o, |t|) = bits|t|t (c)We know (` v : tiv; φv)∗ andS; Sinst(i)` (i32.const k) (t.const c) (t.store align o): ; ti∗v; φ∗v → ti∗; l; φbecause they are premises of Rule Code which we have assumed tohold.Then, by Lemma Inversion on Rule Composition, Rule Const,and Rule Mem-Store, we have ti∗ = , tiv = l, and φ∗v, (i32 a1), (=a1 (i32 k)), (t a2), (= a2 (t c)) =⇒ φ.Since a1 and a2 are fresh, φ∗v =⇒ φ.We have S; Sinst(i) `  : ; l; φ∗v → ; l; φ∗v by Rule Empty.Then, S; Sinst(i) `  : ; tiv; φ∗v → ; l; φ by Rule Subtyping.Recall that (` v : tiv; φv)∗. Therefore, S; (ti∗; l; φ)? `i v∗;  : ti∗; l; φby Rule Code.Now we must ensure that the new store s′ is well typed: ` s′ : S.Recall ` s : S, then Smem(i) = n and smem(i) = b∗ where n ≤ |b∗|because it’s a premise of Rule Store.Since s′ = s with mem(i, k + o, |t|) = bits|t|t (c), then |s′textmem(i) |=|stextmem(i)|, and therefore n ≤ |s′textmem(i)|, so s′ : S by RuleStore.119• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.const c) (t.store tp align o) :ti∗1; l1; φ1 → ti∗2; l2; φ2 ∧ ` s : S∧ s; (i32.const k) (t.const c) (t.store tp align o) ↪→i s′; , where s′ =s with mem(i, k + o, |tp|) = bits|tp|t (c)Similar to above case, except with |tp| replacing |t| and constsxt (b∗)instead of constt(b∗).• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) (t.const c) (t.store tp? align o) :ti∗; l; φ∧ s; (i32.const k) (t.const c) (t.store tp? align o) ↪→i trapWe know (` v : tiv; φv)∗ because it is a premise of Rule Code whichwe have assumed to hold.We have S; Sinst(i) ` trap : ; ti∗v; φ∗v → ti∗; l; φ by Rule Trap.Then, S; (ti∗; l; φ)? `i v∗; trap by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; current memory : ti∗; l; φ∧ s; current memory ↪→i i32.const |smem(i, ∗)|/64KiWe know (` v : tiv; φv)∗ and S; Sinst(i) ` current memory : ; ti∗v; φ∗v →ti∗; l; φ because they are premises of Rule Code which we have assumedto hold.Then, by Lemma Inversion on Rule Current-Memory, ti∗ = (i32 a),ti∗v = l, and φ∗v, (i32 a) =⇒ φ.Let c = |smem(i, ∗)|/64Ki. Although note that the actual value of c isirrelevant to the rest of the proof case.S; Sinst(i) ` i32.const c : ; l; φ∗v → (i32 a); l; φ∗v, (i32 a), (= a (i32 c))by Rule Const.S; Sinst(i) ` i32.const c : ; ti∗; φ∗v → (i32 a); l; φ by Rule Subtyping.Recall that (` v : tiv; φv)∗. Thus, S; (ti∗; l; φ)? `i v∗; i32.const c :ti∗; l; φ by Rule Code.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) grow memory : ti∗; l; φ∧ s; (i32.const k) grow memory ↪→i s′; i32.const |smem(i, ∗)|/64Ki,120where s′ = s with mem(i, ∗) = smem(i, ∗)(0)k·64KiWe have (` v : tiv; φv)∗ and S; Sinst(i) ` (i32.const k) grow memory :; ti∗v; φ∗v → ti∗; l; φ because they are premises of Rule Code which wehave assumed to hold.By Lemma Inversion on Rule Composition, Rule Const, andRule Grow-Memory, we also have ti∗ = (i32 a1), ti∗v = l, andφφvv , (i32 a2), (= a2 (i32 k)), (i32 a1) =⇒ φ.Further, Smem(i) ≤ |smem(i, ∗)| because it is a premise of Rule Storeon ` s : S, which we have assumed to hold.Let c = i32.const |smem(i, ∗)|/64Ki. Although note that the actual valueof c is irrelevant to the rest of the proof case.S; Sinst(i) ` i32.const c : ; l; φ∗v→ (i32 a1); l; φ∗v, (i32 a1), (= a1 (i32 c))by Rule Const.Since a2 is fresh, φ∗v, (i32 a1) =⇒ φ.S; Sinst(i) ` i32.const c : ; ti∗v; φ∗v → (i32 a1); l; φ by Rule Subtyping.S; (ti∗; l; φ)? `i i32.const c : ti∗; l; φ by Rule Code.Now we must ensure that the new store s′ is well typed: ` s′ : S.Recall ` s : S, then Smem(i) = n and smem(i) = b∗ where n ≤ |b∗|because it’s a premise of Rule Store.Since s′ = s with mem(i, ∗) = smem(i, ∗)(0)k·64Ki, then |s′mem(i)| >|smem(i)|, and therefore n ≤ |s′mem(i)|, so s′ : S by Rule Store.• Case: S; (ti∗; l; φ)? `i v∗; (i32.const k) grow memory : ti∗; l; φ∧ s; (i32.const k) grow memory ↪→i i32.const (−1)Same as above case since the value of c is irrelevant (and can thereforebe -1).121• Case: S; (ti∗; l; φ)? `j v∗0; local{i; v∗} e∗ : ti∗; l; φ∧ s; v∗0; local{i; v∗} e∗ ↪→j s′; v∗0; local{i; v′∗} e′∗where s; v∗; e∗ ↪→i s′; v′∗; e′∗We want to show that `j s′; v∗0; local{i; v′∗} e′∗ : ti∗; l; φ.First, we will derive the type of the body of the local block.We have S; Sinst(j) ` local{i; v∗} e∗ : ; ti∗v; φ∗v0 → ti∗; l; φ where(` v0 : tiv; φv0)∗ because they are premises of Rule Code.Then, S; (ti∗; l; φ) `i v∗; e∗ : ti∗; l; φ0, where φ0 =⇒ φ by LemmaInversion on Rule Local.Now, we invoke the inductive hypothesis and use it to rebuild theoriginal type.Since S; (ti∗; l; φ) `i v∗; e∗ : ti∗; l; φ0, s ` S and s; v∗; e∗ ↪→i s′; v′∗; e′∗,then by the inductive hypothesis we know that ` s′ : S andS; (ti∗; l; φ) `i v′∗; e′∗ : ti∗; l; φ0Thus, S; Sinst(j) ` local{i; v′∗} e′∗ : ; ti∗v; φ∗v0 → ti∗; l; φ by RuleLocal.Finally, S; (ti∗; l; φ)? `i v∗0; local{i; v′∗} e′∗ : ti∗; l; φ and ` s′ : S.• Case: S; (ti∗; l; φ)? `i v∗; Lk[e∗] : ti∗; l; φ∧ s; v∗; Lk[e∗] ↪→i s′; v′∗; Lk[e′∗]where s; v∗; e∗ ↪→i s′; v′∗; e′∗We want to show that S; (ti∗; l; φ)∗ `i Lk[e′∗] : ti∗; l; φ.First, we will derive the type of the body of the local context.We have S; C ` Lk[e∗] : ; ti∗v; φ∗v → ti∗; l; φ,where C = Sinst(i), local t∗v, return (ti∗; l; φ)? because it is a premise ofRule Code.The intuition for the proof is that there is no requirement on whatthe label stack is of the module type context C under which Lk[e∗] is122typed. Thus, we can reduce e∗ outside of Lk, but with the module typecontext C as if it were inside of Lk.The proof continues via induction on k.– Case: k = 0Lk[e∗] = v∗0 e∗ e∗0.By Lemma Inversion on Rule Composition and Rule ConstS; C ` e∗ : ti∗1; ti∗v; φ∗v, φ∗v0 → ti∗2; l2; φ2 andS; C ` e∗0 : ti∗2; l2; φ2 → ti∗; l; φ.Since s; v∗; e∗ reduces, e∗ can be typed with an empty stack pre-condition. Therefore ti∗2 = ti∗1 ti∗3 and S; C ` e∗ : ; ti∗v; φ∗v, φ∗v0 →ti∗3; l2; φ2.Since φ∗v0 only contains fresh index variables, φ∗v =⇒ φ∗v, φ∗v0.S; C ` e∗ : ; ti∗v; φ∗v → ti∗3; l2; φ2 by Rule Implies.Then, S; (ti∗; l; φ)? `i v∗; e∗ : ti∗3; l2; φ2 by Rule Code.Now, we invoke the Lemma Subject Reduction for Codeinductive hypothesis and rebuild the type using the reduced ex-pression.Since S; (ti∗; l; φ)∗ `i v∗; e∗ : ti∗3; l2; φ2, s ` S, and s; v∗; e∗ ↪→is′; v′; e′∗, then by the inductive hypothesis we know that ` s′ : Sand S; (ti∗; l; φ) `i v′∗; e′∗ : ti∗3; l2; φ2.S; C ` e′∗ : ; ti∗v′ ; φ∗v′ → ti∗3; l2; φ2 because it is a premise of RuleCode.S; C ` v∗0 : ; ti∗v′ ; φ∗v′ → ti∗1; ti∗v′ ; φ∗v′ , φ∗v0 by Rule Const.S; C ` e′∗ : ti∗1; ti∗v′ ; φ∗v′ , φ∗v0 → ti∗2; l2; φ2 by Rule Implies andRule Stack-Poly.S; C ` v∗0 e′∗ e∗0 : ; ti∗v′ ; φ∗v′ , φ∗v0 → ti∗; l; φ by Rule Composi-tion.Therefore, S; (ti∗; l; φ)∗ `i Lk[e′∗] : ti∗; l; φ and ` s′ : S.– Case: k > 0Lk[e∗] = v∗k labeln{e∗0} Lk−1[e∗] end e∗k.123By Lemma Inversion on Rule Const and Rule Composition,S; C ` labeln{e∗0} Lk−1[e∗] end : ti∗1; ti∗v; φ∗v, φ∗vk → ti∗2; l2; φ2 andS; C ` e∗k : ti∗2; l2; φ2 → ti∗; l; φ.By Lemma Inversion on Rule Label, ti∗2 = ti∗1 ti∗3, S; C ` e∗0 :ti∗4; l4; φ4 → ti∗3; l2; φ2, and S; C, label (ti∗4; l4; φ4) ` Lk−1[e∗] :; ti∗v; φ∗v, φ∗vk → ti∗3; l2; φ2.Since φ∗vk only contains fresh index variables, φ∗v =⇒ φ∗v, φ∗vk.S; C, label (ti∗4; l4; φ4) ` Lk−1[e∗] : ; ti∗v; φ∗v → ti∗3; l2; φ2 by RuleImplies.S; (ti∗; l; φ)? ` v∗; Lk−1[e∗] : ti∗3; l2; φ2 by Rule Code.Now, we invoke the inductive hypothesis on Lk−1[e∗] and rebuildthe type using the reduced expression.Since S; (ti∗; l; φ)∗ `i v∗; Lk−1[e∗] : ti∗3; l2; φ2, s ` S, ands; v∗; e∗ ↪→i s′; v′; e′∗, then by the inductive hypothesis onLk−1[e∗] we know that ` s′ : S andS; (ti∗; l; φ) `i v′∗; Lk−1[e′∗] : ti∗3; l2; φ2S; C, label ` Lk−1[e′∗] : ; ti∗v′ ; φ∗v′ → ti∗3; l2; φ2 because it is apremise of Rule Code.S; C ` v∗k : ; ti∗v′ ; φ∗v′ → ti∗1; ti∗v′ ; φ∗v′ , φ∗vk by Rule Const.S; C ` labeln{e∗0} Lk−1[e′∗] end : ; ti∗v′ ; φ∗v′ → ti∗3; l2; φ2 by RuleLabel.S; C ` labeln{e∗0} Lk−1[e′∗] end : ti∗1; ti∗v′ ; φ∗v′ , φ∗vk → ti∗2; l2; φ2 byRule Implies and Rule Stack-Poly.S; C ` v∗k labeln{e∗0} Lk−1[e∗] end e∗k : ; ti∗v′ ; φ∗v′ → ti∗; l; φ byRule Composition.Therefore, S; (ti∗; l; φ)∗ `i Lk[e′∗] : ti∗; l; φ and ` s′ : S.• Otherwise: we have (` (t.const c) : (t a); (◦, (t a), (= a (t c))))∗, andS, Sinst(i) ` e∗ : ; (t a)∗; (◦, (t a), (= a (t c)))∗ → ti; l; φBy Lemma Subject Reduction Without Effects, we haveS, Sinst(i) ` e′∗ : ; (t a)∗; (◦, (t a), (= a (t c)))∗ → ti; l; φ.Then, S; (ti∗; l; φ)? ` v∗; e′∗ : ti; l; φ124Lemma 17. Subject Reduction Without EffectsIf S; C ` e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2,` s : S (note: we omit this for cases which do not use s),and s; v∗; e∗ ↪→ s; v∗; e′∗,then S; C ` e′∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2Proof. By case analysis on the reduction rules.• S; C ` L0[trap] : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ L0[trap] ↪→ trapThis case is trivial since trap accepts any precondition and postcondition.Thus, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• S; C ` (t.const c1) (t.const c2) t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) t.binop ↪→ t.const c where c = binop(c1, c2)We want to show that S; C ` t.const c : ti∗1; l1; φ1 → ti∗2; l2; φ2.We begin by reasoning about the type of the original instructions(t.const c1) (t.const c2) t.binopBy Lemma Inversion on Rule Composition, Rule Const, and RuleBinop, we know that ti∗2 = ti∗1(t a3), l2 = l1, and thatφ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(t a3), (= a3 (binop a1 a2))=⇒ φ2Now we will show that t.const c has the appropriate type.By const, S; C ` t.const c : ; l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (t c)).Because c = binopt(c1, c2), then by =⇒ ,φ1, (t a), (= a (t c)) =⇒ φ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(t a3), (= a3 (binop a1a2))125Therefore, S; C ` (t.const c) : ti∗1; l1; φ1 → ti∗1 (t a3); l1; φ2, by RuleStack-Poly and Rule Subtyping.• C ` (t.const c1) (t.const c2) t.binop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) t.binop ↪→ trapThis case is trivial since trap accepts any precondition and postcondition.Thus, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• C ` (t.const c) t.testop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c) t.testop ↪→ i32.const c2 where c2 = testop(c)We want to show that S; C ` i32.const c2 : ti∗1; l1; φ1 → ti∗2; l2; φ2.First, we use our reasoning principles to get more information aboutthe original type.By Lemma Inversion on Rule Composition, Rule Const, and RuleTestop, we know that ti∗2 = ti∗1 (t a2), l2 = l1, and thatφ1, (t a1), (= a1 (t c)),(i32 a2), (= a2 (testop a1))=⇒ φ2Now we show that i32.const c2 has the appropriate type.By const, C ` i32.const c2 : ; l1; φ1→ (i32 a2); l1; φ1, (i32 a2), (= a2 (t c2)).Because c2 = testop(c), then by =⇒ ,φ1, (t a), (= a (t c2)) =⇒ φ1, (t a1), (= a1 (t c)),(i32 a2), (= a2 (testop a1))Therefore, S; C ` t.const c2 : ti∗1; l1; φ1 → ti∗1 (t a2); l1; φ2, by RuleStack-Poly and Rule Subtyping• S; C ` (t.const c1) (t.const c2) t.relop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) t.relop ↪→ t.const c where c = relop(c1, c2)126This case is identical to the (t.const c1) (t.const c2) t.binop ↪→ t.const ccase, except that binop is replaced with relop.• S; C ` unreachable : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ unreachable ↪→ trapThis case is once again trivial since trap accepts any precondition andpostcondition. Thus, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by trap.• S; C ` nop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ nop ↪→ We want to show that S; C `  : ti∗1; l1; φ1 → ti∗2; l2; φ2.This case follows from the fact that the postcondition ti∗2; l2; φ2 for nopmust be immediately reachable from the precondition ti∗1; l1; φ1.By Lemma Inversion on Rule Nop, we know that ti∗2 = ti∗1, l2 = l1,and φ1 =⇒ φ2.Then, S; C `  : ; l; g; φ1 → ; l; g; φ1 by Rule Empty.Thus, S; C ` ti∗1; l; g; φ1 → ti∗1; l; g; φ2 by Rule Stack-Poly andRule Subtyping.• S; C ` (t.const c) drop : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c) drop ↪→ We want to show that S; C `  : ti∗1; l1; φ1 → ti∗2; l2; φ2.Like the above case, this follow from the fact that the postcondi-tion ti∗2; l2; φ2 must be immediately reachable from the preconditionti∗1; l1; φ1. However, there are a few extra steps since we now have toreason about two different instructions (and therefore Rule Composi-tion).By Lemma Inversion on Rule Composition, Rule Const, and RuleDrop, we know that ti∗2 = ti∗1, l2 = l1, and φ1 =⇒ φ2.By empty, S; C `  : ; l1; φ1 → ; l1; φ1.Thus, S; C ` ti∗1; l; g; φ1 → ti∗1; l; g; φ2 by Rule Stack-Poly andRule Subtyping.127• Case: S; C ` (t.const c1) (t.const c2) (i32.const 0) select: ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c1) (t.const c2) (i32.const 0) select ↪→ (t.const c2)We want to show that S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗2; l2; φ2.First, we reason about what the original type must look like.By Lemma Inversion on Rule Composition, Rule Const, and RuleSelect, we know that ti∗2 = ti∗1 (a3 ), l2 = l1, andφ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(i32 a), (= a (i32 0)),(t a3), (if (= a (i32 0)) (= a3 a2) (= a3 a1))=⇒ φ2Now we show that (t.const c2) has the appropriate type.By Rule Const,C ` (t.const c2) : ; l1; φ1→ (t a3); l1; φ1, (t a3), (= a3 (t c2))Then, S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗1 (t a3); l1; φ1, (t a3), (=a3 (t c2)) by Rule Stack-Poly.By =⇒ , we haveφ1, (t a3), (= a3 (t c2)) =⇒ φ1, (t a1), (= a1 (t c1)),(t a2), (= a2 (t c2)),(i32 a), (= a (i32 0)),(t a3), (if (= a (i32 0))(= a3 a2)(= a3 a1))Therefore, S; C ` (t.const c2) : ti∗1; l1; φ1 → ti∗2 (t a3); l1; φ2 by sub −typing• Case: S; C ` (t.const c)n block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end :128ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c)n block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end↪→ labelm{} (t.const c)n e∗ endWe want to show that labelm{} (t.const c)n e∗ end : ti∗1; l1; φ1 →ti∗2; l2; φ2.First, we reason about ti∗1; l1; φ1 → ti∗2; l2; φ2.We know S; C` block (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end: ti∗1 (t a)n; l1; φ1, (t a)n, (= a (t c))n → ti∗2; l2; φ2by Lemma Inversion on Rule Composition and Rule Const.By Lemma Inversion on Rule Block, l1 = l3 and l2 = l4. We willuse l1, l2 in place of l3, l4, respectively, for the remainder of the case.Then, S; C, label(tm4 ; l2; φ4) ` e∗ : (t a)n; l1; φ3 → tim4 ; l2; φ4 becauseit is a premise of Rule Block which we have already assumed to hold.Also, (t a)n = tin3 , ti∗2 = ti∗1 tim4 , φ1, (t a)n, (= a (t c))n =⇒ φ3, andφ4 =⇒ φ2 by Lemma Inversion on Rule Block.Now we have all the information we need to show thatlabelm{} (t.const c)n e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2.Remember that Rule Label uses the types of both the body(t.const c)n e∗ and the stored instructions .First, we show the type of the body.We haveS; C, label(tm4 ; l2; φ4) ` (t.const c)n : ; l1; φ1→ (t a)n; l1; φ1, (t a)n, (= a (t c))nby Rule Const.Then, since φ1, (t a)n, (= a (t c))n =⇒ φ3, we haveS; C, label(tn3 ; l1; φ3) ` (t.const c)n : ; l1; φ1 → (t a)n; l1; φ3by Rule Subtyping.129Recall we have S; C, label(tm4 ; l2; φ4) ` e∗ : (t a)n; l1; φ3 → tim4 ; l2; φ4.Then S; C, label(tm4 ; l2; φ4) ` (t.const c)n e∗ : ; l1; φ1 → tim4 ; l2; φ4 byRule Composition.We have the type we want from the body. Now we get the type wewant of the stored instructions. We already have the postcondition wewant, tm4 ; l2; φ4, in the label stack, so we want the stored instructionto just pass the information through. Since the stored instructions is ,this is simple to show: we have S; C `  : tim2 ; l2; φ4 → tim2 ; l2; φ4 byRule Empty and Rule Stack-Poly.Therefore, C ` labelm{} (t.const c)n e∗ end : ; l1; φ1 → tim2 ; l2; φ4 bylabel.Finally, since φ4 =⇒ φ2, S; C ` labelm{} (t.const c)n e∗ end :ti∗1; l1; φ1 → ti∗1 tim4 ; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` (t.const c)n loop (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗ end :ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (t.const c)n loop tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗ end↪→ labeln{loop tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗ end} (t.const c)n e∗ endWe want to show that labeln {loop tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗ end}(t.const c)n e∗ end : ti∗1; l1; φ1 → ti∗2; l2; φ2This rule is similar to the above one, except that we must reason alittle more about the stored instructions since we are storing the loop.We start by figuring out what ti∗1; l1; φ1 → ti∗2; l2; φ2 looks like.We knowS; C ` loop tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗ end: ti∗1 (t a)n; l1; φ1, (t a)n, (= a (t c))n → ti∗2; l2; φ2by Lemma Inversion on Rule Composition and Rule Const.By Lemma Inversion on Rule Loop, l1 = l3 and l2 = l4. We will usel1, l2 in place of l3, l4, respectively, for the remainder of the case.130Then, S; C, label(tm4 ; l2; φ4) ` e∗ : (t a)n; l1; φ3 → tim4 ; l2; φ4 becauseit is a premise of Rule Loop which we have already assumed to hold.Also, (t a)n = tin3 , ti∗2 = ti∗1 tim4 , φ1, (t a)n, (= a (t c))n =⇒ φ3, andφ4 =⇒ φ2 by Lemma Inversion on Rule Loop.Now we have all the information we need to show thatS; C ` labeln{loop tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗ end} (t.const c)n e∗ end: ti∗1; l1; φ1 → ti∗2; l2; φ2We have S; C, label(tn3 ; l1; φ3) ` (t.const c)n : ; l1; φ1 →(t a)n; l1; φ1, (t a)n, (= a (t c))n by Rule Const.Then, since φ1, (t a)n, (= a (t c))n =⇒ φ3, we haveS; C, label(tn3 ; l1; φ3) ` (t.const c)n : ; l1; φ1 → (t a)n; l1; φ3by Rule Subtyping.Recall that S; C, label(tn3 ; l1; φ3) ` e∗ : tin1 ; l1; φ3 → tim2 ; l1; φ4.Then S; C, label(tn3 ; l1; φ3) ` (t.const c)n e∗ : ; l1; φ1 →tim4 ; l2; φ4 by composition.We have the type we want from the body. Now we get the type we wantof the stored instructions, which in this case is the loop. Since we alreadyhave the necessary type information of the body, we then have thatS; C ` loop tfi e∗ end : (t a)n; l1; φ1, (t a)n, (= a (t c))n → tim4 ; l2; φ4by Rule Loop.Therefore, S; C ` labelm{loop tfi e∗ end} vn e∗ end : ; l1; φ1 →tim4 ; l2; φ4 by Rule Label.Finally, since φ4 =⇒ φ2, S; C ` labelm{} (t.const c)n e∗ end :ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` (i32.const 0) if (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗1 else e∗2 end :ti∗1; l1; φ1 → ti∗2; l2; φ2131∧ (i32.const 0) if tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 else e∗2 end↪→ block tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗2 endWe want to show thatblock tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 end : ti∗1; l1; φ1 → ti∗2; l2; φ2First, we reason about ti∗1; l1; φ1 → ti∗2; l2; φ2.We knowS; C` if tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 else e∗2 end: ti∗1 (t a); l1; φ1, (t a)n, (= a (t 0))n → ti∗2; l2; φ2by Lemma Inversion on Rule Composition and Rule Const.Then, we have S; C, label(tim4 ; l4; φ4) ` e∗2 : tin3 ; l3; φ3, (= a (i32 0))→tim4 ; l4; φ4 because it is a premise of Rule If which we have assumed tohold.By Lemma Inversion on Rule If, ti∗1 = ti∗0 tin3 and ti∗2 = ti∗0 tim4for some ti∗0, l1 = l3, l2 = l4, φ1, (i32 a), (= a (i32 0)) =⇒ φ3, andφ4 =⇒ φ2.Now, we show that block tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 end : ti∗1; l1; φ1 →ti∗2; l2; φ2S; C ` block tin3 ; l3; φ3, (= a (i32 0)) → tim4 ; l4; φ4 e∗2 end by RuleBlock.Since a is fresh after reduction, φ1 =⇒ φ1, (i32 a), (= a (i32 0)) by=⇒ .Therefore, S; C ` block tin3 ; l3; φ3, (= a (i32 0))→ tim4 ; l4; φ4 e∗2 end :ti∗0 tin3 ; l1; φ1, (t a), (= a (i32 0)) → s ti∗0 tim4 ; l2; φ2 by Rule Stack-Poly and Rule Subtyping.132• Case: S; C ` (i32.const k + 1) if (tin3 ; l3; φ3 → tim4 ; l4; φ4) e∗1else e∗2end: ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (i32.const k + 1) if tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 else e∗2 end↪→ block tin3 ; l3; φ3 → tim4 ; l4; φ4 e∗1 endThis case is the same as above, except with e2 instead of e1 and k + 1instead of 0.• Case: S; C ` labeln{e∗} vn end : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ labeln{e∗} vn end ↪→ vnWe want to show that vn : ti∗1; l1; φ1 → ti∗2; l2; φ2We first figure out what ti∗1; l1; φ1 → ti∗2; l2; φ2 looks like.By Lemma Inversion on Rule Label, we know ti∗2 = ti∗1 tin4 .S; C ` vn : ; l1; φ1 → tin4 ; l2; φ2 because it is a premise of Rule Labelwhich we have assumed to hold.Now we can show that vn has the same type.Therefore, S; C ` vn : ti∗1; l1; φ1 → ti∗1 tin4 ; l1; φ2 by Rule Stack-Poly.• Case: S; C ` labeln{e∗} trap end : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ labeln{e∗} trap end ↪→ trapTrivially, C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap since trapaccepts any precondition and postcondition.• Case: S; C ` labeln{e∗} Lj [(t.const c)n (br j)] end : ti∗1; l1; φ1 →ti∗2; l2; φ2∧ labeln{e∗} Lj [(t.const c)n (br j)] ↪→ (t.const c)n e∗We want to show that vn e∗ : ti∗1; l1; φ1 → ti∗2; l2; φ2.Intuitively, this proof works because the premise of Rule Br assumesthat Clabel(i) is the precondition (tin1 ; l3; φ5, as we will soon see) of thestored instructions e∗ in the i + 1th label, and the postcondition ofthe label block is immediately reachable from the postcondition of e∗.133Meanwhile, that assumptions is ensured by Rule Label, which ensuresthat e∗ has the same precondition as the i+1th branch postcondition onthe label stack and the same postcondition as the label block instruction.By Lemma Inversion on Rule Label, ti∗2 = ti∗1 ti∗4 for some ti∗4.Also, S; C, label(tin1 ; l3; φ5)j ` (t.const c)n (br j) : ; l3; φ3 → ti∗∅; l∅; φ∅for some l3 and φ3, where φ5 = φ3, (t a)n, (= a (t c))n, by LemmaInversion on Rule Label and Rule Br.Then, S; C, label(tin1 ; l3; φ5)j ` (br j) : tin1 ; l3; φ5 → ti∗∅; l∅; φ∅, byLemma Inversion on Rule Composition and Rule Const.Then, S; C, label(tin1 ; l3; φ5)j ` (t.const c)n : ; l3; φ3 → tin1 ; l3; φ5since it is a premise of composition which we have assumed to hold.Further, S; C ` e∗ : tin1 ; l3; φ5 → ti∗2; l2; φ4 since it is a premise of RuleLabel which we have assumed to hold, and φ4 =⇒ φ2 by LemmaInversion on Rule Label.Then, S; C ` (t.const c)n e∗ : ; l1; φ1 → ti∗2; l2; φ4 by Lemma Lift-Consts and Rule Composition.Finally, C ` (t.const c)n e∗ : ti∗1; l1; φ1 → ti∗1 ti∗4; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` (i32.const 0) (br if j) : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (i32.const 0) (br if j) ↪→ In the case that br if does not branch, it acts exactly like drop (consumes(i32.const 0) and reduces to the empty sequence). Thus, this case is thesame as the drop case.• Case: S; C ` (i32.const k + 1) (br if j) : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (i32.const k + 1) (br if j) ↪→ br jWe want to show that S; C ` br j : ti∗1; l1; φ1 → ti∗2; l2; φ2We know S; C ` br table j : ti∗1 (i32 a); l1; φ1, (t a), (= a (i32 k)) →ti∗2; l2; φ2 by Lemma Inversion on Rule Composition and RuleConst.134Then we know Clabel(j) = (ti∗3; l1; φ3), where ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 ti∗3,and φ1, (t a),¬(= a (i32 0)) =⇒ φ3 by Lemma Inversion on RuleBr-Table.Now we can show that S; C ` br j : ti∗0 ti∗3; l1; φ1 → ti∗0 ti∗3; l2; φ2.We have S; C ` br j : ti∗3; l1; φ3 → ti∗3; l2; φ2 by Rule Br.Then, S; C ` br j : ti∗3; l1; φ1, (t a),¬(= a (i32 0)) → ti∗3; l2; φ2, andtherefore S; C ` br j : ti∗3; l1; φ1, (t a), (= a (i32 k)) → ti∗3; l2; φ2 byRule SubtypingBecause a is fresh after reduction, φ1 =⇒ φ1, (i32 a), (= a (i32 k)).Therefore, C ` br j : ti∗0 ti∗3; l1; φ1 → ti∗0 ti∗3; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: S; C ` (i32.const k) (br table jk1 j j∗2) : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (i32.const k) (br table jk1 j j∗2) ↪→ br jWe want to show that S; C ` br j : ti∗1; l1; φ1 → ti∗2; l2; φ2This case is similar in structure to the (i32.const k + 1) (br if j) case.We knowS; C ` br table jk1 j j∗2 : ti∗1 (i32 a); l1; φ1, (t a), (= a (i32 k))rightarrowti∗2; l2; φ2by Lemma Inversion on Rule Composition and Rule Const.Then we know Clabel(j) = (ti∗3; l1; φ3), where ti∗1 = ti∗0 ti∗3, ti∗2 = ti∗0 ti∗3,and φ1, (t a),¬(= a (i32 0)) =⇒ φ3 by Lemma Inversion on RuleBr-Table.Now we can show that S; C ` br j : ti∗0 ti∗3; l1; φ1 → ti∗0 ti∗3; l2; φ2.We have S; C ` br j : ti∗3; l1; φ3 → ti∗3; l2; φ2 by Rule Br.Then, S; C ` br j : ti∗3; l1; φ1, (t a), (= a (i32 k))→ ti∗3; l2; φ2 by RuleSubtyping.Because a is fresh after reduction, φ1 =⇒ φ1, (i32 a), (= a (i32 k)).135Therefore, C ` br j : ti∗0 ti∗3; l1; φ1 → ti∗0 ti∗3; l2; φ2 by Rule Stack-Poly and Rule Subtyping.• Case: C ` (i32.const k + n) (br table jk1 j) : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ (i32.const k + n) (br table jk1 j) ↪→ br jSame as above.• Case: S; C ` call j : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ s; call j ↪→i call sfunc(i, j)We want to show that call sfunc(i, j) : ti∗1; l1; φ1 → ti∗2; l2; φ2.By Lemma Inversion on RuleCall, we know that l2 = l1, ti∗1 = ti∗0 ti∗3,ti∗2 = ti∗0 ti∗4, φ1 =⇒ φ3, and φ3, φ4 =⇒ φ2, where ti∗3; l3; φ3 →ti∗4; l4; φ4 = Cfunc(j).We also know S ` sinst(i) : C since it is a premise of ` s : S which wehave assumed to hold.Then we know S ` sfunc(i, j) : ti∗3; l3; φ3 → ti∗4; l4; φ4 because it is apremise of S ` sinst(i) : C.Therefore, S; C ` call sfunc(i, j) : ti∗3; l3; φ3 → ti∗4; l4; φ4 by Rule Call-Cl.Thus, S; C ` call sfunc(i, j) : ti∗0 ti∗3; l1; φ1 → ti∗0 ti∗4; l2; φ2 by RuleStack-Poly and Rule Subtyping.• Case: S; C ` (i32.const j) call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4: ti∗1; l1; φ1 → ti∗2; l2; φ2∧ s; (i32.const j) call indirect ti∗3; l3; φ3 → ti∗4; l4; φ4 ↪→i call stab(i, j)where stab(i, j)code = (func tfi0 local t∗ e∗) and tfi0 <: ti∗3; l3; φ3 →ti∗4; l4; φ4We want to show that call stab(i, j) : ti∗1; l1; φ1 → ti∗2; l2; φ2.By Lemma Inversion on Rule Composition, Rule Const, and RuleCall-Indirect, we know that ti∗1 = ti∗0 ti∗3 and ti∗2 = ti∗0 ti∗4 for someti∗0, l1 = l)2, φ1 =⇒ φ3, and φ4 =⇒ φ2.136We know S ` stab(i, j) : tfi0 since it is a premise of ` s : S which wehave assumed to hold.Then, S; C ` call stab(i, j) : tfi0 by Rule Call-Cl.S; C ` call stab(i, j) : ti∗3; l1; φ3 → ti∗4; l2; φ4 by Rule Subtyping.Therefore, S; C ` call stab(i, j) : ti∗0 ti∗1; l1; φ1 → ti∗0 ti∗1; l2; φ2 by RuleStack-Poly.• Case: S; C ` (i32.const j) call indirect tfi : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ s; (i32.const j) call indirect tfi ↪→i trap.Trivially, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• Case: S; C ` vn call cl : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ s; vn call cl ↪→i localm {i; vn (t.const 0)k}block (; tin3 (t a)n; φ3, (t a)k, (= a (t 0))k→ tim4 ; l4; φ4)e∗endendwhere clcode = func (tin3 ; ; φ3 → tim4 ; l4; φ4) local tk e∗ and clinst = iLettfi0 = ti∗1; l1; φ1 → ti∗2; l2; φ2,tfi1 = ; tin3 (t a)n; φ3, (t a)k, (= a (t 0))k → tim4 ; l4; φ4, andtfi2 = tin3 ; ; φ3 → tim4 ; l4; φ4We want to show thatS; C `i localm {i; vn (t.const 0)k}block ; tin3 (t2 a2)n; φ3 → tim4 ; l4; φ4 e∗ endend: ti∗1; l1; φ1 → ti∗2; l2; φ2By Lemma Inversion on Rule Composition, Rule Const, and Rule137Call-Cl, we know l2 = l1, ti∗2 = ti∗1 tim4 , φ1, (t2 a2), (eq a2 (t2 c)) =⇒φ3, φ4 =⇒ φ2, and S ` cl : tfi1.We also know thatS; C ` (t2.const c)n : ti∗1; l1; φ1 → ti∗1 tin5 ; l1; φ1, (t2 a2), (= a2 (t2 c))where vn = (t2.const c)n, andS; C ` call cl : ti∗1 tin5 ; l1; φ1, (t2 a2)n, (= a2 (t2 c))n → ti∗ tim2 ; l2; φ2because they are premises of RuleComposition which we have assumedto hold.We have C ` func tfi2 local tk e∗ : tfi2 because it is a premise ofS ` cl : tfi2.Then,S; C, local tn2 tk, label (tim4 ; l4; φ4), return (tim4 ; l4; φ4) ` e∗ : tfi1because it is a premise of the above derivation.We can now reconstruct the type after reduction.S; C, local tn2 tk, return (tim4 ; l4; g4; φ4) ` block tfi1 e∗ end : tfi1 byRule Block.` v : (t2 a2); ◦, (t2 a2), (eq a2 (t2 c)))n by Rule Admin-Const, and(` (tconst 0) : (t a); ◦, (t a), (eq a (t 0)))k by Rule Admin-Const.Then, S; (tim4 ; l4; φ4) ` vn (tconst 0)k; block tfi2 e∗ end : tim4 ; l4; φ4by Rule Code.Recall that φ4 =⇒ φ2.Then, S; (tim4 ; l4; φ4) ` vn (tconst 0)k; block tfi2 e∗ end : tim4 ; l4; φ2by Rule Subtyping.S; C ` localm{j; vn (t.const 0)k} block tfi2 e∗ end end : ; l1; φ1 → tim4 ; l1; φ1, φ2 by Rule Local.138S; C ` localm{j; vn (t.const 0)k} block tfi2 e∗ end end : tfi0 by RuleStack-Poly.• Case: S; C ` localn{i; v∗l } trap end : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ localn{i; v∗l } trap end ↪→ trapTrivially, S; C ` trap : ti∗1; l1; φ1 → ti∗2; l2; φ2 by Rule Trap.• Case: S; C ` localn{i; v∗l } Lk[(t.const c)n return] end : ti∗1; l1; φ1 →ti∗2; l2; φ2∧ localn{i; v∗l } Lk[(t.const c)n return] end ↪→j (t.const c)nWe want to show that (t.const c)n : ti∗1; l1; φ1 → ti∗2; l2; φ2This proof is similar to the br case above, but with a few extra steps.First, we derive the type of (t.const c)n from the precondition of return.ti∗2 = ti∗1 tin, l1 = l2, S; (tin3 ; l2; φ3) `i v∗l ; Lk[(t.const c)n return] :tin3 ; l2; φ3, and φ1, φ3 =⇒ φ2 by Lemma Inversion on Rule Local.(` vl : til; φl)∗ and S; Cl ` Lk[(t.const c)n return] : ; ti∗l ; φ∗l →tin; l3; φ3, where Cl = Sinst(i), local t∗, return (tin; l3; φ3), becausethey are premises of Rule Code that we have assumed to hold.ti∗l = (tl al)∗ because it is a premise of Rule Admin-Const which wehave assumed to hold.By Lemma Inversion on Rule Composition and Rule Return,S; Cl ` (t.const c)n : ti∗4; l4; φ4 → tin3 ; l3; φ3, and S; Cl ` return :tin3 ; l3; φ3 → ti∗∅; l∅; φ∅.By Lemma Inversion on Rule Const, l4 = l3 and φ4, (t a)n, (=a (t c))n =⇒ φ3.Now we can show that (t.const c)n : ti∗1; l1; φ1 → ti∗2; l2; φ2We have S; C ` (t.const c)n : ; l3; φ4 → tin3 ; l3; φ4, (t a)n, (= a (t c))nby Rule Const.Then, S; C ` (t.const c)n : ; ti∗l ; φ∗l → tin3 ; l3; φ4, (t a)n, (= a (t c))nby Lemma Lift-Consts.139By Lemma Inversion on Rule Const, φ∗l =⇒ φ4. Further, since a∗lare fresh, ◦ =⇒ φ∗l .Thus, S; C ` (t.const c)n; ti∗l ; ◦ → tin3 ; l3; φ4, (t a)n, (= a (t c))n byRule Subtyping.We know then that (t a)n, (= a (t c))n =⇒ φ4, (t a)n, (= a (t c))n byLemma Inversion on Rule Const, and therefore that φ4 only containsconstraints on fresh variables.Then, S; C ` (t.const c)n : ; l1; φ1 → tin3 ; l1; φ1, (t a)n, (= a (t c))n byRule Const.Then, S; C ` (t.const c)n : ; l1; φ1 → tin3 ; l2; φ1, φ4, (t a)n, (= a (t c))n,S; C ` (t.const c)n : ; l1; φ1 → tin; l2; φ1, φ3, and finally S; C `(t.const c)n : ; l1; φ1 → tin; l2; φ2 by Rule Subtyping.Therefore, S; C ` (t.const c)n : ti∗1; l1; φ∗l → ti∗2; l2; φ2 by Rule Stack-Poly.• Case: S; C ` v (tee local j) : ti∗1; l1; φ1 → ti∗2; l2; φ2∧ v (tee local j) ↪→ v v (set local j)Note: We can include tee local here because it does not actually needto reason about locals since it gets reduced to a set local , so we onlyhave to do the reasoning in the set local case.We want to show that v v (set local j) : ti∗1; l1; φ1 → ti∗2; l2; φ2.As usual, we start by figuring out what ti∗1; l1; φ1 → ti∗2; l2; φ2 lookslike.By Lemma Inversion on Rule Composition, we know that S; C ` v :ti∗1; l1; φ1 → ti∗3; l3; φ3, and S; C ` tee local j : ti∗3; l3; φ3 → ti∗2; l2; φ2.By Lemma Inversion on Rule Tee-Local, we also know that ti∗3 =ti∗ (t a), ti∗2 = ti∗ (t a2), l2 = l3[j := (t a)], and φ3, (t a2), (= a2 a) =⇒φ2.Then, by Lemma Inversion on Rule Const, t.const c = v, ti∗1 = ti∗,l3 = l1, and φ1, (t a), (= a (t c)) =⇒ φ3.140Now, we can show that v v (set local j) : ti∗1; l1; φ1 → ti∗2; l2; φ2.We have S; C ` v v : ; l1; φ1 → (t a2) (t a); l1; φ1, (t a2), (=a2 (t c)), (t a), (= a (t c)) by Rule Const.We also have (t a2), (= a2 (t c)), (t a), (= a (t c)) =⇒ (t a2), (=a2 a), (t a), (= a (t c)) by =⇒ .Then, S; C ` v v : ; l1; φ1 → (t a2) (t a); l1; φ2 by Rule Subtyping.We have S; C ` set local j : (t a); l1; φ2 → ; l1[j := (t a)]; φ2 by RuleSet-Local.Therefore, S; C ` v v (set local j) : ti∗1; l1; φ1 → ti∗2; l2; φ2 by RuleComposition and Rule Stack-Poly.141
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NonCommercial-NoDerivatives 4.0 International
Graduate
An indexed type system for faster and safer WebAssembly
Text