The VLISP Image Builder

Vipin Swarup  William M. Farmer  Joshua D. Guttman
Leonard G. Monk  and John D. Ramsdell

The MITRE Corporation^{1} M92B096 September 1992

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. \begin{matrix}c \\ ◯ \end{matrix}1992 The MITRE Corporation. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the MITRE copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of the MITRE Corporation.

Abstract

The Verified Programming Language Implementation project has developed a formally verified implementation of the Scheme programming language. This report documents the image builder, which lays out a binary image for a program. It contains detailed proofs that the operational semantics of the resulting output matches the operational semantics of the input. iv

Contents

1 Introduction 1 1.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Stored Byte Code (SBC) 4

2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.1.3 Programs . . . . . . . . . . . . . . . . . . . . . . . . . 8

2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2.1 SBC State Machines (SBCM) . . . . . . . . . . . . . . 9 2.2.2 Operational Semantics of SBC Programs . . . . . . . . 24

3 Relating SBC and LBC 25 3.1 Relating Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 Relating Semantics . . . . . . . . . . . . . . . . . . . . . . . . 28

3.2.1 State Correspondence Relation . . . . . . . . . . . . . 28 3.2.2 Establishing State Correspondence . . . . . . . . . . . 33 3.2.3 Preserving State Correspondence . . . . . . . . . . . . 33 3.2.4 Correspondence of Final Answers . . . . . . . . . . . . 42 3.2.5 Correspondence of Semantics . . . . . . . . . . . . . . 42

4 The Image Builder Algorithm 44

5 Correctness of the Image Builder 55 5.1 Translating Constants . . . . . . . . . . . . . . . . . . . . . . 55 5.2 Translating Globals . . . . . . . . . . . . . . . . . . . . . . . . 57 5.3 Translating Templates . . . . . . . . . . . . . . . . . . . . . . 58 5.4 Translating Programs . . . . . . . . . . . . . . . . . . . . . . 60

References 62

1 Introduction

This report presents and justifies the vlisp translation from linked byte code to stored byte code. A Linked Byte Code (lbc) program is translated to a sequence of simple (unstructured) terms. This sequence is called a “store” since it corresponds to the store of a state machine. The translated programs are called Stored Byte Code (sbc) programs. A straightforward translation is all that is needed to map sbc programs to binary images that can be loaded into the store of a physical computer and executed. The program that translates lbc programs to binary images is the Image Builder. However, in this report, we shall refer to the program that translates lbcprograms to sbc programs as the image builder, and shall defer discussion of the translation of sbc programs to binary images to the vlisp report on the byte-code interpreter [4].

This report addresses the following issues:

1. lbc terms are tree structured whereas sbc terms have a flat structure. The translation from lbc to sbc consists of flattening the lbc terms and representing them by linked structures within a “store” (a store is a sequence of values). For example, the lbc term ⟨continuation t n a u k⟩ is represented in sbc as a “pointer” (i.e., index) into a store. This pointer identifies six locations of the store whose contents correspond to the representations of the six components of the lbc term.

Note that it is possible to create circular structures (e.g., circular lists) within a store (in the conventional way that circular linked lists are implemented). Thus, the correctness proof of this translation needs to deal with the fact that during execution of lbc and sbc programs, circular data structures may be created.

2. The memory of a physical computer is organized as a sequence of words, each word being a sequence of bytes. Some data (e.g. numbers) are represented by entire words, while others (e.g. characters and machine instruction opcodes) can be represented by bytes. The latter representation permits several characters (or opcodes) to be represented within a word, and hence results in smaller executable images. The image builder performs this storage optimization of packing several bytes into words. The correctness proof ensures that the optimization does not alter the operational semantics of programs.

This report presents:

1. the syntax and operational semantics of vlisp Stored Byte Code (sbc);

2. a correspondence relation that relates vlisp Stored Byte Code (sbc) programs and vlisp Linked Byte Code (lbc) programs;

3. a proof that the operational semantics of sbc is faithful to the operational semantics of lbc with respect to the above correspondence relation. That is, if an sbc program corresponds to an lbc program, then their respective operational semantics yield equal answers;

4. an image builder algorithm for translating lbc programs to sbc programs; and

5. a proof that the image builder translates lbc programs to corresponding sbc programs.

We do not reproduce the syntax and semantics of Linked Byte Code but refer the reader to the vlisp report that describes that language [1].

1.1 Notation

We will use the notation contained in Figure 1. Additional explanation of our notation can be found in the vlisp report [2].

⟨ … ⟩  finite sequence formation, commas optional
#s  length of sequence s
⟨ x … ⟩ sequence s with s(0) = x
⟨ … x ⟩ sequence s with s(#s − 1) = x
s^{⌢} t  concatenation of sequences s and t
Σ_{i=0}^{n−1}α_{i} concatenation of sequences α_{i} for 0 ≤ i < n
s † k  drop the first k members of sequence s
s ‡ k  the sequence of only the first k members of s
ρ[i ↦ x] the function which is the same as ρ

except that it takes the value x at i Figure 1: Some Notation

2 Stored Byte Code (SBC)

In this chapter, we present the syntax of the vlisp Stored Byte Code (sbc) and give it an (operational) semantics in a style very similar to the presentation of the vlisp Flattened Byte Code [3].

2.1 Syntax

The Stored Byte Code (sbc) provides an alternate (more “concrete”) representation of Linked Byte Code (lbc) terms. lbc represents objects such as environments, closures, and continuations as nested lists. sbc flattens all lbc terms and represents them within a “store”, where a store is a sequence of “cells” (which are defined below). An sbc term consists of a store together with an index into the store. For example, the lbc term ⟨continuation t n a u k⟩ is represented in sbc as an index (“pointer”) into a store. This pointer identifies six cells (“locations”) of the store that correspond to the representations of the six components of the lbc term.

2.1.1 Abstract Syntax

We express the syntax of sbc in Backus-Naur form (bnf). The terminal symbols of sbc are:

primitives: natural numbers (i.e., 0,1,2,…), booleans (i.e., #t and #f), and identifiers (i.e., alphanumeric symbols that begin with an alphabetic letter);

constructors: header, ptr, fixnum, imm, false, true, char, null, undefined, pair, symbol, string, vector, location, template, codevector;

keywords: empty, call, return, make-cont, literal, closure, global,
     local, set-global!, set-local!, push, make-env, make-restlist,
     unspecified, jump, jump-if-false, check-args=, check-args>=

symbols: “<”, “>”

The nonterminal symbols are as follows:

nat  for natural numbers,
bool  for booleans,
ident  for identifiers,
program for (sbc) programs,
term  for (sbc) terms,
store  for (sbc) stores,
cell  for (sbc) cells,
desc  for (sbc) descriptors,
vdesc  for (sbc) value descriptors,
imm  for (sbc) immediates,
htag  for (sbc) header tags,
bhtag  for (sbc) byte header tags,
dhtag  for (sbc) descriptor header tags,
byte  for (sbc) bytes,
loc  for (sbc) locations, and
obj  for (sbc) stored object data

We use extended bnf with productions having the form N ::= S_{1} | … | S_{n} where N is a nonterminal, and the S_{i}’s are possible forms for phrases in the set denoted by N. We use a variant of the conventional notation for repetition. We write S^{k} (where k is a nonnegative integer) to stand for the sequence ⟨SS … S⟩ containing k occurrences of S. We write S^{∗} to stand for the sequence ⟨SS …⟩ containing a finite number of occurrences of S (including, possibly, no occurrence of S).

We assume bpw to be some constant natural number; in the implementation, bpw will be either 1 or 4 (due to the architecture of the physical machines we shall be working with).

The abstract syntax of Stored Byte Code (sbc) is as follows:

program ::= term
term ::= ⟨store vdesc⟩
store ::= cell^{∗}
cell ::= desc | byte^{bpw}
desc ::= ⟨header htag bool nat⟩ | vdesc
vdesc ::= ⟨ptr loc⟩ | ⟨fixnum nat⟩ | ⟨imm imm⟩
imm ::= false | true | ⟨char nat⟩ | null | undefined
htag ::= bhtag | dhtag
bhtag ::= string | codevector

dhtag ::= pair | symbol | vector | location | template

    byte ::= nat | empty | call | return | make-cont | literal |

              closure | global | local | set-global! | set-local! |
              push | make-env | make-restlist | unspecified | jump |
              jump-if-false | check-args= | check-args>= | ident

loc ::= nat
obj ::= vdesc | byte

We will use i and m-like variables for natural numbers, p-like variables for booleans, and r-like variables for identifiers. Similarly for the other nonterminals, with

P  for (sbc) programs,
T  for (sbc) terms,
s  for (sbc) stores,
c  for (sbc) cells,
d  for (sbc) descriptors,
vd  for (sbc) value descriptors,
imm for (sbc) immediates,
h  for (sbc) header tags,
bh  for (sbc) byte header tags,
dh  for (sbc) descriptor header tags,
b  for (sbc) bytes,
l  for (sbc) locations, and
o  for (sbc) stored object data

We will define an sbc store in such a way that it can be viewed as a succession of stored objects. Each stored object is a sequence of cells, with the first cell being a header and the remaining cells being data. Stored objects are classified into two broad classes: descriptor objects and byte objects.

The data cells of descriptor objects are value descriptors, which are either constants (numbers, booleans, characters, etc.) or pointers to stored objects. A pointer is restricted to index the first data cell of some stored object. A header cell of a descriptor object has the form ⟨header dh p m⟩ where dh (the (descriptor) header tag) is a tag that describes the stored object, p (the mutability flag) is a boolean value that describes whether the object is mutable, and m (the header size) is a multiple of the number of value descriptors in the stored object, the multiple being the constant bpw.

The data cells of byte objects are fixed length sequences of bytes, bytes being numbers, keywords, or (special) identifiers. These sequences of bytes can be concatenated to obtain a single sequence of bytes. Only a prefix of this sequence is considered to be useful, and the bytes in this prefix are called useful bytes. A header cell of a byte object has the form ⟨header bh p m⟩ where bh (the (byte) header tag) is a tag that describes the stored object, p (the mutability flag) is a boolean value that describes whether the object is mutable, and m (the header size) is the number of useful bytes in the stored object.

We shall identify a stored object by the name of its header tag. Thus we call a stored object with header tag template to be a template. Templates, codevectors, and symbols are immutable and hence their immutability flag is always false (#f). Locations are always mutable, while pairs, strings, and vectors may be either mutable or immutable. Likewise, the header size of symbols is always 1 ∗ bpw, the header size of locations and pairs is always 2 ∗ bpw, and the header size of templates, codevectors, strings, and vectors varies.

An sbc term is an sbc store together with a value descriptor. If the value descriptor is a constant, then the store is irrelevant; otherwise, the value descriptor will be a pointer to a stored object in the store. An sbc program is an sbc term that consists of an sbc store and a pointer to a “template object” in the store.

The header of a stored object contains the object size in units of the number of bytes — we call this the size in bytes. The object size in units of cells (i.e., the size in cells) is obtained by means of a function ℧ that converts a size in bytes to a size in cells. Thus if a stored object’s header size is n, then the object consists of ℧(n) data cells. The function Ω converts a size in cells to a size in bytes. These functions use the constant bpw which represents the number of bytes per cell.

Definition 1 Let div be the integer division (i.e., quotient) operation. Then ℧ and Ω are functions (from natural numbers to natural numbers) defined as follows:

℧n =^{def} (n + bpw − 1) div bpw
Ωn =^{def} n ∗ bpw

2.1.2 Stores

A store s is represented as a sequence of cells. Thus #s is the domain of s, and is also the least l such that s(l) is not defined. s[l ↦ v] is the function whose domain is #s ∪ l and which is identical to s at all arguments except possibly l where its value is v. This is a store if and only if l ≤ #s. An sbc store is defined to be a store that satisfies the following invariants:

1. If s(l) = ⟨header h p m⟩ for some l, h, p, m, then for all 1 ≤ x ≤ ℧m,

• If h ∈ bhtag, then s(l + x) = ⟨b_{1} … b_{bpw}⟩ for some b_{1} … b_{bpw},

• If h ∈ dhtag, then s(l + x) = vd for some vd;

2. For all l such that s(l) is defined,

s(l)(1) ≠ header ⇒

(∃l′, h, p, m) \begin{matrix}(s(l′) = ⟨header h p m⟩)∧ \\ (l′ < l ≤ l′ + ℧m) \end{matrix}

3. If s(l) = ⟨ptr l′⟩ for some l, l′, then s(l′ − 1) = ⟨header h p m⟩ for some h, p, m.

These invariants ensure that the store is a succession of stored objects. Thus every header cell in the store is the header of a stored object and should be followed by the appropriate number and kind of data cells (invariant 1), every non-header cell in the store is a data cell of some stored object (invariant 2), and every pointer cell is a pointer to the first data cell of a stored object (invariant 3).

2.1.3 Programs

An sbc program is defined to be a term ⟨s vd⟩ such that

1. s is an sbc store;

2. all location objects have undefined values. That is, if s(l − 1) = ⟨header location #t 2 ∗ bpw⟩, then s(l) = ⟨imm undefined⟩; and

3. vd is a pointer to a template object in the store s, i.e., vd = ⟨ptr l⟩ and s(l−1) = ⟨header template #f m⟩ for some l, m. vd represents the root template of the program.

2.2 Semantics

In this section, we define the operational semantics of stored byte code as a deterministic state machine with concrete states. The state machine is called the Stored Byte Code Machine (sbcm).

2.2.1 SBC State Machines (SBCM)

We define the syntax of sbc States by augmenting the syntax of the Stored Byte Code. We then define the states and action rules of a deterministic state machine. We adopt the notation and conventions presented in the vlisp Flattener report [3].

Augmented Stored Byte Code (ASBC) The Augmented Stored Byte Code (asbc) provides the syntactic objects that form the states of the sbcm. It expands the sbc to provide representations of objects such as environments, closures, continuations, etc. These objects are not part of sbc as they do not occur in the code obtained by compiling Scheme programs; they are put in the initial state of the sbcm and are also generated during the course of computation.

We distinguish between asbc and sbc for two reasons. First, sbc is the representation language of the image builder’s output. We shall identify a small collection of primitives that permit sbc programs to be constructed. The image builder shall use these primitives to manipulate sbc programs. By changing the specification and implementation of these primitives, we shall be able to change the representation language of the image builder’s output.

Second, the vlisp byte code interpreter [4] is derived via a sequence of state machines, each of which is a refinement of the previous. Each state machine shall provide an alternate definition of the operational semantics of sbc programs. Thus sbc shall be a common sublanguage of each state machine, while the augmented languages of each machine shall vary.

Abstract Syntax The new asbc tokens are as follows:

constructors: unspecified, empty-env, halt, eof, closure, port, continuation, environment

The new asbc syntactic categories are:

t for (asbc) templates,
n for (asbc) offsets,
c for (asbc) codevectors,
v for (asbc) values,
u for (asbc) environments,
k for (asbc) continuations,
a for (asbc) argument stacks,

The abstract syntax of Augmented Stored Byte Code (asbc) is defined below. This grammar redefines several syntactic categories of sbc. However, the extensions of these syntactic categories include the extensions of the sbc syntactic categories.

program ::= term
term ::= ⟨store vdesc⟩
store ::= cell^{∗}
cell ::= desc | byte^{bpw}
desc ::= ⟨header htag bool nat⟩ | vdesc
vdesc ::= ⟨ptr loc⟩ | ⟨fixnum nat⟩ | ⟨imm imm⟩
imm ::= false | true | ⟨char nat⟩ | null | undefined

unspecified | empty-env | halt | eof

htag ::= bhtag | dhtag
bhtag ::= string | codevector
dhtag ::= pair | symbol | vector | location | template |

closure | port | continuation | environment

byte ::= nat | empty | call | return | make-cont | literal |

closure | global | local | set-global! | set-local! |
push | make-env | make-restlist | unspecified | jump |
jump-if-false | check-args= | check-args>= | ident

loc ::= nat
obj ::= vdesc | byte
stack ::= vdesc^{∗}

We extend the naming conventions of sbc for variables. Thus, we will use m-like variables for natural numbers, p-like variables for booleans, and r-like variables for identifiers. Similarly for the other nonterminals, with

P  for (asbc) programs,
T  for (asbc) terms,
s  for (asbc) stores,
c  for (asbc) cells,
d  for (asbc) descriptors,
vd  for (asbc) value descriptors,
imm for (asbc) immediates,
h  for (asbc) header tags,
bh  for (asbc) byte header tags,
dh  for (asbc) descriptor header tags,
b  for (asbc) bytes,
l  for (asbc) locations,
o  for (asbc) stored object data, and
a  for (asbc) stacks

In addition, we will use t, c, v, u, and k-like variables for (asbc) value descriptors, and n-like variables for natural numbers.

Stores An asbc store is defined to be a store that satisfies the following invariants:

1. If s(l) = ⟨header h p m⟩ for some l, h, p, m, then for all 1 ≤ x ≤ ℧m,

• If h ∈ bhtag, then s(l + x) = ⟨b_{1} … b_{bpw}⟩ for some b_{1} … b_{bpw},

• If h ∈ dhtag, then s(l + x) = vd for some vd;

2. For all l such that s(l) is defined,

s(l)(1) ≠ header ⇒

(∃l′, h, p, m) \begin{matrix}(s(l′) = ⟨header h p m⟩)∧ \\ (l′ < l ≤ l′ + ℧m) \end{matrix}

3. If s(l) = ⟨ptr l′⟩ for some l, l′, then s(l′ − 1) = ⟨header h p m⟩ for some h, p, m.

These invariants ensure that the store is a succession of stored objects. Thus every header cell in the store is the header of a stored object and should be followed by the appropriate number and kind of data cells (invariant 1), every non-header cell in the store is a data cell of some stored object (invariant 2), and every pointer cell is a pointer to the first data cell of a stored object (invariant 3). Note that every sbc store is also an asbc store.

Stored Objects An asbc store may be viewed as a succession of stored objects. Each stored object is a sequence of cells, with the first cell being a header and the remaining cells being data. A stored object is always identified by the location of its first data cell. If l is a location such that s(l) is the first data cell of a stored object, then ⟨ptr l⟩ is called a pointer to the stored object in asbc store s.

Let d be a pointer into asbc store s. Then S(d, s) is defined to be a sequence of the contents of the stored object pointed to by d in s. The first element of this sequence is the header tag, the second element is the mutability flag, and the remaining elements are the data elements of the object. Note that the sequences of bytes within a byte object are flattened into a single byte sequence; this resulting sequence may be larger than the object size, so the extra bytes are truncated from the end of the sequence. The result is the sequence of “useful” bytes in the stored object.

Definition 2 For all d, s, h, p, m, o^{∗}, l such that s(l +_{A} (℧m − 1)) is defined,

S(d, s) =^{def} ⟨h p o^{∗}⟩ if

• d = ⟨ptr l⟩

• s(l − 1) = ⟨header h p m⟩

• if h ∈ dhtag then

o^{∗} = ⟨s(l) … s(l + (℧m − 1))⟩ else

o^{∗} = (s(l)^{⌢} …^{⌢} s(l + (℧m − 1))) ‡ m

The following notation provides a concise way of appending stored objects to asbc stores. Definition 3

s > ⟨h p o^{∗}⟩ =^{def} if h ∈ dhtag then s^{⌢} ⟨⟨header h p (Ω#o^{∗})⟩⟩^{⌢} o^{∗} else s^{⌢} ⟨⟨header h p #o^{∗}⟩⟩^{⌢} o^{′∗} where #o^{′∗} = ℧#o^{∗}, and (∀0 ≤ i < #o^{′∗}) #o^{′∗}(i) = bpw and o^{∗} = (o^{′∗}(1)^{⌢} …^{⌢} o^{′∗}(#o^{′∗} − 1)) ‡ #o^{∗}

The following lemma asserts that appending a stored object to an asbc store s results in a new asbc store s′ such that ⟨ptr (#s + 1)⟩ is a pointer to that stored object in s′.

Lemma 4 S(⟨ptr (#s + 1)⟩, s > ⟨h p o^{∗}⟩) = ⟨h p o^{∗}⟩

Proof: Immediate from definitions.

□

Predicates We define a family of predicates that characterize the types of stored objects in an asbc store. These predicates are defined recursively and are presented in Figure 2.

Let d, t, c, v, u, k range over value descriptors. The free variables in each formula are (implicitly) existentially quantified over the entire formula. Thus, for example,

String(d, s) =^{def} S(d, s) = ⟨string p b^{∗}⟩

means

String(d, s) =^{def} (∃p, b^{∗}) (S(d, s) = ⟨string p b^{∗}⟩).

States The states of a stored byte code state machine (sbcm) are the sequences of the form

⟨t, n, c, v, a, u, k, s⟩

that satisfy the following (sbcm) state invariants:

1. s is an asbc store

2. Template(t, s)

3. Codevector(c, s)

4. S(t, s) = ⟨template #f c::o^{∗}⟩

5. Offset(n, t, s)

6. Value(v, s)

Pair(d, s)  ⟺ S(d, s) = ⟨pair p ⟨o_{1} o_{2}⟩⟩

and Value(o_{1}, s) and Value(o_{2}, s)

Symbol(d, s)  ⟺ S(d, s) = ⟨symbol #f ⟨o⟩⟩ and String(o, s)
String(d, s)  ⟺ S(d, s) = ⟨string p b^{∗}⟩
Vector(d, s)  ⟺ S(d, s) = ⟨vector p o^{∗}⟩

and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

Location(d, s)  ⟺ S(d, s) = ⟨location #t ⟨o_{1} o_{2}⟩⟩

and Value(o_{1}, s) and Symbol(o_{2}, s)

Template(t, s)  ⟺ S(t, s) = ⟨template #f c::o^{∗}⟩

and Codevector(c, s) and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

or Location(o^{∗}(i), s)

or Template(o^{∗}(i), s)
Codevector(c, s)  ⟺ S(c, s) = ⟨codevector #f b^{∗}⟩
Offset(n, t, s)  ⟺ Template(t, s)

and S(t, s) = ⟨template #f c::o^{∗}⟩ and S(c, s) = ⟨codevector #f b^{∗}⟩ and 0 ≤ n < #b^{∗}

Closure(d, s)  ⟺ S(d, s) = ⟨closure #f ⟨t u⟩⟩

and Template(t, s) and Environment(u, s)

Continuation(k, s) ⟺ k = ⟨imm halt⟩ or

S(k, s) = ⟨continuation #f ⟨t n u k⟩^{⌢} vd^{∗}⟩ and Template(t, s) and Offset(n, t, s) and Environment(u, s) and Continuation(k, s) and (∀0 ≤ i < #vd^{∗}) Value(vd^{∗}(i), s)

Environment(u, s) ⟺ u = ⟨imm empty-env⟩ or

S(u, s) = ⟨environment #t u′::o^{∗}⟩ and Environment(u′, s) and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

Value(v, s)  ⟺ v = ⟨fixnum n⟩ or v = ⟨imm imm⟩

or S(v, s) is defined

Figure 2: Predicates for Stored Objects 7. Environment(u, s)

8. Continuation(k, s)

9. (∀0 ≤ i < #a) Value(a(i), s) ∨ Environment(a(i), s)

The components of a state are called, in order, its template, offset, codevector, value, argument stack, environment, continuation, and store, and we may informally speak of them as being held in registers. The first invariant ensures that the store is an asbc store. The remaining invariants restrict the values of the register components of states. For example, the register t is restricted to hold pointers to templates (i.e., stored objects with header tag template).

Initial and Halt States The initial states ⟨t, n, c, v, a, u, k, s⟩ are the states such that

• n = 0,

• v = ⟨imm unspecified⟩,

• a = ⟨⟩,

• u = ⟨imm empty-env⟩, and

• k = ⟨imm halt⟩

The halt states ⟨t, n, c, v, a, u, k, s⟩ are the states such that for some b^{∗},

• S(c, s) = ⟨codevector #f b^{∗}⟩,

• b^{∗}(n) = return, and

• k = ⟨imm halt⟩

Actions We present actions as the union of subfunctions called (action) rules. The action rules are functions from pairwise disjoint subsets of states × inputs × outputs into states × inputs × outputs where states is the set of sbcm states, and inputs and outputs are sets of finite sequences of characters. Since the domains of these functions are disjoint, the union of these functions is a partial function from states × inputs × outputs into states × inputs × outputs. We denote this function by R.

Let Σ, i^{∗}, and o^{∗} be a state, input sequence, and output sequence respectively. The value of the function R at ⟨Σ, i^{∗}, o^{∗}⟩ only depends on Σ and possibly on the first element of i^{∗}. Let R(⟨Σ, i^{∗}, o^{∗}⟩) = ⟨Σ′, i^{′∗}, o^{′∗}⟩. Then, one of the following hold:

• The input and output sequences are unchanged, i.e., i^{′∗} = i^{∗} and o^{′∗} = o^{∗}. We call such rules pure rules.

• The rule drops the first element of the argument input sequence, i.e., i^{′∗} = i^{∗} † 1 and o^{′∗} = o^{∗}. We call such rules input port rules.

• The rule appends a sequence of values to the argument output sequence, i.e., i^{′∗} = i^{∗} and o^{′∗} = o^{∗} ^{⌢} o^{′′∗}. We call such rules output port rules.

We define a function R^{∗} as follows:

R^{∗} =^{def} R^{∗}(R(⟨Σ, i^{∗}, o^{∗}⟩)) if R(⟨Σ, i^{∗}, o^{∗}⟩) is defined
⟨Σ, i^{∗}, o^{∗}⟩  otherwise

If, when started in state ⟨Σ, i^{∗}, o^{∗}⟩, the state machine halts, then R^{∗}(⟨Σ, i^{∗}, o^{∗}⟩) is defined and is the state the machine halts in. Otherwise, R^{∗}(⟨Σ, i^{∗}, o^{∗}⟩) is undefined.

In the remainder of this report, we shall only consider pure action rules. By abuse of notation, we shall consider R and R^{∗} to be functions from states to states. We now present a few auxiliary functions, then present the pure action rules.

Auxiliary Functions The function env-frame(u, n, s) returns the environment that is nested n levels deep within the environment pointed to by u in asbc store s.

env-lookup(u, m, s) =^{def} l + m if u = ⟨ptr l⟩ and S(u, s) = ⟨environment #t u′::vd^{∗}⟩

env-frame(u, 0, s) =^{def} u, and
env-frame(u, n + 1, s) =^{def} env-frame(u′, n, s) if S(u, s) = ⟨environment #t u′::vd^{∗}⟩

The function stack-to-list(lp, n, a, s) pops the first n values of a stack a and stores them as a linked list in asbc store s. The tail of this linked list is the list pointed to by lp in asbc store s. The function returns a pointer to the new linked list, together with the modified stack and asbc store.

stack-to-list(lp, 0, a, s) =^{def} ⟨lp a s⟩, and
stack-to-list(lp, n + 1, a, s) =^{def}
stack-to-list(⟨ptr #s + 1⟩, n, a † 1, s > ⟨pair #f ⟨a(0) lp⟩⟩)

The (partial) function list-to-stack(p, a, s) returns the stack a′ ^{⌢} a, where a′ is the stack (if any) represented by the linked list pointed to by p in asbc store s.

list-to-stack(⟨imm null⟩, a, s) =^{def} a, and
list-to-stack(p, a, s) =^{def} list-to-stack(p′, v :: a, s) if S(p, s) = ⟨pair p ⟨v p′⟩⟩

The function compute-offset takes two integers and returns an integer representing an offset they are together encoding. For 0 ≤ n_{0}, n_{1},

compute-offset(n_{0}, n_{1}) =^{def} (256 ∗ n_{0}) + n_{1}.

We will usually write n_{0} ⊗ n_{1} for compute-offset(n_{0}, n_{1}).

Pure Rules We adopt the presentation format for pure action rules that is described in the VLISP Flattener report [3]. We reproduce that description below with minor variations.

For each pure rule we give a name, one or more conditions determining when the rule is applicable (and possibly introducing new locally bound variables for later use), and a specification of the new values of some registers. Often the domain is specified by equations giving “the form” of certain registers, especially the code. In all specifications, the original values of the various registers are designated by conventional variables used exactly as in the above definition of a state: t, n, c, v, a, u, k, and s. Call these the original register variables. The new values of the registers are indicated by the same variables with primes attached: t′, n′, c′, v′, a′, u′, k′, and s′. Call these the new register variables. New register variables occur only as the left hand sides of equations specifying new register values. Registers for which no new value is given are tacitly asserted to remain unchanged. Input and output must both be null. We use the following two auxiliary functions. Let S(c, s) = ⟨codevector #f b^{∗}⟩ for some c, s, b^{∗}. Then,

current inst(n, c, s) =^{def} b^{∗}(n)
current inst param(n, i, c, s) =^{def} b^{∗}(n + i)

It may help to be more precise about the use of local bindings derived from pattern matching. The domain conditions may involve the original register variables and may introduce new variables (not among the new or old register variables). If we call these new, “auxiliary” variables x_{1}, …, x_{j}, then the domain conditions define a relation of j + 8 places

(†) R(t, n, c, v, a, u, k, s, x_{1}, …, x_{j}).

The domain condition really is this: the rule can be applied in a given state if there exist x_{1}, …, x_{j} such that (†). Furthermore, in the change specifications we assume for these auxiliary variables a local binding such that (†). Independence of the new values on the exact choice (if there is any choice) of the local bindings will be unproblematic.

Rule 1: return Domain conditions:

current inst(n, c, s) = return

k = halt Changes:

Halt in final state Σ

Rule 2: return Domain conditions:

current inst(n, c, s) = return

S(k, s) = ⟨continuation #f ⟨t_{1} n_{1} u_{1} k_{1}⟩^{⌢} a_{1}⟩ S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩ n_{1} = ⟨fixnum m⟩

Changes:

t′ = t_{1}

c′ = c_{1}
n′ = m
a′ = a_{1}
u′ = u_{1}
k′ = k_{1}

Rule 3: call m Domain conditions:

current inst(n, c, s) = call current inst param(n, 1, c, s) = m S(v, s) = ⟨closure #f ⟨t_{1} u_{1} d_{1}⟩⟩ S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩

Changes:

\begin{matrix}t′ = t_{1} \\ c′ = c_{1} \\ n′ = 0 \\ u′ = u_{1} \end{matrix}

Rule 4: jump-if-false m_{1} m_{2} Domain conditions:

current inst(n, c, s) = jump-if-false current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} v ≠ ⟨imm false⟩

Changes:

n′ = n + 3

Rule 5: jump-if-false m_{1} m_{2} Domain conditions:

current inst(n, c, s) = jump-if-false current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} v = ⟨imm false⟩

Changes:

n′ = n + 3 + (m_{1} ⊗ m_{2})

Rule 6: jump m_{1} m_{2} Domain conditions:

current inst(n, c, s) = jump current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2}

Changes:

n′ = n + 3 + (m_{1} ⊗ m_{2})

Rule 7: make-cont m_{1} m_{2} m_{3} Domain conditions:

current inst(n, c, s) = make-cont current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} current inst param(n, 3, c, s) = m_{3} m = n + 4 + (m_{1} ⊗ m_{2})

Changes:

n′ = n + 4 a′ = ⟨⟩ k′ = ⟨ptr #s + 1⟩ s′ = s > ⟨continuation #f ⟨t ⟨fixnum m⟩ u k⟩^{⌢} a⟩

Rule 8: literal m Domain conditions:

current inst(n, c, s) = literal current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m)

Changes:

\begin{matrix}n′ = n + 2 \\ v′ = o_{m} \end{matrix}

Rule 9: closure m Domain conditions:

current inst(n, c, s) = closure current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) S(o_{m}, s) = ⟨template #f c_{1}::o_{1}^{∗}⟩

Changes:

n′ = n + 2 v′ = ⟨ptr (#s + 1)⟩ s′ = s > ⟨closure #f ⟨o_{m} u ⟨imm unspecified⟩⟩⟩ Rule 10: global m Domain conditions:

current inst(n, c, s) = global current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) S(o_{m}, s) = ⟨location #t ⟨v_{1} x⟩⟩ v_{1} ≠ ⟨imm undefined⟩

Changes:

\begin{matrix}n′ = n + 2 \\ v′ = v_{1} \end{matrix}

Rule 11: set-global! m Domain conditions:

current inst(n, c, s) = set-global! current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) = ⟨ptr l⟩ S(o_{m}, s) = ⟨location #t ⟨v_{1} x⟩⟩

Changes:

n′ = n + 2 s′ = s[l ↦ v] v′ = ⟨imm unspecified⟩

Rule 12: local m_{1} m_{2} Domain conditions:

current inst(n, c, s) = local current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} l = env-lookup(env-frame(u, m_{1}, s), m_{2}, s) v_{1} = s(l) v_{1} ≠ ⟨imm undefined⟩

Changes:

\begin{matrix}n′ = n + 3 \\ v′ = v_{1} \end{matrix}

Rule 13: set-local! m_{1} m_{2} Domain conditions:

current inst(n, c, s) = set-local! current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} l = env-lookup(env-frame(u, m_{1}, s), m_{2}, s)

Changes:

n′ = n + 3 v′ = ⟨imm unspecified⟩ s′ = s[l ↦ v]

Rule 14: push Domain conditions:

current inst(n, c, s) = push Changes:

\begin{matrix}n′ = n + 1 \\ a′ = v::a \end{matrix}

Rule 15: make-env m Domain conditions:

current inst(n, c, s) = make-env current inst param(n, 1, c, s) = m m = #a

Changes:

n′ = n + 2 a′ = ⟨⟩ u′ = ⟨ptr (#s + 1)⟩ s′ = s > ⟨environment #t u::a⟩ Rule 16: make-rest-list m Domain conditions:

current inst(n, c, s) = make-rest-list current inst param(n, 1, c, s) = m #a ≥ m ⟨v_{1} a_{1} s_{1}⟩ = stack-to-list(⟨imm null⟩, (#a − m), a, s)

Changes:

\begin{matrix}n′ = n + 2 \\ v′ = v_{1} \\ a′ = a_{1} \\ s′ = s_{1} \end{matrix}

Rule 17: unspecified Domain conditions:

current inst(n, c, s) = unspecified Changes:

n′ = n + 1 v′ = ⟨imm unspecified⟩

Rule 18: check-args= m Domain conditions:

current inst(n, c, s) = check-args= current inst param(n, 1, c, s) = m #a = m

Changes:

n′ = n + 2

Rule 19: check-args>= m Domain conditions:

current inst(n, c, s) = check-args>= current inst param(n, 1, c, s) = m #a ≥ m

Changes:

n′ = n + 2 Rule 20: primitive-throw Domain conditions:

current inst(n, c, s) = primitive-throw

S(v, s) = ⟨continuation #f ⟨t_{1} n_{1} u_{1} k_{1}⟩^{⌢} a_{1}⟩ Changes:

\begin{matrix}n′ = n + 1 \\ k′ = v \end{matrix}

2.2.2 Operational Semantics of SBC Programs

The sbcm Loader L_{sbcm} is defined to be a partial function that maps sbc programs to sbcm initial states such that:

L_{sbcm}(⟨s t⟩) =^{def} ⟨t, 0, c, ⟨imm unspecified⟩, ⟨⟩,

⟨imm empty-env⟩, ⟨imm halt⟩, s⟩ if S(t, s) = ⟨template #f c::o^{∗}⟩.

Note that sbcm initial states are asbc terms, and hence the loader involves coercing sbc terms to asbc terms. This coercion is trivial since every sbc term is also an asbc term. The sbcm Answer A_{sbcm} is defined to be a partial function that maps sbcm halt states to natural numbers such that:

A_{sbcm}(⟨t, n, c, v, a, u, k, s⟩) =^{def} m  if v = ⟨fixnum m⟩

Definition 5 Let P be an sbc program. Then L_{sbcm}(P) is an initial state of the sbcm. If R_{sbcm}^{∗}(L_{sbcm}(P)) is defined, then the meaning of program P as given by the sbc operational semantics is

O_{sbcm}[[P]] =^{def} A_{sbcm}(R_{sbcm}^{∗}(L_{sbcm}(P)))

Otherwise O_{sbcm}[[P]] is undefined.

3 Relating SBC and LBC

In this chapter, we define a correspondence relation between vlisp Stored Byte Code (sbc) programs and vlisp Linked Byte Code (lbc) programs. We prove that the operational semantics of vlisp Stored Byte Code (sbc) is faithful to the operational semantics of vlisp Linked Byte Code (lbc) with respect to this correspondence relation. That is, if an sbc program corresponds to an lbc program, then their respective operational semantics yield equal answers.

We adopt the concept and notation of storage relations [5] in defining program, term, and state correspondence relations. However, since we need to relate structures that may be circular, we modify their technique so that we can prove the correctness of storage representations for circular structures. We cannot merely take the greatest fixpoint of relations defined in the style of Oliva and Wand, since primitives like the Scheme standard procedure “eq?” distinguish between objects that have identical structure but are represented at different locations within the store.

3.1 Relating Syntax

Let p = ⟨n constants::c^{∗} global-variables::n^{∗}⟩^{⌢} t^{∗} be an lbc program, where c^{∗}, n^{∗}, and t^{∗} are lbc constant, global, and template tables respectively, and n is an index into t^{∗} (t^{∗}(n) represents the “root” template of the program). We shall use an alternate syntax for lbc programs in this report and shall represent p by ⟨m^{L} η_{c}^{L} η_{g}^{L} η_{t}^{L}⟩, where m^{L} = n, η_{c}^{L} = c^{∗}, η_{g}^{L} = n^{∗}, and η_{t}^{L} = t^{∗}. Let s^{L} be a sequence of length #s^{L} = #η_{g}^{L}.

Let ⟨s vd⟩ be an sbc program where s is an sbc store and vd is a pointer to a template object in the store s. vd represents the “root” template of the program.

We define a relation ≃^{p} (called a program correspondence) that relates lbc and sbc programs by relating constants, globals, and templates by another relation (called a term correspondence). ≃^{p} only relates programs that have the same semantics. Now the semantics of lbc considers the globals in η_{g}^{L} to be distinct from each other. Thus, the term correspondence relation needs to be one-to-one between the globals of related lbc and sbc programs. This is formalized by defining a 1-to-1 relation between a subset of dom(s^{L}) and a subset of dom(s). Each lbc global is associated with a unique location in dom(s^{L}). Similarly, each sbc global is associated with a unique location in dom(s). The term correspondence relation relates globals only if their associated locations are related by the 1-to-1 location correspondence.

If ≃ is a four-place relation, we write (s^{L}, s ⊢ x^{L} ≃ x) to mean that (s^{L}, x^{L}, s, x) is in the relation ≃. We first define a relation between locations in s^{L} and locations in s. This relation relates locations that are associated with globals.

Definition 6 A location correspondence ≃_{0} ⊆ (s^{L} × l^{L}) × (s × l) is defined to be a relation such that for all s^{L}, s, the set {(l^{L}, l) | (s^{L}, s ⊢ l^{L} ≃_{0} l)} is a 1-to-1 relation between a subset of dom(s^{L}) and a subset of dom(s). Further, if (s^{L}, s ⊢ l^{L} ≃_{0} l) then s(l − 1) = ⟨header location #t 2⟩.

We extend the relation between locations to a relation between lbc and sbc terms.

Definition 7 Let ≃_{0} ⊆ (s^{L} × l^{L}) × (s × l) be a location correspondence relation. Let η_{c}^{L}, η_{g}^{L}, and η_{t}^{L} be lbc constant, global, and template tables respectively. A term correspondence ≃ ⊆ (s^{L} × (t^{L} + w^{L} + o^{L} + r^{L} + v^{L})) × (s × vd) is defined as follows. The definition is by induction on the size of the second argument, i.e., the lbc term. Notationally, this is the first term after the turnstile.

1. (s^{L}, s ⊢ t^{L} ≃ t) if

(a) S(t, s) = ⟨template #f c::o^{∗}⟩

(b) t^{L} = ⟨template w^{L} e^{L}⟩

(c) (s^{L}, s ⊢ w^{L} ≃ c)

(d) #e^{L} = #(c::o^{∗})

(e) (∀0 ≤ i < #o^{∗}) (s^{L}, s ⊢ (e^{L} † 1)(i) ≃ o^{∗}(i))

2. (s^{L}, s ⊢ w^{L} ≃ c) if

(a) S(c, s) = ⟨codevector #f b^{∗}⟩

(b) w^{L} = b^{∗}

3. (s^{L}, s ⊢ o^{L} ≃ d) if

• (a) o^{L} = ⟨constant i⟩ (b) η_{c}(i) = c^{L}

(c) (s^{L}, s ⊢ c^{L} ≃ d)

• (a) o^{L} = ⟨global-variable i⟩

(b) r^{L} = η_{c}^{L}(η_{g}^{L}(i))

(c) l^{L} = i

(d) d = ⟨ptr l⟩

(e) S(d, s) = ⟨location #t ⟨v_{1} v_{2}⟩⟩

(f) (s^{L}, s ⊢ l^{L} ≃_{0} l)

(g) (s^{L}, s ⊢ r^{L} ≃ v_{2})

• (a) o^{L} = ⟨template i⟩ (b) η_{t}(i) = t^{L}

(c) (s^{L}, s ⊢ t^{L} ≃ d)

4. (s^{L}, s ⊢ r^{L} ≃ d) if

(a) S(d, s) = ⟨symbol #f ⟨d′⟩⟩

(b) S(d′, s) = ⟨string #f b^{∗}⟩

(c) char→int^{∗}(symbol→string(r^{L})) = b^{∗}

5. (s^{L}, s ⊢ v^{L} ≃ v) if

• (a) v^{L} = ⟨immutable-pair m_{1}^{L} m_{2}^{L}⟩ (b) S(v, s) = ⟨pair #f ⟨v_{1} v_{2}⟩⟩

(c) (s^{L}, s ⊢ η_{c}^{L}(m_{1}^{L}) ≃ v_{1})

(d) (s^{L}, s ⊢ η_{c}^{L}(m_{2}^{L}) ≃ v_{2})

• (a) v^{L} = ch^{L∗} (b) S(v, s) = ⟨string #f b^{∗}⟩

(c) char→int^{∗}(ch^{L∗}) = b^{∗}

• (a) v^{L} = immutable-vector::m^{L∗}

(b) S(v, s) = ⟨vector #f v^{′∗}⟩

(c) #m^{L∗} = #v^{′∗}

(d) (∀0 ≤ i < #m^{L∗}) (s^{L}, s ⊢ η_{c}^{L}(m^{L∗}(i)) ≃ v^{′∗}(i))

• (a) v^{L} = m (a number)

(b) v = ⟨fixnum m⟩

• (a) v^{L} = #f (b) v = ⟨imm false⟩

• (a) v^{L} = #t

(b) v = ⟨imm true⟩

• (a) v^{L} = ch (a character) (b) v = ⟨imm ⟨char char→int(ch)⟩⟩

• (a) v^{L} = nil (b) v = ⟨imm null⟩

We define an lbc program to be related to an sbc program if their root templates are related by a term correspondence:

Definition 8 A program correspondence relation ≃^{p}⊂ (lbc programs × sbc programs) is defined as follows:

⟨m^{L} η_{c}^{L} η_{g}^{L} η_{t}^{L}⟩ ≃^{p} ⟨s vd⟩

if there exists a location correspondence ≃_{0}, and a term correspondence ≃ induced by ≃_{0}, such that (s^{L}, s ⊢ η_{t}^{L}(m^{L}) ≃ vd) where s^{L} = undefined^{∗} and #s^{L} = #η_{g}^{L}.

3.2 Relating Semantics

We prove that programs related by the program correspondence relation have the same semantics. We proceed by first extending the program correspondence relation to a correspondence relation between lbcm and sbcm states. We then show that the lbcm and sbcm Loaders map related programs to related states. We prove that the lbcm and sbcm action rules preserve the state correspondence relation, and that the final answer functions map related states to the same natural number.

3.2.1 State Correspondence Relation

In Section 3.1, we presented location, term, and program correspondence relations between lbc and sbc locations, terms, and programs respectively. We extend these to correspondence relations between albc and asbc locations, terms, and states.

Definition 9 An augmented location correspondence ≃_{0} ⊆ (s^{L}×l^{L})×(s×l) is defined to be a relation such that for all s^{L}, s, the set {(l^{L}, l) | (s^{L}, s ⊢ l^{L} ≃_{0} l)} is a 1-to-1 relation between a subset of dom(s^{L}) and a subset of dom(s); further, if (s^{L}, s ⊢ l^{L} ≃_{0} l) then there exists an l′ ∈ dom(s) such that s(l′ − 1) = ⟨header h p m⟩ and one of the following hold:

• h = location and l = l′

• h = pair and l′ ≤ l < l′ + 2

• h = string and l = l′

• h = vector and l′ ≤ l < l′ + ℧m

• h = closure and l = l′ + 2

• h = environment and l′ + 1 ≤ l < l′ + ℧m

Definition 10 Let ≃_{0} ⊆ (s^{L} × l^{L}) × (s × l) be an augmented location correspondence relation. An augmented term correspondence ≃ ⊆ (s^{L} × (t^{L} + w^{L} + o^{L} + i^{L} + v^{L} + u^{L} + a^{L} + k^{L})) × (s × vd) is defined as follows. The definition is by induction on the size of the second argument, i.e., the albc term. Notationally, this is the first term after the turnstile. Note that clauses 1–4 and the first eight subclauses of clause 5 are identical to those in the definition of a term correspondence.

1. (s^{L}, s ⊢ t^{L} ≃ t) if

(a) S(t, s) = ⟨template #f c::o^{∗}⟩

(b) t^{L} = ⟨template w^{L} e^{L}⟩

(c) (s^{L}, s ⊢ w^{L} ≃ c)

(d) #e^{L} = #(c::o^{∗})

(e) (∀0 ≤ i < #o^{∗}) (s^{L}, s ⊢ (e^{L} † 1)(i) ≃ o^{∗}(i))

2. (s^{L}, s ⊢ w^{L} ≃ c) if

(a) S(c, s) = ⟨codevector #f b^{∗}⟩

(b) w^{L} = b^{∗}

3. (s^{L}, s ⊢ o^{L} ≃ d) if

• (a) o^{L} = ⟨constant i⟩ (b) η_{c}(i) = c^{L}

(c) (s^{L}, s ⊢ c^{L} ≃ d)

       • (a) o^{L} = ⟨global-variable i⟩

(b) r^{L} = η_{c}^{L}(η_{g}^{L}(i))

(c) l^{L} = i

(d) d = ⟨ptr l⟩

(e) S(d, s) = ⟨location #t ⟨v_{1} v_{2}⟩⟩

(f) (s^{L}, s ⊢ l^{L} ≃_{0} l)

(g) (s^{L}, s ⊢ r^{L} ≃ v_{2})

• (a) o^{L} = ⟨template i⟩ (b) η_{t}(i) = t^{L}

(c) (s^{L}, s ⊢ t^{L} ≃ d)

4. (s^{L}, s ⊢ r^{L} ≃ d) if

(a) S(d, s) = ⟨symbol #f ⟨d′⟩⟩

(b) S(d′, s) = ⟨string #f b^{∗}⟩

(c) char→int^{∗}(symbol→string(r^{L})) = b^{∗}

5. (s^{L}, s ⊢ v^{L} ≃ v) if

• (a) v^{L} = ⟨immutable-pair m_{1}^{L} m_{2}^{L}⟩ (b) S(v, s) = ⟨pair #f ⟨v_{1} v_{2}⟩⟩

(c) (s^{L}, s ⊢ η_{c}^{L}(m_{1}^{L}) ≃ v_{1})

(d) (s^{L}, s ⊢ η_{c}^{L}(m_{2}^{L}) ≃ v_{2})

• (a) v^{L} = ch^{L∗} (b) S(v, s) = ⟨string #f b^{∗}⟩

(c) char→int^{∗}(ch^{L∗}) = b^{∗}

• (a) v^{L} = immutable-vector::m^{L∗}

(b) S(v, s) = ⟨vector #f v^{′∗}⟩

(c) #m^{L∗} = #v^{′∗}

(d) (∀0 ≤ i < #m^{L∗}) (s^{L}, s ⊢ η_{c}^{L}(m^{L∗}(i)) ≃ v^{′∗}(i))

• (a) v^{L} = m (a number)

(b) v = ⟨fixnum m⟩

• (a) v^{L} = #f (b) v = ⟨imm false⟩

• (a) v^{L} = #t (b) v = ⟨imm true⟩

• (a) v^{L} = ch (a character)

(b) v = ⟨imm ⟨char char→int(ch)⟩⟩

• (a) v^{L} = nil (b) v = ⟨imm null⟩

• (a) v^{L} = ⟨closure t^{L} u^{L} l^{L}⟩ (b) v = ⟨ptr l⟩

(c) S(v, s) = ⟨closure #f ⟨t u ⟨imm unspecified⟩⟩⟩

(d) (s^{L}, s ⊢ t^{L} ≃ t)

(e) (s^{L}, s ⊢ u^{L} ≃ u)

(f) (s^{L}, s ⊢ l^{L} ≃_{0} l + 2)

• (a) v^{L} = ⟨mutable-pair l_{1}^{L} l_{2}^{L}⟩ (b) v = ⟨ptr l⟩

(c) S(v, s) = ⟨pair #t ⟨v_{1} v_{2}⟩⟩

(d) (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l)

(e) (s^{L}, s ⊢ l_{2}^{L} ≃_{0} l + 1)

• (a) v^{L} = ⟨mutable-string l^{L∗}⟩ (b) v = ⟨ptr l⟩

(c) S(v, s) = ⟨string #t b^{∗}⟩

(d) #l^{L∗} = #b^{∗}

(e) (∀0 ≤ i < #l^{L∗}) char→int(s^{L}(l^{L∗}(i))) = b^{∗}(i)

(f) (s^{L}, s ⊢ l^{L∗}(0) ≃_{0} l)

(g) for all 1 ≤ i < #l^{L∗}, the location l^{L∗}(i) is not related to any

location l′ by ≃_{0}.

• (a) v^{L} = ⟨mutable-vector l^{L∗}⟩ (b) v = ⟨ptr l⟩

(c) S(v, s) = ⟨vector #t v^{′∗}⟩

(d) #l^{L∗} = #v^{′∗}

(e) (∀0 ≤ i < #l^{L∗}) (s^{L}, s ⊢ l^{L∗}(i) ≃_{0} l + i)

• (a) v^{L} = unspecified (b) v = ⟨imm unspecified⟩

• (a) v^{L} = undefined (b) v = ⟨imm undefined⟩

• (a) v^{L} = eof (b) v = ⟨imm eof⟩ 6. (u^{L}, s^{L}) ≃ (u, s) if

• (a) u^{L} = empty-env (b) u = ⟨imm empty-env⟩

• (a) u^{L} = ⟨env u^{′L} l^{L∗}⟩ (b) u = ⟨ptr l⟩

(c) S(u, s) = ⟨environment #t u′::v^{∗}⟩

(d) (s^{L}, s ⊢ u^{′L} ≃ u′)

(e) #l^{L∗} = #v^{∗}

(f) (∀0 ≤ i < #l^{L∗}) (s^{L}, s ⊢ l^{L∗}(i) ≃_{0} l + i + 1)

7. (s^{L}, s ⊢ k^{L} ≃ k) if

• (a) k^{L} = halt (b) k = ⟨imm halt⟩

• (a) k^{L} = ⟨cont t^{L} n^{L} a^{L} u^{L} k^{L}⟩ (b) S(k, s) = ⟨continuation #f ⟨t n u k⟩^{⌢} a⟩

(c) (s^{L}, s ⊢ t^{L} ≃ t)

(d) (s^{L}, s ⊢ n^{L} ≃ n)

(e) (s^{L}, s ⊢ a^{L} ≃ a)

(f) (s^{L}, s ⊢ u^{L} ≃ u)

(g) (s^{L}, s ⊢ k^{L} ≃ k)

Definition 11 The state correspondence relation ≅ ⊂ state^{L} × state is defined as follows:

⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{L}⟩ ≅ ⟨t, n, c, v, a, u, k, s⟩ if there exists an augmented location correspondence ≃_{0}, and an augmented term correspondence ≃ induced by ≃_{0}, such that

• for all l^{L} ∈ dom(s^{L}) and l ∈ dom(s),

((s^{L}, s ⊢ l^{L} ≃_{0} l) and s(l) ∉ bhtag) ⇒ (s^{L}, s ⊢ s^{L}(l^{L}) ≃ s(l))

• (s^{L}, s ⊢ t^{L} ≃ t)

• n^{L} = n

• (s^{L}, s ⊢ v^{L} ≃ v)

• #a^{L} = #a and (∀0 ≤ i < #a)(s^{L}, s ⊢ a^{L}(i) ≃ a(i))

• (s^{L}, s ⊢ u^{L} ≃ u)

• (s^{L}, s ⊢ k^{L} ≃ k)

3.2.2 Establishing State Correspondence

The linked byte code machine loader L_{lbcm} is a partial function defined as follows:

L_{lbcm}(⟨m^{L} η_{c}^{L} η_{g}^{L} η_{t}^{L}⟩)
= ⟨η_{t}^{L}(m^{L}), 0, unspecified, ⟨⟩, empty-env, halt, s^{L}⟩
where s^{L} = undefined^{∗} and #s^{L} = #η_{g}^{L}.

The stored byte code machine loader L_{sbcm} is a partial function defined as follows:

L_{sbcm}(⟨s vd⟩) = ⟨vd, 0, c, ⟨imm unspecified⟩, ⟨⟩,

⟨imm empty-env⟩, ⟨imm halt⟩, s⟩ if S(vd, s) = ⟨template #f c::o^{∗}⟩.

Lemma 12 The lbcm and sbcm Loaders map related programs to related states. That is,

p^{L} ≃^{p} p ⇒ L_{lbcm}(p^{L}) ≅ L_{sbcm}(p)

Proof: Let p^{L} ≃^{p} p. From the definition of a program correspondence, there exists a location correspondence ≃_{0}, and a term correspondence ≃ induced by ≃_{0}, such that (s^{L}, s ⊢ η_{t}^{L}(m^{L}) ≃ vd) where s^{L} = undefined^{∗} and #s^{L} = #η_{g}^{L}. We show that ≃_{0} and ≃ are witness to the state correspondence L_{lbcm}(p^{L}) ≅ L_{sbcm}(p).

All conditions in the definition of a state correspondence hold trivially, except for the condition that related locations of the stores s^{L} and s should contain related values. Now, by definition of a location correspondence, an sbcm location is related to an lbcm location only if the former indexes the first data cell of a location object. But, by definition of an sbc program, such a data cell is always the value ⟨imm undefined⟩. This is related to the value of the lbcm location, since s^{L} = undefined^{∗}.

□

3.2.3 Preserving State Correspondence

We prove that each action rule preserves state correspondence. That is, if Σ^{L} and Σ are related lbcm and sbcm states respectively, then an lbcm action rule maps Σ^{L} to a state Σ^{′L} if and only if an sbcm action rule maps Σ to a state Σ′; furthermore, the states Σ^{′L} and Σ′ are related.

The following two lemmas will be used extensively in the proof. The first lemma states that if related values are stored in related locations of stores in related states, then the resulting states are also related.

Lemma 13 Let ≃_{0} be an augmented location correspondence and ≃ be the augmented term correspondence induced by ≃_{0}. Let

\begin{matrix}Σ^{L} = ⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{L}⟩ and \\ Σ = ⟨t, n, c, v, a, u, k, s⟩ \end{matrix}

be related states of the lbcm and sbcm respectively; that is, let Σ^{L} ≅ Σ with witnesses ≃_{0} and ≃.

Let l^{L}, l be related locations (s^{L}, s ⊢ l^{L} ≃_{0} l) such that s(l) ∈ dhtag. Let e^{L}, e be related terms (s^{L}, s ⊢ e^{L} ≃ e). Let s^{′L} = s^{L}[l^{L} ↦ e^{L}] and s′ = s[l ↦ e]. Let ≃′_{0} be an augmented location correspondence defined such that (s^{′L}, s′ ⊢ l^{L} ≃′_{0} l) if and only if (s^{L}, s ⊢ l^{L} ≃_{0} l). Let ≃′ be the augmented term correspondence induced by ≃′_{0}. Then,

1. terms related by ≃ relative to s^{L}, s are also related by ≃′ relative to s^{′L}, s′. That is,

for all x^{L}, x, (s^{L}, s ⊢ x^{L} ≃ x) ⇒ (s^{′L}, s′ ⊢ x^{L} ≃′ x)

2. If two locations are related by ≃′_{0}, then their contents are related by ≃′. That is,

for all l^{L} ∈ dom(s^{′L}) and l ∈ dom(s′) ((s^{′L}, s′ ⊢ l^{L} ≃′_{0} l) and s(l) ∉ bhtag) ⇒ (s^{′L}, s′ ⊢ s^{′L}(l^{L}) ≃′ s′(l))

3. ⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{′L}⟩ ≅ ⟨t, n, c, v, a, u, k, s′⟩ is a state correspondence with witnesses ≃′_{0} and ≃′.

Proof:

1. Since (s^{L}, s ⊢ l^{L} ≃_{0} l), we have from definition 9 that l is an address that lies within a stored object which represents a location, pair, string, vector, closure, or environment. Since s(l) ∈ dhtag by assumption, l does not lie within a string object. By inspection, we see that the definition of an augmented term correspondence relation does not depend on the content of such a location.

Now, l^{L} is a location related to l by ≃_{0}, and l does not lie within a string object. By inspection, we see that the definition of an augmented term correspondence relation does not depend on the content of such a location. Thus, modifying the contents of l^{L} and l does not affect the augmented term correspondence relation ≃, hence the result.

2. Let l_{1}^{L} ∈ dom(s^{′L}), l_{1} ∈ dom(s′), and (s^{′L}, s′ ⊢ l_{1}^{L} ≃_{0} l_{1}). The proof is by cases:

Case (l_{1}^{L} ≠ l^{L}) and (l_{1} ≠ l):

(s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1})
⇒ (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1})  by definition of ≃_{0}
⇒ (s^{L}, s ⊢ s^{L}(l_{1}^{L}) ≃ s(l_{1}))  since Σ^{L} ≅ Σ with witnesses

≃_{0} and ≃

⇒ (s^{′L}, s′ ⊢ s^{L}(l_{1}^{L}) ≃′ s(l_{1})) by part 1 of this lemma
⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) by case condition and

definitions of s^{′L} and s′

Case (l_{1}^{L} = l^{L}) and (l_{1} = l):

(s^{L}, s ⊢ e^{L} ≃ e)  by assumption
⇒ (s^{′L}, s′ ⊢ e^{L} ≃′ e)  by part 1 of this lemma
⇒ (s^{′L}, s′ ⊢ s^{′L}(l^{L}) ≃′ s′(l)) by definition of s^{′L} and s′
⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) by case condition

There are no other cases by definition of ≃_{0} (since ≃_{0} is 1-to-1 on locations).

3. Follows trivially from Definition 11 and parts (1) and (2) of this lemma.

□

The following lemma states that if related values are stored in unused locations of stores in related states, then the resulting states are also related.

Lemma 14 Let ≃_{0} be an augmented location correspondence and ≃ be the augmented term correspondence induced by ≃_{0}. Let

\begin{matrix}Σ^{L} = ⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{L}⟩ and \\ Σ = ⟨t, n, c, v, a, u, k, s⟩ \end{matrix}

be related states of the lbcm and sbcm respectively; that is, let Σ^{L} ≅ Σ with witnesses ≃_{0} and ≃.

Let l^{L}, l be locations such that l^{L} ∉ dom(s^{L}) and l ∉ dom(s). Let e^{L}, e be related terms, i.e., let (s^{L}, s ⊢ e^{L} ≃ e). Let s^{′L} = s^{L}[l^{L} ↦ e^{L}] and s′ = s[l ↦ e][l_{1} ↦ e_{1}] … [l_{k} ↦ e_{k}] where l_{i} ∉ dom(s[l ↦ e]) and e_{i} are terms for 1 ≤ i ≤ k. Let ≃′_{0} be a new augmented location correspondence such that for all locations l_{1}^{L}, l_{1}, (s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1}) holds if either (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1}) holds or if l_{1}^{L} = l^{L} and l_{1} = l. That is, the relation {(l_{1}^{L}, l_{1}) | (s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1})} extends the relation {(l_{1}^{L}, l_{1}) | (s^{L}, s ⊢ l_{1}^{L} ≃ l_{1})} with the tuple (l^{L}, l). Let ≃′ be the augmented term correspondence induced by ≃′_{0} (by Definition 10).

Then,

1. for all x^{L} ∈ D^{L}, x ∈ D, (s^{L}, s ⊢ x^{L} ≃ x) ⇒ (s^{′L}, s′ ⊢ x^{L} ≃′ x).

2. for all l^{L} ∈ dom(s^{′L}) and l ∈ dom(s′)

(s^{′L}, s′ ⊢ l^{L} ≃′_{0} l) ⇒ (s^{′L}, s′ ⊢ s^{′L}(l^{L}) ≃′ s′(l))

3. ⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{′L}⟩ ≅ ⟨t, n, c, v, a, u, k, s′⟩ with witnesses ≃_{0} and ≃.

Proof:

1. ≃ and ≃′ are obtained as the transitive closures of the relations ≃_{0} and ≃′_{0} respectively, under the same set of closure rules. But, by definition of ≃′_{0}, (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1}) implies (s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1}). Further, if (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1}) then s^{L}(l_{1}^{L}) = s^{′L}(l_{1}^{L}) and s(l_{1}) = s′(l_{1}). The result thus follows (by induction over the set of closure rules).

2. Let l_{1}^{L} ∈ dom(s^{′L}), l_{1} ∈ dom(s′), and (s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1}). The proof is by cases.

Case (l_{1}^{L} ≠ l^{L}) and (l_{1} ≠ l): Since s^{′L} = s^{L}[l^{L} ↦ e^{L}], we have that l_{1}^{L} ∈ dom(s^{L}) and s^{′L}(l_{1}^{L}) = s^{L}(l_{1}^{L}). Now, ≃_{0} relates all locations in dom(s^{L}) to locations in dom(s). Since ≃′_{0} extends ≃_{0} and is 1-to-1 on locations, l_{1} ∈ dom(s) and hence s′(l_{1}) = s(l_{1}). Now,

(s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1})
⇒ (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1})  by definition of ≃′_{0}
⇒ (s^{L}, s ⊢ s^{L}(l_{1}^{L}) ≃ s(l_{1}))  since Σ^{L} ≅ Σ
⇒ (s^{L}, s ⊢ s^{′L}(l_{1}^{L}) ≃ s′(l_{1})) since s^{′L}(l_{1}^{L}) = s^{L}(l_{1}^{L})
and s′(l_{1}) = s(l_{1})
⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) by part 1 of this lemma

Case (l_{1}^{L} = l^{L}) and (l_{1} = l):

(s^{L}, s ⊢ e^{L} ≃ e)
⇒ (s^{′L}, s′ ⊢ e^{L} ≃′ e)  by part 1 of this lemma
⇒ (s^{′L}, s′ ⊢ s^{′L}(l^{L}) ≃′ s′(l)) by definition of s^{′L} and s′
⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) by case condition

There are no other cases by definition of ≃′_{0}.

3. Follows trivially from Definition 11 and parts (1) and (2) of this lemma.

□

Lemma 15 Let ≃_{0} be an augmented location correspondence and ≃ be the augmented term correspondence induced by ≃_{0}. Let

\begin{matrix}Σ^{L} = ⟨t^{L}, n^{L}, v^{L}, a^{L}, u^{L}, k^{L}, s^{L}⟩ and \\ Σ = ⟨t, n, c, v, a, u, k, s⟩ \end{matrix}

be related states of the lbcm and sbcm respectively; that is, let Σ^{L} ≅ Σ with witnesses ≃_{0} and ≃. Then,

R^{L}(Σ^{L}) ≅ R(Σ)

Proof: We prove this in the following subsections by considering each action rule in turn. We classify the action rules into three categories: rules that do not mutate the store, rules that mutate the store by altering its values at already defined locations, and rules that mutate the store by augmenting the defined domain of the store. In this report, we only present proofs for representative rules in each category. Proofs of all action rules are detailed in a separate manuscript, and closely follow the representative proofs presented here.

□

Correspondence of Auxiliary Functions

Lemma 16 Let (s^{L}, s ⊢ u^{L} ≃ u). Then,

(s^{L}, s ⊢ env-reference(u^{L}, m_{1}, m_{2}) ≃_{0} env-lookup(env-frame(u, m_{1}, s), m_{2}, s))

Proof: The proof is by induction on m_{1}. Case m_{1} = 0: By definition,

env-reference(u^{L}, 0, m_{2})

= l^{∗}(m_{2} − 1)
if u^{L} = ⟨env u^{′L} l^{∗}⟩ and 0 ≤ (m_{2} − 1) < #l^{∗}.
env-lookup(env-frame(u, 0, s), m_{2}, s)
= env-lookup(u, m_{2}, s) = l + m_{2}
if u = ⟨ptr l⟩, S(u, s) = ⟨environment #t u′::vd^{∗}⟩,
and 1 ≤ m_{2} < #(u′::vd^{∗})

Since (s^{L}, s ⊢ u^{L} ≃ u), we have by definition of ≃ (Definition 10) that (s^{L}, s ⊢ l^{∗}(m_{2} − 1) ≃_{0} l + (m_{2} − 1) + 1) as desired.

Case m_{1} > 0: By definition,

env-reference(u^{L}, m_{1}, m_{2})

= env-reference(u^{′L}, m_{1} − 1, m_{2})
if u^{L} = ⟨env u^{′L} l^{∗}⟩
env-lookup(env-frame(u, m_{1}, s), m_{2}, s)
= env-lookup(env-frame(u′, m_{1} − 1, s), m_{2}, s)
if S(u, s) = ⟨environment #t u′::vd^{∗}⟩

Since (s^{L}, s ⊢ u^{L} ≃ u), we have by definition that (s^{L}, s ⊢ u^{′L} ≃ u′). The result then follows by inductive hypothesis since m_{1} − 1 < m_{1}.

□

Correspondence of Actions Rule 1: call m

Changes:

Σ^{′L} = Σ^{L}[t^{′L} = t_{1}^{L}][n^{′L} = 0][u^{′L} = u_{1}^{L}]
where v^{L} = ⟨closure #f ⟨t_{1}^{L} u_{1}^{L} l_{1}^{L}⟩⟩
Σ′ = Σ[t′ = t_{1}][u′ = u_{1}][c′ = c_{1}][n′ = 0]
where S(v, s) = ⟨closure #f ⟨t_{1} u_{1} d_{1}⟩⟩
and S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩

Proof Obligations:

1. (s^{L}, s ⊢ t_{1}^{L} ≃ t_{1}) which follows by definition since (s^{L}, s ⊢ v^{L} ≃ v)

2. (s^{L}, s ⊢ u_{1}^{L} ≃ u_{1}) which follows by definition since (s^{L}, s ⊢ v^{L} ≃ v)

3. 0 = 0

Rule 2: set-local! m_{1} m_{2}

Changes:

Σ^{′L} = Σ^{L}[n^{′L} = n^{L} + 3][s^{′L} = s^{L}[l^{L} ↦ v^{L}]][v^{′L} = unspecified]
where l^{L} = env-reference(u^{L}, m_{1}, m_{2})
Σ′ = Σ[n′ = n + 3][s′ = s[l ↦ v]][v′ = ⟨imm unspecified⟩]
where l = env-lookup(env-frame(u, m_{1}, s), m_{2}, s)

Proof Obligations: By assumption, Σ^{L} ≅ Σ. Let ≃_{0} and ≃ be the location and term correspondences that are witness to the state correspondence Σ^{L} ≅ Σ.

Let s^{′L} = s^{L}[l^{L} ↦ v^{L}] and s′ = s[l ↦ v]. Now, (s^{L}, s ⊢ v^{L} ≃ v) holds since Σ^{L} ≅ Σ. (s^{L}, s ⊢ l^{L} ≃_{0} l) follows from Lemma 16. We can thus use Lemma 13 to prove the proof obligations. By Lemma 13(3),

Σ^{L}[s^{′L} = s^{L}[l^{L} ↦ v^{L}]] ≅ Σ[s′ = s[l ↦ v]]

with location correspondence ≃′_{0} and term correspondence ≃′ as witnesses. Then, Σ^{′L} ≅ Σ′ holds with witnesses ≃′_{0} and ≃′ since:

1. for all l_{1}^{L} ∈ dom(s^{′L}) and l_{1} ∈ dom(s′),

(s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1}) ⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) This follows from Lemma 13.

2. (s^{′L}, s′ ⊢ t^{L} ≃′ t) which follows from Lemma 13.

3. n^{′L} = n′ where n^{′L} = n^{L} + 3 and n′ = n + 3; this holds since n^{L} = n by the assumption that Σ^{L} ≅ Σ.

4. (s^{′L}, s′ ⊢ v^{′L} ≃′ v′) where we have that v^{′L} = unspecified and v′ = ⟨imm unspecified⟩; this holds by definition of a term correspondence.

5. #a^{L} = #a and (∀0 ≤ i < #a)(s^{′L}, s′ ⊢ a^{L}(i) ≃′ a(i)) which follows from Lemma 13.

6. (s^{′L}, s′ ⊢ u^{L} ≃′ u) which follows from Lemma 13.

7. (s^{′L}, s′ ⊢ k^{L} ≃′ k) which follows from Lemma 13.

Rule 3: closure m

Changes:

Σ^{′L} = Σ^{L}[n^{′L} = n^{L} + 2] [v^{′L} = ⟨closure η_{t}(i) u^{L} #s^{L}⟩] [s^{′L} = s^{L} ^{⌢} ⟨unspecified⟩]

where t^{L} = ⟨template b^{L} e^{L}⟩ and e^{L}(m) = ⟨template i⟩

Σ′ = Σ[s′ = s > ⟨closure #f ⟨o_{m} u d^{u}⟩⟩] [v′ = ⟨ptr #s + 1⟩] [n′ = n + 2]

where S(t, s) = ⟨template #f c::o^{∗}⟩ and 1 ≤ m ≤ #o^{∗} and o_{m} = (c::o^{∗})(m) and S(o_{m}, s) = ⟨template #f c_{1}::o^{′∗}⟩ and d^{u} = ⟨imm unspecified⟩

Proof Obligations: Let ≃_{0} and ≃ be the location and augmented term correspondences that are witnesses to the state correspondence Σ^{L} ≅ Σ. Let ≃′_{0} be a new location correspondence such that for all locations l_{1}^{L}, l_{1}, (s^{′L}, s′ ⊢ l_{1}^{L} ≃′_{0} l_{1}) holds if either (s^{L}, s ⊢ l_{1}^{L} ≃_{0} l_{1}) holds, or if l_{1}^{L} = #s^{L} and l_{1} = #s + 3. Let ≃′ be the augmented term correspondence induced by ≃_{0} (by Definition 10).

Let e^{L} = unspecified and e = ⟨imm unspecified⟩. Then, by definition, (s^{L}, s ⊢ e^{L} ≃ e). Let

s^{′L} = s^{L}[l_{1}^{L} ↦ e^{L}]
s′ = s[#s ↦ ⟨header closure #f 3⟩] [#s + 1 ↦ o_{m}] [#s + 2 ↦ u] [l_{1} ↦ e]

That is, let s^{′L} = s^{L} ^{⌢} ⟨e^{L}⟩ and s′ = s > ⟨closure #f ⟨o_{m} u e⟩⟩.

We show that ≃′ is witness to the state correspondence Σ^{′L} ≅ Σ′. The above conditions permit us to use Lemma 14 in proving the obligations.

1. for all l_{1}^{L} ∈ dom(s^{′L}) and l_{1} ∈ dom(s′),

(s^{′L}, s′ ⊢ l_{1}^{L} ≃′ l_{1}) ⇒ (s^{′L}, s′ ⊢ s^{′L}(l_{1}^{L}) ≃′ s′(l_{1})) This follows from Lemma 14.

2. (s^{′L}, s′ ⊢ t^{L} ≃′ t) which follows from Lemma 14.

3. n^{′L} = n′ where n^{′L} = n^{L} + 2 and n′ = n + 2; this holds since n^{L} = n by the assumption that Σ^{L} ≅ Σ.

4. (s^{′L}, s′ ⊢ v^{′L} ≃′ v′) where v^{′L} = ⟨closure η_{t}(i) u^{L} #s^{L}⟩ and v′ = ⟨ptr #s + 1⟩.

S(v′, s′) = ⟨closure #f ⟨o_{m} u ⟨imm unspecified⟩⟩⟩ by Lemma 4. Since (s^{L}, s ⊢ t^{L} ≃ t) by assumption, we have by definition of ≃ that (s^{L}, s ⊢ η_{t}(i) ≃ o_{m}); hence, by Lemma 14, (s^{′L}, s′ ⊢ η_{t}(i) ≃′ o_{m}). Since (s^{L}, s ⊢ u^{L} ≃ u) by assumption, we have by Lemma 14 that (s^{′L}, s′ ⊢ u^{L} ≃′ u). By definition of ≃′_{0} we have that (s^{′L}, s′ ⊢ #s^{L} ≃′_{0} #s + 3). The result then holds by definition of ≃.

5. #a^{L} = #a and (∀0 ≤ i < #a)(s^{′L}, s′ ⊢ a^{L}(i) ≃′ a(i)) which follows from Lemma 14.

6. (s^{′L}, s′ ⊢ u^{L} ≃′ u) which follows from Lemma 14.

7. (s^{′L}, s′ ⊢ k^{L} ≃′ k) which follows from Lemma 14.

Lemma 17 Let Σ^{L} and Σ be lbcm and sbcm states respectively. If Σ^{L} ≅ Σ, then Σ^{L} is a halt state of the lbcm if and only if Σ is a halt state of the sbcm.

Proof: Since Σ^{L} ≅ Σ, we have that (s^{L}, s ⊢ t^{L} ≃ t), (s^{L}, s ⊢ k^{L} ≃ k), and n^{L} = n. The result then follows immediately by definition of term correspondence and halt states.

□

Lemma 18 Let Σ^{L} and Σ be lbcm and sbcm initial states respectively. If Σ^{L} ≅ Σ, then

R^{∗L}(Σ^{L}) ≅ R^{∗}(Σ)

Proof: This follows immediately from Lemmas 15 and 17.

□

3.2.4 Correspondence of Final Answers

The following lemma asserts that the lbcm and sbcm answer functions map related states to equal natural numbers.

Lemma 19 Let Σ_{f}^{L} and Σ_{f} be lbcm and sbcm halt states respectively. If Σ_{f}^{L} ≅ Σ_{f}, then A_{lbcm}(Σ_{f}^{L}) = A_{sbcm}(Σ_{f}).

Proof: Let v^{L} and v be the value registers of Σ_{f}^{L} and Σ_{f} respectively. By definition of state correspondence, v^{L} and v are related (i.e. (s^{L}, s ⊢ v^{L} ≃ v)). By definition of augmented term correspondence, if v^{L} is a number m, then v = ⟨fixnum m⟩ and so A_{lbcm}(Σ_{f}^{L}) = A_{sbcm}(Σ_{f}) = m. If v^{L} is not a number, then v is not of the form ⟨fixnum m⟩ and so A_{lbcm}(Σ_{f}^{L}) and A_{sbcm}(Σ_{f}) are both undefined.

□

3.2.5 Correspondence of Semantics

We can now prove the main theorem of this chapter.

Theorem 20 If an lbc program p^{L} corresponds to an sbc program p, then their respective operational semantics yield equal answers. That is,

p^{L} ≃^{p} p ⇒ O^{lbc}[[p^{L}]] = O^{sbc}[[p]]

Proof: Follows immediately from Lemmas 12, 18, and 19. □

4 The Image Builder Algorithm

In this chapter, we present the Scheme code that implements the image builder. The image builder translates lbc programs into sbc programs such that their respective operational semantics yield equal answers. The input of the image builder is an lbc program in the following format.

(m^{L}

      (constants c^{L∗})
      (globals m^{L∗})
      {(template (w^{L∗}) ({(constant m^{L}) | (global m^{L}) | (template m^{L})}^{∗}) )}^{+}

)

where m^{L} ranges over numbers, c^{L} ranges over lbc constants, and w^{L} ranges over lbc byte codes (either numbers, byte code operations, or identifiers). The notation {…}^{∗} denotes a sequence of zero or more terms drawn from within the braces, {…}^{+} denotes a sequence of one or more terms drawn from within the braces, and … | … denotes a choice of terms.

The output of the image-builder is an sbc program in the format

⟨m_{1} m_{2} m_{3}⟩^{⌢} s^{⌢} ⟨m_{4} vd_{1} vd_{2}⟩

where m_{1}, m_{2}, m_{3} = 0 (these may eventually be used to convey information), s is an sbc store, m_{4} is the length of s, vd_{1} is a pointer to a template object in the store s, and vd_{2} is a pointer to a vector object in the store s. vd_{1} represents the root template of the program and vd_{2} represents the symbol table of the program. The symbol table is a table of all symbol constants in the program. We do not discuss the symbol table any further in this report; it is only used by certain Scheme standard functions which have not been given a formal semantics and hence whose behavior is not being verified.

Primitive functions

The image builder algorithm is presented in terms of a collection of primitive functions. These functions have sbc syntactic classes as their ranges. The image builder constructs sbc terms by applying these functions to values in the appropriate domains; thus the image builder algorithm does not use the actual representation of sbc terms but manipulates them only through these primitive functions. The primitive functions are specified in Figure 3.

bins-per-cell  = bpw
integer->addr m  = m
addr->pointer m  = ⟨ptr m⟩
int->fixnum m  = ⟨fixnum m⟩

false  = ⟨imm false⟩
true  = ⟨imm true⟩

char->immediate ch  = ⟨imm ⟨char m⟩⟩

                                     where m = char->integer ch

null  = ⟨imm null⟩

unassigned-marker  = ⟨imm undefined⟩
hdr/pair  = pair
hdr/symbol  = symbol
hdr/string  = string
hdr/vector  = vector
hdr/location  = location
hdr/template  = template
hdr/codevector  = codevector

make-header h p m  = ⟨header h p m⟩

header-size-in-bins ⟨header h p m⟩ = m
header-size-in-cells ⟨header h p m⟩ = ℧m
integer->binval m  = m
opname->binval r  = r

Figure 3: Primitive functions.

The implementation of the image builder does not have sbc programs as its range; rather, it produces a binary image, i.e., a sequence of bits. This aspect of the algorithm is verified in the vlisp report on the virtual machine [4]. We define a function from sbc descriptors and cells to the natural numbers. The primitive functions are implemented as the composition of this function with the specifications of Figure 3.

Miscellaneous functions

(define (allign bins-lst)
(let* ((bins-in-last-cell
 (remainder (length bins-lst) bins-per-cell))
(extra-bins-needed
 (remainder (- bins-per-cell bins-in-last-cell)
            bins-per-cell))
)
(do ((i 0 (+ i 1))
(extra-bins-lst '() (cons 0 extra-bins-lst))
)
((= i extra-bins-needed) (append bins-lst extra-bins-lst))
)))
(define (threaded-foreach f lst acc)
(if (null? lst) acc
(threaded-foreach f (cdr lst) (f (car lst) acc))))

Translating Constants

(define (translate-constants const-list image)
(threaded-foreach translate-constant const-list image))
(define (translate-constant c image)
(image-constant-add!
(cond ((number? c) (PAIR (int->fixnum c) image))
((boolean? c) (PAIR (if c true false) image))
((char? c) (PAIR (char->immediate c) image))
((null? c) (PAIR null image))
((symbol? c) (build-symbol c image))
((string? c) (build-immutable-string c image))
((and (pair? c) (eq? (car c) 'pair))
 (build-immutable-pair c image))
((and (pair? c) (eq? (car c) 'vector))
 (build-immutable-vector c image))
(#t (compiler-error 'image-builder 'translate-constant

                    "Invalid constant" c))
)))
(define (build-symbol sym image)
(let* ((symstr (symbol->string sym))
(p1 (build-immutable-string symstr image))
(str-ptr (PAIR-fst p1))
(image1 (PAIR-snd p1))
(p2 (image-store-add-stob image1
     (list (make-header hdr/symbol #f 1) str-ptr)))
(symbol-ptr (PAIR-fst p2))
(image2 (PAIR-snd p2))
)
(PAIR symbol-ptr
 (image-symbol-table-add image2 symstr symbol-ptr))
))
(define (build-immutable-string str image)
(let ((charint-lst
(append (map (lambda (x)
               (integer->binval (char->integer x)))
             (string->list str))
        (list 0)))
)
(image-store-add-stob image
(cons (make-header hdr/string #f (length charint-lst))
  (allign charint-lst))
)))
(define (build-immutable-pair c image)
(image-store-add-stob image
(list (make-header hdr/pair #f 2)
(image-constant-lookup image (cadr c))
(image-constant-lookup image (caddr c))
)
))
(define (build-immutable-vector c image)
(let ((vlist (map (lambda (e)
             (image-constant-lookup image e))
           (cdr c))))
(image-store-add-stob image
(cons (make-header hdr/vector #f (length vlist)) vlist)
)))

Translating Globals

(define (translate-globals globals-list image)
  (threaded-foreach translate-global globals-list image))
(define (translate-global lbc-global-name-index image)
  (let ((sbc-global-name
         (image-constant-lookup image lbc-global-name-index)))
    (image-global-add!
     (image-store-add-stob image
      (list (make-header hdr/location #t 2)
            unassigned-marker
            sbc-global-name)
      ))))

Translating Templates

(define (translate-templates template-lst image)
  (threaded-foreach translate-template template-lst image))
(define (translate-template lbc-templ image)
  (let ((lbc-code-list (cadr lbc-templ))
        (lbc-templ-contents (cdr (caddr lbc-templ)))

;Drop dummy first element

        )
    (image-template-add!
     (build-template lbc-code-list lbc-templ-contents image)

;codevector will be added as real first element of template

     )))
(define (translate-template-contents lbc-templ-contents image)
  (map (lambda (x)
         (cond ((eq? (car x) 'constant)
                (image-constant-lookup image (cadr x)))
               ((eq? (car x) 'global-variable)
                (image-global-lookup image (cadr x)))
               ((eq? (car x) 'template)
                (image-template-lookup image (cadr x)))
               ))
       lbc-templ-contents))
(define (build-template lbc-code-list lbc-templ-contents image)
  (let ((sbc-templ-contents
         (translate-template-contents lbc-templ-contents image))
        (cv-pair (build-codevector lbc-code-list image))

   )
(image-store-add-stob
(PAIR-snd cv-pair)
(cons (make-header hdr/template #f
                   (+ 1 (length sbc-templ-contents)))
      (cons (PAIR-fst cv-pair) sbc-templ-contents))
)))
(define (translate-codelist lbc-code-list)
(map (lambda (x)
    (integer->binval (if (symbol? x) (opname->opcode x) x)))
  lbc-code-list))
(define (build-codevector lbc-code-list image)
(let ((sbc-code-list (translate-codelist lbc-code-list)))
(image-store-add-stob image
(cons (make-header hdr/codevector #f (length sbc-code-list))
      (allign sbc-code-list))
)))

Translating the symbol table

(define (build-symbol-table image)
(do ((i 0 (+ i 1))
  (image image
         (let ((p (build-mutable-list
                   (image-symbol-table-list image i) image)))
           (image-symbol-table-set! (PAIR-snd p) i
                                    (PAIR-fst p))
           ))
  )
 ((= i 256) (build-mutable-vector
             (vector->list (image-symbol-table image))
             image))
))
(define (build-mutable-list lst-of-sbc-values image)
(let loop ((lst-of-sbc-values lst-of-sbc-values)
        (sbc-list null)
        (image image))
(if (null? lst-of-sbc-values) (cons sbc-list image)
   (let ((p (build-immutable-pair-for-st
             (car lst-of-sbc-values) sbc-list image)))
     (loop (cdr lst-of-sbc-values) (PAIR-fst p) (PAIR-snd p))
     ))))

(define (build-immutable-pair-for-st sbc-v1 sbc-v2 image)
(image-store-add-stob image
(list (make-header hdr/pair #f 2) sbc-v1 sbc-v2)
))
(define (build-mutable-vector sbc-lst image)
(image-store-add-stob image
(cons (make-header hdr/vector #t (length sbc-lst)) sbc-lst)
))

Translating lbc programs to sbc programs

(define (build-image lc output-port)
(let* ((lbc-root-template (car lc))
(lbc-constants-list (cdr (cadr lc)))
(lbc-globals-list (cdr (caddr lc)))
(lbc-templates-list (cdddr lc))
(image (null-image (length lbc-constants-list)
                   (length lbc-globals-list)
                   (length lbc-templates-list)
                   output-port))
(image-with-consts
 (translate-constants lbc-constants-list image))
(image-with-globals
 (translate-globals lbc-globals-list image-with-consts))
(image-with-templates
 (translate-templates lbc-templates-list
                      image-with-globals))
(pair-with-symbol-table
 (build-symbol-table image-with-templates))
(symbol-table-ptr (PAIR-fst pair-with-symbol-table))
(final-image (PAIR-snd pair-with-symbol-table))
)
(write-cell (image-store-size final-image) output-port)
(write-cell
(image-template-lookup final-image lbc-root-template)
output-port)
(write-cell symbol-table-ptr output-port)
))
(define (write-cell cell out-port)
(write-bin-lst (cell->bin-list cell) out-port))
(define (cell->bin-list cell)
(let ((pos (>= cell 0)))

(do ((w cell (quotient w MAXBINVAL))
(i 0 (+ i 1))
(lst '()
     (let ((v (remainder w MAXBINVAL)))
       (cons (if pos v (if (= i 0)
                           (+ v MAXBINVAL)
                           (+ v MAXBINVAL -1)))
             lst)))
)
((= i bins-per-cell)
(if (> w 0)
    (compiler-error
     "number is larger than machine word" w)
    lst))
)))
(define (write-bin-lst lst out-port)
(for-each (lambda (bin)
     (write-char (integer->char bin) out-port))
   lst))
(define (write-stob-list lst out-port)
(for-each (lambda (stob) (write-stob stob out-port)) lst))
(define (write-stob stob out-port)
(if (desc-header-tag? (header-tag (car stob)))
(for-each (lambda (cell) (write-cell cell out-port)) stob)
(begin
(write-cell (car stob) out-port)
(write-bin-lst (cdr stob) out-port))
))

Image data type

An image is a tuple with four components:

Constant table: a list of constants, with each constant represented as a descriptor which may be a pointer into the store (see below);

Global table: a list of globals, with each global represented as a pointer into the store;

Template table: a list of templates, with each template represented as a pointer into the store;

Store: a list of bytes that comprise the actual code image.

In addition, the implementation builds a symbol table, i.e., a table of all symbols represented in the constant table.

Each component is represented as a vector together with a counter that contains the length of the list being represented. Thus, an image is represented as a vector with nine components:

1. constant-table: a vector of constants, with each constant represented as a descriptor which may be a pointer into the store (see below);

2. constant-table-index: number of constants in constant table;

3. global-table: a vector of globals, with each global represented as a pointer into the store;

4. global-table-index: number of globals in global table;

5. template-table: a vector of templates, with each template represented as a pointer into the store;

6. template-table-index: number of templates in template table;

7. store: a list of bytes (integers), that comprise the actual code image;

8. store-index: length of store;

9. symbol-table: the symbol table represented as a hash table.

(define (PAIR a b)                (cons a b))
(define (PAIR-fst m)              (car m))
(define (PAIR-snd m)              (cdr m))
(define (null-image cn gn tn output-port)
(write-cell 0 output-port)
(write-cell 0 output-port)
(write-cell 0 output-port)
(list->vector
(list (make-vector cn 0) 0 (make-vector gn 0) 0
      (make-vector tn 0) 0 output-port 0 (make-vector 256 '())
      )))
(define image/constant-table 0)
(define image/constant-table-index 1)
(define image/global-table 2)
(define image/global-table-index 3)
(define image/template-table 4)

(define image/template-table-index 5)
(define image/store 6)
(define image/store-index 7)
(define image/symbol-table 8)
(define (image-lookup image vector-kind n)
    (vector-ref (vector-ref image vector-kind) (- n 1)))
(define (image-add! m vector-kind index-kind)
  (let ((v (PAIR-fst m))
        (image (PAIR-snd m)))
    (vector-set! (vector-ref image vector-kind)
                 (vector-ref image index-kind)
                 v)
    (vector-set! image index-kind
                (+ 1 (vector-ref image index-kind)))
    image
    ))
(define (image-constant-lookup image n)
  (image-lookup image image/constant-table n))
(define (image-constant-add! p)
  (image-add! p image/constant-table image/constant-table-index))
(define (image-global-lookup image n)
  (image-lookup image image/global-table n))
(define (image-global-add! p)
  (image-add! p image/global-table image/global-table-index))
(define (image-template-lookup image n)
  (image-lookup image image/template-table n))
(define (image-template-add! p)
  (image-add! p image/template-table image/template-table-index))

The store is represented by an output port; stobs are added to the store by writing them out.

(define (image-store-size image)
  (vector-ref image image/store-index))
(define (image-store-append-stob! image stob)
  (write-stob stob (vector-ref image image/store))
  )
(define (image-store-add-stob image stob)
  (let* ((out-port (vector-ref image image/store))
         (old-hp (vector-ref image image/store-index))

     (len (+ 1 (header-size-in-cells (car stob))))
     )
(image-store-append-stob! image stob)
(vector-set! image image/store-index (+ old-hp len))
(PAIR (addr->pointer (integer->addr (+ old-hp 1))) image)
))
(define (hash s)
(let ((len (string-length s))
    (hash-prime 251))
(let loop ((i 0)
           (acc 0))
  (if (= i len) acc
      (loop (+ i 1) (remainder
                     (+ (* acc 256)
                        (char->integer (string-ref s i)))
                     hash-prime))
      ))))
(define (image-symbol-table image)
(vector-ref image image/symbol-table))
(define (image-symbol-table-list image n)
(vector-ref (image-symbol-table image) n))
(define (image-symbol-table-set! image index val)
(vector-set! (image-symbol-table image) index val)
image)
(define (image-symbol-table-add image symstr symbol-ptr)
(let ((index (hash symstr)))
(image-symbol-table-set! image index
 (cons symbol-ptr (image-symbol-table-list image index)) )
))

5 Correctness of the Image Builder

We prove that the image builder translates lbc programs to related sbc programs. That is, if p^{L} is an lbc program then p = image-builder(p^{L}) is an sbc program and p^{L} ≃^{p} p. Theorem 20 permits us to conclude that the image builder preserves the operational semantics of programs, as desired.

Let ⟨m^{L} η_{c}^{L} η_{g}^{L} η_{t}^{L}⟩ be an lbc program where η_{c}^{L}, η_{g}^{L}, and η_{t}^{L} are lbc constant, global, and template tables respectively, and m^{L} is an index into η_{t}^{L} (m^{L} represents the “root” template).

The image builder proceeds by translating the lbc constant, global, and template tables. It maintains an intermediate data structure (called an image) of the form ⟨η_{c} η_{g} η_{t} s⟩. η_{c}, η_{g}, and η_{t} are sbc constant, global, and template tables respectively and represent the translations of the respective lbc tables. s is an sbc store and contains the sbc representations of the translated constant, global, and template terms.

5.1 Translating Constants

The function translate-constants translates lbc constants into sbc constants. After translation, entries in the lbc and sbc constant tables are related via a term correspondence relation. translate-constants is expressed in terms of an auxiliary function that translates a single lbc constant to an sbc constant.

Lemma 21 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let η_{c}^{L} be an lbc constant table. Let ⟨s η_{c}⟩ be an sbc constant table such that #η_{c} < #η_{c}^{L} and (⟨⟩, s ⊢ η_{c}^{L}(i) ≃ η_{c}(i)) for all 0 ≤ i < #η_{c}. Then, if

translate-constant(η_{c}^{L}, ⟨η_{c} η_{g} η_{t} s⟩) = ⟨η′_{c} η_{g} η_{t} s′⟩

then η′_{c} = η_{c} ^{⌢} ⟨vd⟩ for some vd, and (⟨⟩, s′ ⊢ η_{c}^{L}(i) ≃ η′_{c}(i)) for all 0 ≤ i < #η′_{c}.

Proof: Let j = #η_{c}.

Case η_{c}^{L}(j) = m Then, η′_{c}(j) = ⟨fixnum m⟩ and s′ = s. By definition of a term correspondence, (⟨⟩, s ⊢ m ≃ ⟨fixnum m⟩).

Case η_{c}^{L}(j) = #f Then, η′_{c}(j) = ⟨imm false⟩ and s′ = s. By definition of a term correspondence, (⟨⟩, s ⊢ #f ≃ ⟨imm false⟩).

Case η_{c}^{L}(j) = #t Then, η′_{c}(j) = ⟨imm true⟩ and s′ = s. By definition of a term correspondence, (⟨⟩, s ⊢ #t ≃ ⟨imm true⟩).

Case η_{c}^{L}(j) = ch Then, η′_{c}(j) = ⟨imm ⟨char char→int(ch)⟩⟩ and s′ = s. By definition of a term correspondence, (⟨⟩, s ⊢ ch ≃ (⟨imm ⟨char char→int(ch)⟩⟩)).

Case η_{c}^{L}(j) = nil Then, η′_{c}(j) = ⟨imm null⟩ and s′ = s. By definition of a term correspondence, (⟨⟩, s ⊢ nil ≃ ⟨imm null⟩).

Case η_{c}^{L}(j) = ch^{L∗} Then, η′_{c}(j) = ⟨ptr #s+1⟩ and s′ = s >⟨string #f char→int^{∗}(ch^{L∗})⟩. By definition of a term correspondence,

(⟨⟩, s′ ⊢ ch^{L∗} ≃ ⟨ptr #s + 1⟩)

Case η_{c}^{L}(j) = ⟨immutable-pair m_{1}^{L} m_{2}^{L}⟩ Then, η′_{c}(j) = ⟨ptr #s + 1⟩ and s′ = s > ⟨pair #f ⟨η_{c}(m_{1}^{L}) η_{c}(m_{2}^{L})⟩⟩. Now, by definition of lbc, m_{1}^{L} < j and m_{2}^{L} < j . Thus, by assumption, (⟨⟩, s ⊢ η_{c}^{L}(m_{i}^{L}) ≃ η_{c}(m_{i}^{L})). Then, by definition of a term correspondence,

(⟨⟩, s′ ⊢ ⟨immutable-pair m_{1}^{L} m_{2}^{L}⟩ ≃ ⟨ptr #s + 1⟩)

Case η_{c}^{L}(j) = immutable-vector::m^{L∗}

Then, η′_{c}(j) = ⟨ptr #s + 1⟩ and s′ = s > ⟨vector #f η_{c}^{∗}(m^{L∗})⟩. Now, by definition of lbc, m^{L∗}(i) < j for 0 ≤ i < #m^{L∗}. Thus, by assumption, for 0 ≤ i < #m^{L∗}, (⟨⟩, s′ ⊢ η_{c}^{L}(m^{L∗}(i)) ≃ η_{c}^{∗}(m^{L∗})(i)). Then, by definition of a term correspondence,

(⟨⟩, s′ ⊢ (immutable-vector::m^{L∗}) ≃ ⟨ptr #s + 1⟩)

Case η_{c}^{L}(j) = r^{L} Let b^{∗} = char→int^{∗}(symbol→string(r^{L})). Let s_{a} = s >⟨string #f b^{∗}⟩ and s′ = s_{a} >⟨symbol #f ⟨⟨ptr #s+1⟩⟩⟩. Then, η′_{c}(j) = ⟨ptr #s_{a}+ 1⟩. Now, S(⟨ptr #s_{a} + 1⟩, s′) = ⟨symbol #f ⟨⟨ptr #s + 1⟩⟩⟩ and S(⟨ptr #s + 1⟩, s′) = ⟨string #f b^{∗}⟩. Then, by definition of a term correspondence, (⟨⟩, s′ ⊢ r^{L} ≃ ⟨ptr #s_{a} + 1⟩).

□

5.2 Translating Globals

The function translate-globals translates lbc globals into sbc globals. After translation, entries in the lbc and sbc global tables are related via a term correspondence relation. translate-globals is expressed in terms of an auxiliary function that translates a single lbc global to an sbc global.

Lemma 22 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let s^{L} be an lbc store, and η_{c}^{L} and η_{g}^{L} be lbc constant and global tables respectively. Let s be an sbc store, and ⟨s η_{c}⟩ and ⟨s η_{g}⟩ be sbc constant and global tables respectively. Let

#s^{L} = #η_{g}s^{L} = unspecified^{∗}
#η_{c} = #η_{c}^{L}
(s^{L}, s ⊢ η_{c}^{L}(i) ≃ η_{c}(i)) for all 0 ≤ i < #η_{c}
#η_{g} < #η_{g}^{L}
(s^{L}, s ⊢ ⟨global-variable i⟩ ≃ η_{g}(i)) for all 0 ≤ i < #η_{g}

Then, if

translate-global(η_{c}^{L}, η_{g}^{L}, ⟨η_{c} η_{g} η_{t} s⟩) = ⟨η_{c} η′_{g} η_{t} s′⟩

then there exists a location correspondence ≃′_{0} such that, if ≃′ is the term correspondence induced by ≃′_{0} and s^{′L} = s^{L} ^{⌢} ⟨unspecified⟩, then

η′_{g} = η_{g} ^{⌢} ⟨vd⟩ for some vd, and
(s^{′L}, s′ ⊢ ⟨global-variable i⟩ ≃′ η′_{g}(i)) for all 0 ≤ i < #η′_{g}

Proof: By definition,

η′_{g} = η_{g} ^{⌢} ⟨ptr #s + 1⟩
s′ = s > ⟨location #t ⟨⟨undefined η_{c}(η_{g}^{L}(#η_{g}))⟩⟩⟩

Let ≃′_{0} be a new location correspondence such that for all locations l^{L}, l, (s^{′L}, s′ ⊢ l^{L} ≃′_{0} l) holds if either (s^{L}, s ⊢ l^{L} ≃_{0} l) holds or if l^{L} = #s^{L} and l = (#s + 1). That is, the relation {(l^{L}, l) | (s^{′L}, s′ ⊢ l^{L} ≃′_{0} l)} extends the relation {(l^{L}, l) | (s^{L}, s ⊢ l^{L} ≃ l)} with the tuple (#s^{L}, (#s + 1)). Let ≃′ be the term correspondence induced by ≃′_{0}.

We now show that

(s^{′L}, s′ ⊢ ⟨global-variable i⟩ ≃′ η′_{g}(i)) for all 0 ≤ i < #η′_{g}

Since ≃′_{0} strictly extends ≃_{0}, it follows that ≃′ strictly extends ≃. The result then follows by assumption for 0 ≤ i < #η_{g}. Now let i = #η_{g} = (#η′_{g} − 1). Then,

(s^{′L}, s′ ⊢ ⟨global-variable i⟩ ≃′ η′_{g}(i))
= (s^{′L}, s′ ⊢ ⟨global-variable #η_{g}⟩ ≃′ ⟨ptr #s + 1⟩)

The proof obligations then are:

• S(⟨ptr #s + 1⟩, s′) = ⟨location #t ⟨v_{1} v_{2}⟩⟩ This holds by Lemma 4, with v_{1} = undefined and v_{2} = η_{c}(η_{g}^{L}(#η_{g})).

• (s^{′L}, s′ ⊢ #η_{g} ≃′_{0} #s + 1)

This holds by definition of ≃′_{0}, since #s^{L} = #η_{g} by assumption.

• (s^{′L}, s′ ⊢ η_{c}^{L}(η_{g}^{L}(#η_{g})) ≃′ η_{c}(η_{g}^{L}(#η_{g}))) Now, since #η_{g} < #η_{g}^{L} by assumption, we have by definition of an lbc program that η_{g}^{L}(#η_{g}) < #η_{c}^{L}. Since #η_{c}^{L} = #η_{c}, we also have that η_{g}^{L}(#η_{g}) < #η_{c}. The result then holds by the assumption that

(s^{L}, s ⊢ η_{c}^{L}(i) ≃ η_{c}(i)) for all 0 ≤ i < #η_{c}

□

5.3 Translating Templates

The function translate-templates translates lbc templates into sbc templates. After translation, entries in the lbc and sbc template tables are related via a term correspondence relation. translate-templates is expressed in terms of an auxiliary function translate-template that translates a single lbc template to an sbc template.

Lemma 23 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let s^{L} be an lbc store, and η_{c}^{L}, η_{g}^{L}, and η_{t}^{L} be lbc constant, global, and template tables respectively. Let s be an sbc store, and ⟨s η_{c}⟩, ⟨s η_{g}⟩, and ⟨s η_{t}⟩ be sbc constant, global, and template tables respectively. Let

#s^{L} = #η_{g}^{L}s^{L} = unspecified^{∗}
#η_{c} = #η_{c}^{L}
(s^{L}, s ⊢ η_{c}^{L}(i) ≃ η_{c}(i)) for all 0 ≤ i < #η_{c}
#η_{g} = #η_{g}^{L}
(s^{L}, s ⊢ ⟨global-variable i⟩ ≃ η_{g}(i)) for all 0 ≤ i < #η_{g}
#η_{t} < #η_{t}^{L}
(s^{L}, s ⊢ η_{t}^{L}(i) ≃ η_{t}(i)) for all 0 ≤ i < #η_{t}

Then, if

translate-template(η_{c}^{L}, η_{g}^{L}, η_{t}^{L}, ⟨η_{c} η_{g} η_{t} s⟩) = ⟨η_{c} η_{g} η′_{t} s′⟩

then

η′_{t} = η_{t} ^{⌢} ⟨vd⟩ for some vd, and
(s^{L}, s′ ⊢ η_{t}^{L}(i) ≃ η′_{t}(i)) for all 0 ≤ i < #η′_{t}

Proof: Let η_{t}^{L}(#η_{t}) = ⟨template w^{L} e^{L}⟩. Then, by definition,

s′′ = s > ⟨codevector #f w^{L}⟩
c = ⟨ptr #s + 1⟩
e^{′L} = e^{L} † 1
o^{∗}(i) = translate-template-content(e^{′L}(i)) for all 0 ≤ i < #e^{′L}
#o^{∗} = #e^{′L}
s′ = s′′ > ⟨template #f c::o^{∗}⟩
η′_{t} = η_{t} ^{⌢} ⟨⟨ptr #s′′ + 1⟩⟩

Now, for 0 ≤ i < #η_{t}, the result follows immediately by assumption. Let i = #η_{t} = (#η′_{t} − 1). Then,

(s^{L}, s′ ⊢ η_{t}^{L}(i) ≃′ η′_{t}(i))
= (s^{L}, s′ ⊢ η_{t}^{L}(#η_{t}) ≃′ η′_{t}(#η′_{t} − 1))
= (s^{L}, s′ ⊢ ⟨template w^{L} e^{L}⟩ ≃′ ⟨ptr #s′′ + 1⟩)

The proof obligations then are:

1. S(⟨ptr #s′′ + 1⟩, s′) = ⟨template #f c::o^{∗}⟩ This holds by Lemma 4, with c and o^{∗} given as above.

2. (s^{L}, s ⊢ w^{L} ≃ c)

This holds by definition since S(c, s) = ⟨codevector #f w^{L}⟩ by Lemma 4.

3. #e^{L} = #(c::o^{∗})

This holds since #o^{∗} = #e^{′L} and e^{′L} = e^{L} † 1.

4. (∀0 ≤ i < #o^{∗}) (s^{L}, s ⊢ e^{′L}(i) ≃ o^{∗}(i)) o^{∗} is defined in terms of the function translate-template-content. We proceed by cases:

Case e^{′L}(i) = ⟨constant j⟩:

By definition of an lbc program, j < #eta_{c}^{L} = #eta_{c}. Then, o^{∗}(i) = translate-template-content(⟨constant j⟩) = η_{c}(j). Now (s^{L}, s ⊢ ⟨constant j⟩ ≃ η_{c}(j)) holds since (s^{L}, s ⊢ η_{c}^{L}(j) ≃ η_{c}(j)) holds by assumption.

Case e^{′L}(i) = ⟨global-variable j⟩:

By definition of an lbc program, j < #eta_{g}^{L} = #eta_{g}. Then, o^{∗}(i) = translate-template-content(⟨global-variable j⟩) = η_{g}(j). But (s^{L}, s ⊢ ⟨global-variable j⟩ ≃ η_{g}(j)) holds by assumption.

Case e^{′L}(i) = ⟨template j⟩:

By definition of an lbc program, j < #eta_{t} < #eta_{t}^{L}. Then, o^{∗}(i) = translate-template-content(⟨template j⟩) = η_{t}(j). Now (s^{L}, s ⊢ ⟨template j⟩ ≃ η_{t}(j)) holds since (s^{L}, s ⊢ η_{t}^{L}(j) ≃ η_{t}(j)) holds by assumption.

□

5.4 Translating Programs

The image builder is defined to be the composition of the above functions.

Definition 24 Let P^{L} = ⟨m^{L} η_{c}^{L} η_{g}^{L} η_{t}^{L}⟩ be an lbc program. Let

a_{0} = ⟨⟨⟩ ⟨⟩ ⟨⟩ ⟨⟩⟩
a_{1} = translate-constants(η_{c}^{L}, a_{0})
a_{2} = translate-globals(η_{c}^{L}, η_{g}^{L}, a_{1})
a_{3} = translate-templates(η_{c}^{L}, η_{g}^{L}, η_{t}^{L}, a_{2})

Then, if a_{3} = ⟨η_{c} η_{g} η_{t} s⟩, then

build-image(P^{L}) = ⟨s η_{t}(m^{L})⟩

Theorem 25 Let P^{L} be an lbc program. Then P = build-image(P^{L}) is an sbc program and P^{L} ≃^{p} P holds.

Proof: Let a_{3} = ⟨η_{c} η_{g} η_{t} s⟩ be defined as in Definition 24 above. Then, by Lemmas 21, 22, and 23, there exists a location correspondence ≃_{0} and a term correspondence ≃ induced by ≃_{0} such that

#η_{c} = #η_{c}^{L}, #η_{g} = #η_{g}^{L}, and #η_{t} = #η_{t}^{L},
(s^{L}, s ⊢ η_{c}^{L}(i) ≃ η_{c}(i)) for all 0 ≤ i < #η_{c},
(s^{L}, s ⊢ η_{g}^{L}(i) ≃ η_{g}(i)) for all 0 ≤ i < #η_{g}, and
(s^{L}, s ⊢ η_{t}^{L}(i) ≃ η_{t}(i)) for all 0 ≤ i < #η_{t}

In particular,

(s^{L}, s ⊢ η_{t}^{L}(m^{L}) ≃ η_{t}(m^{L}))

and so P^{L} ≃^{p} P by definition.

□

References

[1] W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell, and V. Swarup. The vlisp linker. M 92B095, The MITRE Corporation, 1992.

[2] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp byte-code compiler. M 92B092, The MITRE Corporation, 1992.

[3] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp flattener. M 92B094, The MITRE Corporation, 1992.

[4] V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk, and J. D. Ramsdell. The vlisp byte-code interpreter. M 92B097, The MITRE Corporation, 1992.

[5] M. Wand and D. P. Oliva. Proving the correctness of storage representations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 151–160, New York, 1992. ACM Press.