The VLISP Linker

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

The MITRE Corporation^{1} M92B095 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 linker, which lays out a single data structure for a program consisting of constants, variables, and procedures. It contains detailed proofs that the operational semantics of the linked output matches the operational semantics of the input. iv

Contents

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

2 Linked Byte Code State Machines 1 2.1 Syntax of the Linked Byte Code Language . . . . . . . . . . . 1 2.2 States and Actions . . . . . . . . . . . . . . . . . . . . . . . . 2

3 The Linker Algorithm 5

4 Correctness of the Linker Algorithm 12 4.1 Preliminary Definitions . . . . . . . . . . . . . . . . . . . . . 12 4.2 Literal Stores and Tables . . . . . . . . . . . . . . . . . . . . 14 4.3 Syntactic Correctness of the Linker . . . . . . . . . . . . . . . 16 4.4 Semantic Correctness of the Linker . . . . . . . . . . . . . . . 19

References 21

1 Introduction

This paper discusses the vlisp linker, an algorithm which lays out a single data structure for a program consisting of constants, variables, and procedures. The main procedure of the linker, link-template, produces a program of Linked Byte Code (lbc) from a template of Flattened Byte Code (fbc). lbc and its semantics are given in section 2. The linker algorithm is presented in section 3, and its syntactic and semantic correctness are proved in section 4.

1.1 Notation

Finite sequences will be formed using ⟨…⟩ notation. Commas are optional between sequence members; we will usually not use commas in expressions of fbc and lbc. f(a)↓ means the function f is defined at a. Similarly, f(a)↑ means the function f is undefined at a.

2 Linked Byte Code State Machines

This section presents the lbc and gives it an (operational) semantics. Both the syntax and semantics of lbc are very similar to the syntax and semantics of fbc presented in [1]. This paper assumes familiarity with the [1], particularly the sections on state machines in general and fbc state machines.

2.1 Syntax of the Linked Byte Code Language

In the higher-level vlisp languages, the only notion of program that was relevant was a template, including whatever other templates it referenced (possibly through intermediate templates). lbc, by contrast, has a particular syntax for a program, in which all the templates are gathered together in a single linear sequence. In addition, lbc has two other sequences, gathering (respectively) all constants and all global variables referenced throughout the whole program. These sequences are arranged so that if one template refers to another, or if one constant has another as a component, then the template or constant referred to occurs earlier in its sequence than the one referring to it. This property makes it easy for the loader to lay the objects out sequentially in a binary format, and to find an address for an object whenever a later object refers to it.

The bnf grammar for lbc (given in Table 1) is very similar to the grammar for fbc. In fact, the productions for t, e, w, and m are exactly the same. There are two new syntactic classes: p is for programs and õ is for pseudoliterals. An lbc program

         p = ⟨n constants :: c^{∗} global-variables :: n^{∗}⟩^{⌢}t^{+}

is proper if:

(1) For all k < #c^{∗}, if c^{∗}(k) = ⟨immutable-pair n_{1} n_{2}⟩, then 1 ≤ n_{1}, n_{2} ≤ k, and if c^{∗}(k) = ⟨immutable-vector n_{1} ⋯ n_{j}⟩, then 1 ≤ n_{1}, …, n_{j} ≤ k.

(2) For all k < #n^{∗}, 1 ≤ n^{∗}(k) ≤ #c^{∗} and c^{∗}(n^{∗}(k) − 1) is a symbol.

(3) For all k < #t^{+}, if t^{+}(k) = ⟨template w ⟨o_{1} ⋯ o_{j}⟩⟩, then for all o_{i} with 1 ≤ i ≤ j:

(a) if o_{i} = ⟨constant n′⟩, then 1 ≤ n′ ≤ #c^{∗};

(b) if o_{i} = ⟨global-variable n′⟩, then 1 ≤ n′ ≤ #n^{∗};

(c) if o_{i} = ⟨template n′⟩, then 1 ≤ n′ ≤ k.

(4) n = #t^{+}.^{1}

Hence, a proper program satisfies the reference conditions mentioned above.

The Augmented Linked Byte Code (albc) is an expansion of lbc in exactly the same way afbc is an expansion of fbc [1].

2.2 States and Actions

lbc states are defined in just the same way as fbc states; the only difference is that variables over syntactic classes of code are interpreted as ranging over lbc expressions rather than fbc expressions.

Although lbc states are sequences of the form

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

like fbc states, the behavior of an lbc machine depends on two parameters, instead of just one (i.e., globals), which do not change during the execution of the state machine. The first parameter, called globals′, is a function from

1This n clearly adds no new information to p since n = #p − 3, provided p is proper.

 p ::= ⟨n constants :: c^{∗} global-variables :: n^{∗}⟩^{⌢}t^{+}

õ ::= o | t | ⟨constant c⟩

 t ::= ⟨template w e⟩

e ::= o*

 c ::= c_{pr} | strings | ⟨immutable-pair n_{1} n_{2}⟩ | immutable-vector :: n^{∗}
 o ::= ⟨constant n⟩ | ⟨global-variable n⟩ | ⟨template n⟩

w ::= ⟨⟩ | m^{⌢}w

m ::= ⟨call n⟩ | ⟨return⟩ | ⟨make-cont n_{0} n_{1} n_{2}⟩ | ⟨literal n⟩
    | ⟨closure n⟩ | ⟨global n⟩ | ⟨local n_{0} n_{1}⟩ | ⟨set-global! n⟩
    | ⟨set-local! n_{0} n_{1}⟩ | ⟨push⟩ | ⟨make-env n⟩ | ⟨make-rest-list n⟩
    | ⟨unspecified⟩ | ⟨jump n_{0} n_{1}⟩ | ⟨jump-if-false n_{0} n_{1}⟩
    | ⟨checkargs= n⟩ | ⟨checkargs>= n⟩ | ⟨i⟩

Table 1: Grammar for Linked Byte Code

some finite set of natural numbers to locations. The second parameter is the program that the machine is executing, a value in the lbc syntactic class p given in Table 1. However, the parameter p plays a role only in determining two auxiliary functions: u_{c} and u_{t}. For

         p = ⟨n constants :: c^{∗} global-variables :: n^{∗}⟩^{⌢}t^{+},

if 1 ≤ k ≤ #c^{∗}, then u_{c}(k) = c^{∗}(k−1), and if 1 ≤ k ≤ #t^{+}, u_{t}(k) = t^{+}(k−1). Hence, p will not appear below; only these auxiliary functions will appear.

All but four of the pure rules of lbc are syntactically identical to the corresponding rules for fbc. The four rules that differ are those that use the literals. We will not repeat the other rules here.

Rule: Literal Domain conditions:

w†n = ⟨literal n_{1}⟩^{⌢}w_{1} e(n_{1}) = ⟨constant n_{2}⟩ u_{c}(n_{2}) = c

Changes:

n′ = n + 2 v′ = c

Rule: Closure Domain conditions:

w†n = ⟨closure n_{1}⟩^{⌢}w_{1} e(n_{1}) = ⟨template n_{2}⟩ u_{t}(n_{2}) = t_{1}

Changes:

n′ = n + 2 v′ = ⟨closure t_{1} u #s⟩ s′ = s^{⌢}⟨not-specified⟩

Rule: Global Domain conditions:

w†n = ⟨global n_{1}⟩^{⌢}w_{1}

e(n_{1}) = ⟨global-variable n_{2}⟩

l = globals′(n_{2}) v_{1} = s(l) v_{1} ≠ undefined

Changes:

n′ = n + 2 v′ = v_{1}

Rule: Set Global Domain conditions:

w†n = ⟨set-global! n_{1}⟩^{⌢}w_{1}
e(n_{1}) = ⟨global-variable n_{2}⟩

l = globals′(n_{2}) l ≤ #s

Changes:

n′ = n + 2 v′ = not-specified s′ = s + {l ↦ v}

3 The Linker Algorithm

The procedure link-template generates a literal table from an fbc template. The literal table is then converted into an lbc program by assemblelinked-template. (The notion of a “literal table” is defined in subsection 4.2.)

(define (link-template template)
  (let ((tab-lit (link-literal empty-literal-table template)))
    (assemble-linked-template
        (tab-lit-table tab-lit)
        (tab-lit-literal tab-lit))))
(define (assemble-linked-template tab lit)
  `(,(cadr lit)
    (constants
     . ,(hash-table-data (literal-table-constants tab)))
    (global-variables
     . ,(hash-table-data (literal-table-global-variables tab)))
    . ,(template-table-data (literal-table-templates tab))))

The central procedure of the linker is link-literal. Its code is very simple since it treats literals as abstract objects. Its subprocedures—

component-literals, make-linked-literal, and

lookup-in-literal-table—dispatch on the syntax of their arguments.

(define (link-literal tab lit)
  (let* ((lits (component-literals lit))
         (tab-lits (link-literals tab lits))
         (new-lit (make-linked-literal
                   lit
                   (tab-lits-literals tab-lits))))
    (lookup-in-literal-table
     (tab-lits-table tab-lits)
     new-lit)))
(define (link-literals tab lits)
  (link-literals-aux tab lits '()))

(define (link-literals-aux tab old-lits new-lits)
(if (null? old-lits)
(cons tab (reverse new-lits))
(let ((tab-lit (link-literal tab (car old-lits))))
(link-literals-aux
(tab-lit-table tab-lit)
(cdr old-lits)
(cons (tab-lit-literal tab-lit) new-lits)))))
(define tab-lit-table car)
(define tab-lit-literal cdr)
(define tab-lits-table car)
(define tab-lits-literals cdr)

The three dispatch procedures are given below.

(define (component-literals lit)
(cond ((or (atomic-constant? lit)
    (global-variable? lit))
'())
((pair-constant? lit)
(list (list 'constant (car (cadr lit)))
      (list 'constant (cdr (cadr lit)))))
((vector-constant? lit)
(map
 (lambda (x) (list 'constant x))
 (vector->list (cadr lit))))
((template? lit)
(caddr lit))
(else (compiler-error "Bad literal." lit))))
(define (make-linked-literal lit lits)
(cond ((or (atomic-constant? lit)
    (global-variable? lit))
lit)
((pair-constant? lit)
(list 'constant (cons 'pair (map cadr lits))))
((vector-constant? lit)
(list 'constant (cons 'vector (map cadr lits))))
((template? lit)

         (list 'template (cadr lit) lits))
        (else (compiler-error "Bad literal." lit))))
(define (lookup-in-literal-table tab lit)
  (cond ((or (atomic-constant? lit)
             (pair-constant? lit)
             (vector-constant? lit))
         (lookup-constant-in-literal-table tab (cadr lit)))
        ((global-variable? lit)
         (lookup-global-variable-in-literal-table
          tab
          (cadr lit)))
        ((template? lit)
         (lookup-template-in-literal-table tab lit))
        (else (compiler-error "Bad literal." lit))))
(define (atomic-constant? lit)
  (and (eq? (car lit) 'constant)
       (not (pair? (cadr lit)))
       (not (vector? (cadr lit)))))
(define (pair-constant? lit)
  (and (eq? (car lit) 'constant)
       (pair? (cadr lit))))
(define (vector-constant? lit)
  (and (eq? (car lit) 'constant)
       (vector? (cadr lit))))
(define (global-variable? lit)
  (eq? (car lit) 'global-variable))
(define (template? lit)
  (eq? (car lit) 'template))

The following are the low-level procedures for building and manipulating literal tables. These procedures could be pared down somewhat.

(define (make-literal-table c-table gv-table t-table)
  (vector c-table gv-table t-table))

(define (literal-table-constants tab)
(vector-ref tab 0))
(define (literal-table-global-variables tab)
(vector-ref tab 1))
(define (literal-table-templates tab)
(vector-ref tab 2))
(define empty-literal-table
(make-literal-table  (list 1 (make-vector 512 '()))
            (list 1 (make-vector 512 '()))
            '(1)))
(define (literal-table->pairs tab)
(let ((c-pairs
(reverse
(map
(lambda (x)
  (cons (cons 'constant (cdr x))
        (list 'constant (car x))))
(vector->list
 (cdr (literal-table-constants tab))))))
(gv-pairs
(reverse
(map
(lambda (x)
  (cons (cons 'global-variable (cdr x))
        (list 'global-variable (car x))))
(vector->list
 (cdr (literal-table-global-variables tab))))))
(t-pairs
(reverse
(map
(lambda (x)
  (cons (cons 'template (cdr x))
        (car x)))
(cdr (literal-table-templates tab))))))
(append c-pairs gv-pairs t-pairs)))

(define (lookup-constant-in-literal-table tab constant)
(let ((probe (lookup-data-in-hash-table
          (literal-table-constants tab)
          constant)))
(cons
(make-literal-table
(probe-table probe)
(literal-table-global-variables tab)
(literal-table-templates tab))
(list 'constant (probe-value probe)))))
(define (lookup-global-variable-in-literal-table
   tab global-variable)
(let* ((tab-lit
    (lookup-constant-in-literal-table
     tab
     global-variable))
   (probe (lookup-data-in-hash-table
           (literal-table-global-variables tab)
           (cadr (tab-lit-literal tab-lit)))))
(cons
(make-literal-table
(literal-table-constants (tab-lit-table tab-lit))
(probe-table probe)
(literal-table-templates (tab-lit-table tab-lit)))
(list 'global-variable (probe-value probe)))))
(define (lookup-template-in-literal-table tab template)
(let ((probe (enter-data-in-template-table
          (literal-table-templates tab)
          template)))
(cons
(make-literal-table
(literal-table-constants tab)
(literal-table-global-variables tab)
(probe-table probe))
(list 'template (probe-value probe)))))

(define probe-table car)
(define probe-value cdr)
(define make-probe cons)
(define (template-table-data table)
  (reverse (cdr table)))
(define (hash-table-data table)
  (reverse (cddr table)))
(define (lookup-data-in-hash-table table key)
  (let* ((counter (car table))
         (hash-table (cadr table))
         (data-list (cddr table))
         (hash-index (linker-hash key))
         (indexed-list (vector-ref hash-table hash-index))
         (query (assoc key indexed-list)))
    (if query
        (make-probe table (cdr query))
        (begin
          (vector-set!
           hash-table
           hash-index
           (cons (cons key counter) indexed-list))
          (make-probe
           (cons (+ 1 counter)
                 (cons hash-table (cons key data-list)))
           counter)))))
(define (enter-data-in-template-table table key)
  (make-probe (cons (+ 1 (car table))
                    (cons key (cdr table)))
              (car table)))

(define (hash-string s hash-prime)
(let ((len (string-length s)))
(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 (hash-vector x hash-prime)
(let loop ((lst (cdr x))
   (acc 0))
(if (null? lst) acc
(loop (cdr lst)
      (remainder
       (+ (* acc 512) (car lst))
       hash-prime)))))
(define (linker-hash x)
(let ((hash-prime 509))
(cond ((number? x) (remainder (abs x) hash-prime))
((symbol? x)
 (hash-string (symbol->string x) hash-prime))
((string? x) (hash-string x hash-prime))
((and (pair? x) (eq? (car x) 'pair))
 (remainder (* (cadr x) (caddr x)) hash-prime))
((char? x) (char->integer x))
((and (pair? x) (eq? (car x) 'vector))
 (hash-vector x hash-prime))
((boolean? x) (if x 510 511))
((null? x) 511)
(#t
 (compiler-error
  'linker 'hash "Invalid constant" x)))))

4 Correctness of the Linker Algorithm

We show in this section that link-template is correct in two ways:

(1) link-template always produces a proper lbc program from an fbc template (Corollary 4.9).

(2) The execution of an lbc program p produced by link-template from an fbc template t mirrors the execution of t (see Theorem 4.10).

For the most part, the verification of the low-level procedures for building and manipulating literal tables is left to the reader. Except for the hash function routines, these procedures are unchallenging.

Throughout this section we shall refer to “template literals,” “immutable pairs,” and “immutable vectors” of both fbc and lbc as simply “literals,” “pairs,” and “vectors,” respectively. By a “pseudoliteral” we shall mean an fbc literal or an lbc pseudoliteral; both fbc and lbc pseudoliterals will be denoted by the symbol õ.

We shall assume that ζ is an arbitrary injective function from identifiers to symbols.^{2}

4.1 Preliminary Definitions

A kind is a member of the set

          kinds = {constant, global-variable, template}.

We shall sometimes use c, g, and t as shorthand for the three members of kinds. The kind of a pseudoliteral õ, written kind(õ), is the kind õ(0).

The components of a pseudoliteral õ, written comp(õ), is a list of pseudoliterals defined as follows: comp(õ) = \{ \begin{matrix}⟨⟩ & if õ is ⟨constant x⟩ and x is neither a pair nor \\ & a vector \\ ⟨x′_{1} x′_{2}⟩ & if õ is ⟨constant x⟩ and x is \\ & ⟨immutable-pair x_{1} x_{2}⟩ \\ ⟨x′_{1} ⋯ x′_{m}⟩ & if õ is ⟨constant x⟩ and x is \\ & ⟨immutable-vector x_{1} ⋯ x_{m}⟩ \\ ⟨⟩ & if õ is ⟨global-variable x⟩ \\ ⟨⟩ & if õ is ⟨template n⟩ \\ o^{∗} & if õ is ⟨template w o^{∗}⟩ \end{matrix}

2In the linker algorithm, the function corresponding to ζ maps identifiers to the symbols from which they are constructed. However, the correctness of the linker algorithm does not depend on what ζ actually is.

where x′_{i} = ⟨constant x_{i}⟩. A pseudoliteral õ is atomic if comp(õ) = ⟨⟩ and is compound otherwise. The depth of a pseudoliteral õ, written depth(õ), is defined inductively by the following:

(1) If õ is atomic, then depth(õ) = 0.

(2) If õ is compound, then depth(õ) = 1 + max{depth(õ′) : õ′ ∈ comp(õ)}.

Let L_{fbc}, A_{fbc}, and C_{fbc} denote the sets of literals, atomic literals, and compound literals, respectively, of fbc. Also, let L̃_{lbc}, Ã_{lbc}, and C̃_{lbc} denote the sets of pseudoliterals, atomic pseudoliterals, and compound pseudoliterals, respectively, of lbc. Obviously, L_{fbc} = A_{fbc} ∪ C_{fbc} and L̃_{lbc} = Ã_{lbc} ∪ C̃_{lbc}. Also, let L_{lbc} denote the set of lbc literals (which are always atomic). Notice that (Ã_{lbc} \ L_{lbc}) ⊆ A_{fbc}.

Suppose õ ∈ C̃_{lbc} and o_{1}, …, o_{m} ∈ L_{fbc} with m = #comp(õ). Then make-flat-lit(õ, ⟨o_{1} ⋯ o_{m}⟩) is:

 (1) ⟨constant ⟨immutable-pair c_{1} c_{2}⟩⟩
     if õ = ⟨constant ⟨immutable-pair n_{1} n_{2}⟩⟩

and o_{i} = ⟨constant c_{i}⟩ for i = 1, 2;

 (2) ⟨constant ⟨immutable-vector c_{1} · · · c_{m}⟩⟩
     if õ = ⟨constant ⟨immutable-vector n_{1} · · · n_{m}⟩⟩

and o_{i} = ⟨constant c_{i}⟩ for i = 1, …, m;

(3) ⟨template w ⟨o_{1} ⋯ o_{m}⟩⟩ if õ = ⟨template w o^{∗}⟩; and

(4) undefined otherwise.

It is easy to see that make-flat-lit(õ, ⟨o_{1} ⋯ o_{m}⟩) ∈ L_{fbc} provided it is defined.

4.2 Literal Stores and Tables

Let L̃′_{lbc} = L̃_{lbc} \ {⟨k n⟩ : k = c, t}. A literal store is an injective function f : kinds × N^{+} → L̃′_{lbc} with finite domain such that, whenever f(k, n)↓, the following hold:

(1) kind(f(k, n)) = k.

(2) f(k, m)↓ for all m with 1 ≤ m < n.

(3) If k = c, then, for all ⟨c m⟩ ∈ comp(f(k, n)), m < n.

(4) If k = g, then for some m ∈ N^{+} f(g, n) = ⟨g m⟩ and f(c, m) = ⟨c c⟩ where c ∈ ran(ζ).

(5) If k = t, then, for all ⟨k′m⟩ ∈ comp(f(k, n)), f(k′, m)↓ if k′ = c, g, and m < n if k′ = t.

Let stores denote the set of literal stores.

A Scheme data structure τ is a literal table if one of the following hold:

 (1) τ is produced by empty-literal-table.

(2) ⟨τ, o⟩ is produced by lookup-in-literal-table from a literal table and a member of L̃′_{lbc}.

A literal table τ represents a literal store f if literal-table->pairs produces a list ⟨⟨⟨a_{1}, b_{1}⟩, c_{1}⟩ ⋯ ⟨⟨a_{m}, b_{m}⟩, c_{m}⟩⟩ from τ such that:

(1) f(a_{i}, b_{i}) = c_{i} for each i with 1 ≤ i ≤ m; and

(2) f(k, n)↓ implies k = a_{i} and n = b_{i} for some i with 1 ≤ i ≤ m.

Lemma 4.1 The procedure empty-literal-table produces a literal table which represents the literal store with the empty domain.

Proof By inspection of the Scheme code for empty-literal-table and

literal-table->pairs. □

The function lookup : (stores × A_{fbc} ∪ C̃_{lbc}) → (stores × L_{lbc}) is defined as follows:

(1) Let ⟨f, õ⟩ ∈ (stores × A_{fbc} ∪ C̃_{lbc}) with õ in the range of f. Then lookup(f, õ) = ⟨f, ⟨k n⟩⟩, where f(k, n) = õ.

(2) Let ⟨f, õ⟩ ∈ (stores × A_{fbc} ∪ C̃_{lbc}) such that (a) k = kind(õ) ≠ g and (b) õ not is in the range of f but each o′ ∈ comp(õ) is in the range of f. Suppose n is the least positive integer such that f(k, n)↑. Then lookup(f, õ) = ⟨f′, ⟨k n⟩⟩, where f′ = f ∪ {⟨⟨k, n⟩, õ⟩}.

(3) Let ⟨f, õ⟩ ∈ (stores×A_{fbc}) such that (a) õ = ⟨g i⟩ and (b) õ not is in the range of f. Let ⟨f′, ⟨c m⟩⟩ = lookup(f, ⟨c ζ(i)⟩). Suppose n is the least positive integer such that f′(g, n)↑. Then lookup(f, õ) = ⟨f′′, ⟨g n⟩⟩, where f′′ = f′ ∪ {⟨⟨g, n⟩, ⟨g m⟩⟩}.

(4) Let ⟨f, õ⟩ ∈ (stores × A_{fbc} ∪ C̃_{lbc}) with õ and some o′ ∈ comp(õ) not in the range of f. Then lookup(f, õ)↑.

Proposition 4.2 The function lookup is well-defined, i.e., if ⟨f, õ⟩ ∈ (stores × A_{fbc} ∪ C̃_{lbc}), then lookup(f, õ) ∈ (stores × L_{lbc}) for cases (1), (2), and (3). Moreover, lookup(f, õ) = ⟨f′, o⟩ implies f′ extends f and kind(o) = kind(õ).

Proof Straightforward. □

Lemma 4.3 Let τ be a literal table representing f, õ ∈ A_{fbc} ∪ C̃_{lbc}, ⟨τ′, o⟩ be produced by lookup-in-literal-table from τ and õ, and ⟨f′, o′⟩ = lookup(f, õ). Then τ′ represents f′ and o = o′.

Proof By a comparison of the Scheme code for lookup-in-literal-table with the definition of lookup. □

Proposition 4.4 Every literal table represents a literal store.

Proof Follows from Lemma 4.1 and the previous lemma. □

The function extract : (stores × L_{lbc} ∪ C̃_{lbc}) → L_{fbc} is defined recursively by:

(1) If f ∈ stores and o = ⟨k n⟩ ∈ L_{lbc} with f(k, n) ∈ A_{fbc}, then extract(f, o) = f(k, n).

(2) If f ∈ stores and o = ⟨k n⟩ ∈ L_{lbc} with f(k, n) ∈ C̃_{lbc} and k ≠ g, then extract(f, o) = extract(f, f(k, n)).

(3) If f ∈ stores and o = ⟨g n⟩ ∈ L_{lbc}, then extract(f, o) = ⟨g i⟩, where i is the unique identifier such that, for some m ∈ N^{+}, f(g, n) = ⟨g m⟩ and f(c, m) = ⟨c ζ(i)⟩.

(4) If f ∈ stores, õ ∈ C̃_{lbc}, and comp(õ) = ⟨õ_{1} ⋯ õ_{m}⟩, then extract(f, õ) =

make-flat-lit(õ, ⟨extract(f, õ_{1}) ⋯ extract(f, õ_{m})⟩).

(5) Otherwise, extract(f, õ)↑.

4.3 Syntactic Correctness of the Linker

We show in this section that link-template always produces a proper lbc program from an fbc template. The principal result we prove is the following theorem:

Theorem 4.5 (Main Linker Correctness Theorem) Let f ∈ stores be represented by the literal table τ, and let o ∈ L_{fbc}. If link-literal produces ⟨τ′, o′⟩ from τ and o, then:

(1) τ′ is a literal table which represents a literal store f′ extending f;

(2) o′ ∈ L_{lbc} and kind(o′) = kind(o);

(3) extract(f′, o′) = o.

Before proving this theorem, we present three elementary lemmas.

Lemma 4.6 component-literals produces comp(o) from o ∈ L_{fbc}.

Proof component-literals is a direct implementation in Scheme of the definition of comp for members of L_{fbc}. □

The following lemma shows that link-literals simply iterates link-literal over a list of members of L_{fbc}.

Lemma 4.7 Let τ be a literal table and o_{1}, …, o_{m} ∈ L_{fbc}.

(1) link-literals produces ⟨τ, ⟨⟩⟩ from τ and ⟨⟩.

(2) Assume link-literal produces ⟨τ_{1}, o′_{1}⟩ from τ and o_{1}, and link-literals produces ⟨τ_{m}, ⟨o′_{2} ⋯ o′_{m}⟩⟩ from τ_{1} and ⟨o_{2} ⋯ o_{m}⟩. Then link-literals produces ⟨τ_{m}, ⟨o′_{1} ⋯ o′_{m}⟩⟩ from τ and ⟨o_{1} ⋯ o_{m}⟩.

Proof By inspection of the Scheme code for link-literals.□

Lemma 4.8 Suppose o ∈ L_{fbc} and o_{1}, …, o_{m} ∈ L_{lbc} with m = #comp(o). Then make-linked-literal produces a pseudoliteral õ ∈ A_{fbc} ∪ C̃_{lbc} from o and ⟨o_{1} ⋯ o_{m}⟩ such that:

(1) õ = o if o is atomic;

 (2) õ = ⟨constant ⟨immutable-pair n_{1} n_{2}⟩⟩ if
     o = ⟨constant ⟨immutable-pair c_{1} c_{2}⟩⟩ and

o_{i} = ⟨constant n_{i}⟩ for i = 1, 2;

 (3) õ = ⟨constant ⟨immutable-vector n_{1} · · · n_{m}⟩⟩ if
     o = ⟨constant ⟨immutable-vector c_{1} · · · c_{m}⟩⟩ and

o_{i} = ⟨constant n_{i}⟩ for i = 1, …, m; and

(4) õ = ⟨template w ⟨o_{1} ⋯ o_{m}⟩⟩ if o = ⟨template w ⟨o′_{1} ⋯ o′_{m}⟩⟩.

Proof By inspection of the Scheme code for make-linked-literal.□

Proof of Main Linker Correctness Theorem The proof is by induction on depth(o).

Basis. Assume depth(o) = 0, i.e., o ∈ A_{fbc}. Also, assume link-literal produces ⟨τ′, o′⟩ from τ and o.

By the three lemmas immediately above, lookup-in-literal-table produces ⟨τ′, o′⟩ from τ and o. By the definition of a literal table, τ′ is a literal table in virtue of τ being a literal table. Since o ∈ A_{fbc}, lookup(f, o) = ⟨f′, o′′⟩, where o′′ = ⟨k n⟩ ∈ L_{lbc}. By Proposition 4.2, f′ extends f, and kind(o′′) = kind(o), and by Lemma 4.3, τ′ represents f′ and o′ = o′′. Hence, statements (1) and (2) of the theorem hold. If k = c, then

extract(f′, o′) = extract(f′, o′′)
= f′(c, n))
= o

by definitions of extract and lookup. The argument is the same if k = t. If o = ⟨g i⟩, then for some m ∈ N^{+} f(g, n) = ⟨g m⟩ such that f(c, m) = ⟨c ζ(i)⟩, and so extract(f′, o′) = extract(f′, o′′) = o by the definition of extract. Hence, statement (3) of the theorem holds.

Induction step. Assume 0 < n and the theorem is true for all o ∈ L_{fbc} with depth(o) < n. Let o ∈ C_{fbc} with depth(o) = n. It suffices to show the theorem is true for o.

Assume (∗) link-literal produces ⟨τ′, o′⟩ from τ and o. Consider link-literal acting on τ and o. link-literal has three local variables: lits, tab-lits, and new-lit. Since depth(o) = n > 0, comp(o) = ⟨o_{1} ⋯ o_{m}⟩ where m ≠ 0 and depth(o_{i}) < n for all i with 1 ≤ i ≤ m. By Lemma 4.6, lits is bound to comp(o). Hence, by Lemma 4.7, the induction hypothesis, and the assumption (∗), it follows that there are literal stores f_{1}, …, f_{m}; literal tables τ_{1}, …, τ_{m}; and o′_{1}, …, o′_{m} ∈ L_{lbc} such that:

(a) tab-lits is bound to ⟨τ_{m}, ⟨o′_{1} ⋯ o′_{m}⟩⟩.

(b) τ_{i} represents f_{i} for all i with 1 ≤ i ≤ m.

(c) f_{1} extends f, and f_{i+1} extends f_{i} for all i with 1 ≤ i ≤ m − 1.

(d) extract(f_{i}, o′_{i}) = o_{i} for all i with 1 ≤ i ≤ m.

By Lemma 4.8, make-linked-literal produces õ ∈ C̃_{lbc} from o and ⟨o′_{1} ⋯ o′_{m}⟩, and new-lit is bound to õ. It is easy to see that kind(õ) = kind(o) and that each member of comp(õ) is in the range of f_{m}.

By assumption (∗), lookup-in-literal-table produces ⟨τ′, o′⟩ from τ_{m} and new-lit. By the definition of a literal table, τ′ is a literal table in virtue of τ_{m} being a literal table. Since each member of comp(õ) is in the range of f_{m}, lookup(f_{m}, õ) = ⟨f′, o′′⟩, where o′′ = ⟨k n⟩ ∈ L_{lbc} and f′(k, n) = õ. By Proposition 4.2, f′ extends f_{m} and kind(o′′) = kind(õ), and by Lemma 4.3, τ′ represents f′ and o′ = o′′. Hence, statements (1) and (2) of the theorem hold.

By the definition of extract,

extract(f′, o′) = extract(f′, o′′)
= extract(f′, f′(k, n))
= extract(f′, õ)

Furthermore, by the definitions of extract and make-flat-lit,

extract(f′, õ) = make-flat-lit(õ, ⟨extract(f′, o′_{1}) ⋯ extract(f′, o′_{m})⟩)
= make-flat-lit(õ, ⟨o_{1} ⋯ o_{m}⟩)
= o

Hence, statement (3) of the theorem holds.□

Corollary 4.9 link-template produces a proper lbc program from an fbc template.

Proof Let t be an fbc template. Let τ be the literal table with empty domain. Clearly, link-literal produces some ⟨τ′, o⟩ from τ and t. By Theorem 4.5,

(1) τ′ is a literal table which represents a literal store f, and

(2) o = ⟨t n⟩ for some n ∈ N^{+}.

The procedure assemble-linked-template produces, from τ′ and o, an lbc program

         p = ⟨n constants :: c^{∗} global-variables :: n^{∗}⟩^{⌢}t^{+}

such that:

(a) f(c, k) = ⟨c c^{∗}(k − 1)⟩ for all k with 1 ≤ k ≤ #c^{∗}, and f(c, #c^{∗} + 1)↑.

(b) f(g, k) = ⟨g n^{∗}(k − 1)⟩ and f(c, n^{∗}(k − 1)) is a symbol for all k with 1 ≤ k ≤ #n^{∗}, and f(g, #n^{∗} + 1)↑.

(c) f(t, k) = t^{+}(k − 1) for all k with 1 ≤ k ≤ #t^{+}, and f(t, #t^{+} + 1)↑.

(d) n = #t^{+}.

From these three statements and the fact that f is a store, it follows that p is proper. □

4.4 Semantic Correctness of the Linker

We show in this section that an lbc program p produced by link-template from an fbc template t is semantically correct in the sense that the execution of p in the lbc state machine mirrors the execution of t in fbc state machine. Theorem 4.10 is a precise formulation of this assertion.

Before we can state Theorem 4.10, we must define a function Φ_{ξ} from fbc states to lbc states, which depends on a given fbc template ξ. Φ_{ξ} will be defined using a series of functions Φ_{ξ,o}, Φ_{ξ,c}, Φ_{ξ,t}, Φ_{ξ,v}, Φ_{ξ,a}, Φ_{ξ,s}, and Φ_{ξ,k} that map fbc literals, constants, templates, values, argument stacks, stores, and continuations to lbc literals, constants, templates, values, argument stacks, stores, and continuations, respectively. We shall also define a function Ψ_{ξ} which maps a function ρ : i^{k} → L to a function ρ′ : n^{k} → L with k ≥ 0.

Let ξ be a fixed fbc template. τ_{ξ}, f_{ξ}, and p_{ξ} are defined as follows: τ_{ξ} is the literal table which is produced by link-literal from the literal table with empty domain and ξ. f_{ξ} is the literal store represented by τ_{ξ}. p_{ξ} is the program produced by link-template from ξ. Note that p_{ξ} and τ_{ξ} are just different “representations” of f_{ξ}. Let u_{ξ,c} and u_{ξ,t} be the functions u_{c} and u_{t} for p = p_{ξ}.

Φ_{ξ,o}(o) is the literal (if there is one) produced by link-literal from τ_{ξ} and o ∈ L_{fbc}; otherwise, Φ_{ξ,o}(o) is undefined.

Φ_{ξ,c} is defined by:

Φ_{ξ,c}(c) = \{ \begin{matrix}u_{c}(n) & if ⟨c n⟩ = Φ_{ξ,o}(⟨c c⟩) \\ undefined & if Φ_{ξ,o}(⟨c c⟩) is undefined \end{matrix}

Φ_{ξ,t} is defined by:

Φ_{ξ,t}(t) = \{ \begin{matrix}u_{t}(n) & if ⟨t n⟩ = Φ_{ξ,o}(t) \\ undefined & if Φ_{ξ,o}(t) is undefined \end{matrix}

Φ_{ξ,v} is defined by:

(1) If v = ⟨immutable-pair c_{1} c_{2}⟩, then

Φ_{ξ,v}(v) = ⟨immutable-pair Φ_{ξ,c}(c_{1}) Φ_{ξ,c}(c_{2})⟩,

provided Φ_{ξ,c}(c_{1})↓ and Φ_{ξ,c}(c_{2})↓; otherwise Φ_{ξ,v}(v)↑.

(2) If v = ⟨immutable-vector c_{1} ⋯ c_{m}⟩, then

Φ_{ξ,v}(v) = ⟨immutable-vector Φ_{ξ,c}(c_{1}) ⋯ Φ_{ξ,c}(c_{m})⟩,

provided Φ_{ξ,c}(c_{1})↓, …, Φ_{ξ,c}(c_{m})↓; otherwise Φ_{ξ,v}(v)↑.

(3) If v = ⟨closure t u l⟩, then

Φ_{ξ,v}(v) = ⟨closure Φ_{ξ,t}(t) u l⟩,

provided Φ_{ξ,t}(t)↓; otherwise Φ_{ξ,v}(v)↑.

(4) If v = ⟨escape k l⟩, then

Φ_{ξ,v}(v) = ⟨escape Φ_{ξ,k}(k) l⟩,

provided Φ_{ξ,k}(k)↓; otherwise Φ_{ξ,v}(v)↑.

(5) Otherwise, Φ_{ξ,v}(v) = v.

Φ_{ξ,a} is defined by: For a = ⟨v_{1} ⋯ v_{m}⟩,

Φ_{ξ,a}(a) = ⟨Φ_{ξ,v}(v_{1}) ⋯ Φ_{ξ,v}(v_{m})⟩,

provided Φ_{ξ,v}(v_{1})↓, …, Φ_{ξ,v}(v_{m})↓; otherwise Φ_{ξ,a}(a)↑.

Φ_{ξ,s} = Φ_{ξ,a}.

Φ_{ξ,k} is defined by:

(1) Φ_{ξ,k}(halt) = halt.

(2) If k = ⟨cont t n a u k′⟩, then

Φ_{ξ,k}(k) = ⟨cont Φ_{ξ,t}(t) n Φ_{ξ,a}(a) u Φ_{ξ,k}(k′)⟩,

provided Φ_{ξ,t}(t)↓, Φ_{ξ,a}(a)↓, Φ_{ξ,k}(k′)↓; otherwise Φ_{ξ,k}(k)↑.

Φ_{ξ} is then defined by: For an fbc state Σ = ⟨t, n, v, a, u, k, s⟩,

Φ_{ξ}(Σ) = ⟨Φ_{ξ,t}(t), n, Φ_{ξ,v}(v), Φ_{ξ,a}(a), u, Φ_{ξ,k}(k), Φ_{ξ,s}(s)⟩.

Finally, Ψ_{ξ} is defined by: For a function ρ : i^{∗} → L,

Ψ_{ξ}(ρ)(n) = \{ \begin{matrix}ρ(i) & if extract(f_{ξ}, ⟨g n⟩) = ⟨g i⟩, and ρ(i)↓ \\ undefined & otherwise \end{matrix}

For each (pure) fbc rule R, let R̄ be the corresponding pure lbc rule. Given an fbc state Σ, an fbc rule R, and ρ : i^{∗} → L, R(Σ, ρ) is the fbc state that results from applying R to Σ when globals = ρ. (R(Σ, ρ) = Σ when R is not applicable to Σ given globals = ρ). Similarly, given an lbc state Σ′, an lbc rule R′, ρ′ : n^{∗} → L, and an lbc program p′, R′(Σ′, ρ′, p′) is the lbc state that results from applying R′ to Σ′ when globals′ = ρ′ and p = p′.

Theorem 4.10 Let ξ be an fbc template, Σ be an fbc state, R be an fbc rule, and globals = ρ. Then

Φ_{ξ}(R(Σ, ρ)) = R̄(Φ_{ξ}(Σ), Ψ_{ξ}(ρ), p_{ξ}).

Proof The theorem clearly holds for all the fbc rules except possibly Literal, Closure, Global, and Set Global. The theorem holds for Literal since Φ_{ξ,o}(⟨c c⟩) = ⟨c n⟩ for some n ∈ N^{+} such that Φ_{ξ,c}(c) = u_{c}(n). The theorem holds for Closure since Φ_{ξ,o}(t) = ⟨t n⟩ for some n ∈ N^{+} such that Φ_{ξ,t}(t) = u_{t}(n). And, the theorem holds for Global and Set Global since Φ_{ξ,o}(⟨g i⟩) = ⟨g n⟩ for some n ∈ N^{+} such that globals(i) = globals′(n). □

References

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