A Core Calculus for Provenance
Umut A. Acar

Amal Ahmed

James Cheney

Roly Perera

January 6, 2014

arXiv:1310.6299v2 [] 3 Jan 2014

Abstract
Provenance is an increasing concern due to the ongoing revolution in sharing and processing scientific data on the
Web and in other computer systems. It is proposed that many computer systems will need to become provenanceaware in order to provide satisfactory accountability, reproducibility, and trust for scientific or other high-value data.
To date, there is not a consensus concerning appropriate formal models or security properties for provenance. In previous work, we introduced a formal framework for provenance security and proposed formal definitions of properties
called disclosure and obfuscation.
In this article, we study refined notions of positive and negative disclosure and obfuscation in a concrete setting,
that of a general-purpose programing language. Previous models of provenance have focused on special-purpose
languages such as workflows and database queries. We consider a higher-order, functional language with sums,
products, and recursive types and functions, and equip it with a tracing semantics in which traces themselves can be
replayed as computations. We present an annotation-propagation framework that supports many provenance views
over traces, including standard forms of provenance studied previously. We investigate some relationships among
provenance views and develop some partial solutions to the disclosure and obfuscation problems, including correct
algorithms for disclosure and positive obfuscation based on trace slicing.

1

Introduction

Provenance, or meta-information about the origin, history, or derivation of an object, is now recognized as a central
challenge in establishing trust and providing security in computer systems, particularly on the Web. Essentially,
provenance management involves instrumenting a system with detailed monitoring or logging of auditable records
that help explain how results depend on inputs or other (sometimes untrustworthy) sources. The security and privacy
ramifications of provenance must be understood in order to safely meet the needs of users that desire provenance
without introducing new security vulnerabilities or compromising the confidentiality of other users.
The lack of adequate provenance information can cause (and has caused) major problems, which we call provenance failures [19]. Essentially, a provenance failure can arise either from failure to disclose some key provenance
information to users, or from failure to obfuscate some sensitive provenance information. As an example of failure
to disclose provenance, in 2008 an undated, years-out-of-date story about United Airlines’ 2002 near-bankruptcy was
mistakenly put on Google News’ main page, causing investors to panic about its financial stability, which in turn led
to a significant decrease in its share price over the course of a few hours [12]. Another example is the ‘Climategate’
controversy [42], in which climate scientists were embarrassed (and widely criticized by climate change skeptics)
when private emails that suggested poor data analysis practice were leaked. . As an example of failure to obfuscate,
in 2003 a Word document about British intelligence prior to the invasion of Iraq was published with supposedly secret
contributors’ identities logged in its change history [47], revealing the influence of political advisors on the report.
Obfuscation is obviously closely related to traditional security concerns, such as confidentiality and anonymity.
Disclosure is, in our view, also a security property, linked to the traditional security concern of availability. In securing
provenance, we seek to disclose some important provenance information while keeping other aspects of provenance
confidential. If all we cared about was obfuscation, then security would be easy to achieve by simply not providing
any provenance. The tension between the two goals of disclosure and obfuscation makes the analysis of security for
provenance a more challenging problem.

1

Provenance has predominantly been studied in the context of scientific computation and databases. A number
of forms of provenance have been proposed for different computational models, including why and where provenance [11], how-provenance [28], and dependency provenance [17] in databases. In other settings, a variety of ad hoc
techniques have been proposed, largely based on instrumenting various systems to record a graph diagramming the
procedure calls or dependencies among data and processes [38, 8, 44]. However, almost all of this work assumes a
cooperative setting in which users are not intentionally trying to subvert or forge provenance information. When the
accuracy of information used by day traders, validity and public acceptance of scientific results, and independence of
intelligence reports from political influence depends on provenance, there is a great deal at stake, so it is important to
develop foundations for correctness and security of provenance in the face of attacks.
Although a wide variety of models of provenance have been studied in different settings, there has been relatively
little progress on developing a general understanding of provenance. By analogy with Abadi, Banerjee, Heintze and
Riecke’s core calculus of dependency [1], which elucidated the common ideas underlying different techniques such
as information flow security, program slicing, and binding-time analysis, this article introduces a core calculus for
provenance: that is, a calculus that illustrates and unifies the key ideas underlying a range of provenance techniques,
including tracing, annotation-propagation, and connections to program slicing. Our main application of this framework
is to explore the implications of the general definitions of disclosure and obfuscation introduced in our prior work, but
we hope that our approach will also be useful for studying other aspects of provenance.
Prior work on provenance and security. Despite its apparent importance, there has been relatively little work on
formal foundations of provenance, and work on provenance security has only begun to appear over the last five years.
Our previous work [17] appears to have been the first to explicitly relate information-flow security to a form
of provenance, called dependency provenance. Provenance has been studied in language-based security by Cirillo
et al. [21], who developed a form of authorization logic with notions of provenance for understanding information
flow among concurrently executing objects, and by Swamy et al. [46, 45], who developed mechanisms for dependencyprovenance tracking in a dependently-typed secure programming language called Fable. Both projects focus on specifying and enforcing security policies involving provenance tracking alongside many other concerns, and not on defining provenance semantics or extraction techniques. Work on secure auditing [34, 29] and expressive programming
languages for security [45] is also related, but this work focuses on explicitly manipulating proofs of authorization or
evidence about protocol or program runs rather than automatically deriving or securing provenance information in its
own right.
There is also some work directly addressing security for provenance [20, 32, 15, 23, 6, 24]. Chong [20] gave
(to our knowledge) the first candidate formal definitions of data security and provenance security using a trace semantics, based in part on earlier, unpublished work of ours on traces and provenance [16]. Hasan et al. [32] study
security techniques for ensuring the integrity of a document that changes over time along with its provenance records.
Davidson et al. [23] studied a notion of privacy for provenance in scientific workflows, focusing on complexity lower
bounds. In their approach, the definition of privacy essentially says that for unknown components in a workflow
(i.e. a simple dataflow diagram), an attacker should not be able to learn functional behavior; for example, should
not be able to narrow down the possible output values for any input to less than a parameter k. Cheney [15] gave
an abstract framework for provenance, proposed definitions of properties called obfuscation and disclosure, and discussed algorithms and complexity results for instances of this framework including finite automata, workflows, and
the semiring model of database provenance [28]. Zhang et al. [50] develop tamper-detection techniques for provenance in databases. Blaustein et al. [6] studied the problem of rewriting provenance graphs to hide information while
still satisfying some plausibility constraints. Dey et al. [24] studied provenance publishing policies, aimed at giving
users greater control over what information is shown and hidden. They developed a system called ProPub equipped
with well-defined publishing and hiding operators, along with constraints that such policies should satisfy. (In this respect, Dey et al.’s publishing operators, and work on “provenance views” [35] can be seen retroactively as addressing
disclosure requirements subject to additional conciseness constraints.)
More recently, Lyle and Martin [36] gave a detailed comparative survey of topics in provenance and in security,
pointing out many parallel developments, and Martin et al. [37] advocate study of provenance considered as a security
control. Some other topics in security, such as non-repudiation [43], plausible deniability or differential privacy [26],
also appear analogous to our disclosure and obfuscation properties, and this connection could be explored.

2

In this article, we build on prior work on provenance security by studying the disclosure and obfuscation properties
of different forms of provenance in the context of a higher-order, pure, functional language. To illustrate what we
mean by provenance, we present examples of programming with three different forms of provenance in Transparent
ML (TML), a prototype implementation of the ideas of this article.
To ease exposition, we present the examples in terms of a hypothetical ML-like toplevel loop extended with labeled
values, first-class traces, a type (Γ, τ ) trace that consists of traces returning type τ evaluated in label context Γ, and
with various functions that extract different forms of provenance from traces. The tracing and extraction features are
formalized later in the article, and our prototype supports these examples, as well as the disclosure and obfuscation
slicing algorithms presented later in the paper. The Slicer and LambdaCalc tools of Perera et al. [40, 39] employ
similar ideas, and have been run on larger examples, but focus on slicing as a debugging and program understanding
technique and does not yet support provenance extraction or disclosure and obfuscation slicing. Developing a unified
and mature implementation supporting all of these ideas is left for future work; Perera et al. [40, 39] should be
consulted for further implementation details.

1.1

Examples

Where-provenance. Where-provenance [11, 10] identifies at most one source location from which a part of the
output was copied. For example, consider the following TML session:
- f [(1,2), (4,3), (5,6)];
val it = [(5,6), (3,4), (1,2)]
Without access to the source code, one can guess that f is doing something like
reverse ◦ (map (λ(x, y).if x < y then (x, y) else (y, x)))
However, by providing where-provenance information, the system can explain whether the numbers in the result were
copied from the input or constructed in some other way:
- trace (f [(1@L1,2@L2),(4@L3,3@L4),(5@L5,6@L6)]);
it = <trace> : ({L1:int,...}, (int*int) list) trace
- where it;
val it = [(5@L5,6), (3@L4,4), (1@L1,2)]
This shows that f contrives to copy the first elements of the returned pairs but construct the second components.
Dependency provenance. Dependency provenance [17] is an approach that tracks a set of all source locations on
which a result depends. For example, if we have:
- g [(1,2,3), (4,5,6)];
val it = [6,6] : int list
we again cannot tell much about what g does. By tracing and asking for dependency provenance, we can see:
- trace (g [(1@L1,2@L2,3@L3),(4@L4,5@L5,6@L6)]);
val it = <trace> : ({L1:int,...}, int list) trace
- dependency it;
val it = [6@{L1,L2,L3}, 6@{L1,L2,L3}]
This suggests that g is computing both elements of the result from the first triple and returning the result twice, without
examining the rest of the list. We can confirm this as follows:
- trace (g ((1@L1,2@L2,3@L3)::[]@L));
val it = <trace> : ({L1:int,...}, int list) trace
- dependency it;
val it = [6@{L1,L2,L3}]
3

The fact that L does not appear in the output confirms that g does not look further into the list. While it appears that g
may be computing 6 from 1, 2, 3 by adding them together, the exact process by which g computes 6 from 1, 2, 3 is not
explicit in the dependency annotations; they are also consistent with the hypothesis that g multiplies 1, 2, 3 together to
compute 6 or even that g simply examines 1, 2, 3 and then returns the constant 6.
Expression provenance. A third common form of provenance is an expression graph or tree that shows how a value
was computed by primitive operations. For example, consider:
- (h 3, h 4, h 5)
val it = (6,24,120);
We might conjecture that h is actually the factorial function. By tracing h and extracting expression provenance, we
can confirm this guess (at least for the given inputs):
- trace (h (4@L));
val it = <trace> : ({L:int}, int) trace
- expression it;
val it = 24@{L * (L-1) * (L-2) * (L-3) * 1}
In this case, both where-provenance and dependency provenance would be uninformative since the result is not copied
from, and obviously depends on, the input.
This kind of provenance is used extensively in workflow systems often used in e-science [33], where the main
program is a high-level process coordinating a number of external (and often concurrent) program or RPC calls, for
example, image-processing steps or bulk data transformations, which we could model by adding primitive imageprocessing operations and types to our language. Thus, even though the above examples use fine-grained primitive
operations, this model is also useful for coarse-grained provenance-tracking.
A running example. Figure 1 graphically illustrates these three forms of provenance on a single example: a simple
function mapped over a list. This corresponds to the following TML sessions:
- val y = 2@L;
- fun f x = if x = y then y else x+1;
- val xs = [1@L1,2@L2,3@L3];
- val t = trace (map f xs);
val t = <trace> : ({L1:int,L2:int,L3:int}, int list) trace
- where t;
val it = [2@{},2@{L},4@{}]
- dependency t;
val it = [2@{L1,L},2@{L2,L},4@{L3,L}];
- expression t;
val it = [2@{L1+1},2@{L},4@{L3+1}];
Note that this illustrates much of the power of TML, including higher-order, recursive functions and sum, product and
recursive types. We use this as a running example throughout the paper.
Provenance security. The three models of provenance above represent useful forms of provenance that might increase users’ trust or confidence that they understand the results of a program. However, if the underlying data, or the
structure of the computation, is sensitive, then making this information available may lead to inadvertent vulnerabilities, by making it possible for users to infer sensitive information that they cannot observe directly. This is a particular
problem if we wish to disclose part of the result of a program, and provenance that justifies part of the result, while
keeping other parts of the program’s execution, input, or output confidential.
As a simple example, consider a program if x 6= 1 then (y, y) else (z, w). Suppose we wish to disclose some
information about the computation to an untrusted recipient Alice (not necessarily a malicious attacker), that none of
4

xs
1 2 3

y

map (λx.
if x = y
then y
else x+1)
xs

2 2 4

map (λx.
if x = y
then y
else x+1)
xs

2 2 4

map (λx.
if x = y
then y
else x+1)
xs

2 2 4

2

xs
1 2 3

y

2

xs
1 2 3

y

2

+1

copy
+1

Figure 1: Illustration of various forms of provenance

5

x, y are visible to Alice, that z, w are visible to Alice, and only the value of x is confidential. If z and w happen to both
equal a common value, say 42, then the result is (42, 42). It is safe to disclose this result to Alice, because (without
inspecting x or y) she cannot be certain whether x = 1, since there are two scenarios consistent with the result: x = 1
and y = 42 or x 6= 1 and y arbitrary. However, any of the above forms of provenance make it possible to distinguish
which branch was taken because the two different copies of 42 in z and w will have different provenance. Thus, if the
provenance information is released then a principal can infer that the second branch was taken, and hence, x = 1. In
technical terms, we cannot disclose any of the above forms of provenance for the result while obfuscating the fact that
x = 1.
To study these problems systematically, we introduce a single, general model of provenance that can be instantiated
in different ways to obtain the other models mentioned above (among many others). Essentially, our approach is to
record a detailed trace of evaluation, whose structure corresponds closely to that of a large-step operational semantics
derivation. Other forms of provenance can then be extracted by traversing the trace, and the trace itself can be viewed
as a form of provenance. Of course, naively recording such a detailed trace may be prohibitively expensive, and in this
article we are not advocating that such traces be explicitly constructed in practical systems, only that they are useful
as a formalism for understanding different forms of provenance and their security properties.

1.2

Summary

Contributions. In this article, we build on, and refine, the provenance security framework previously introduced
by Cheney [15]. We introduce a core language with replayable execution traces for a call-by-value, higher-order
functional language, and make the following technical contributions:
• Refined definitions of obfuscation and disclosure (Sec. 2).
• A core calculus defining traced execution for a pure functional programming language (Sec. 3).
• A generic provenance extraction framework that includes several previously-studied forms of provenance as
instances (Sec. 4).
• An analysis of disclosure and obfuscation guarantees provided by different forms of provenance, including
techniques based on slicing execution traces (Sec. 5).
This article is a revised and expanded version of a conference paper [3]. Compared with the conference paper, this
article includes detailed proofs, a more complete discussion of related work (including work published recently that
was not covered in the conference paper), and additional examples and discussion of technical points. In addition,
we encountered a problem with proving correctness of the disclosure slicing algorithm proposed in [3]; specifically,
Lemma 2 in the conference version had a subtle problem, which we avoid through a reformulation of the disclosure
slicing algorithm.
This article is also closely related to work on using traces for program slicing [40] published in ICFP 2012. The
two papers present different aspects of a single research project; the trace model and some aspects of the slicing
algorithms are closely related. However, the two papers make distinct contributions, and the system in the ICFP paper
incorporates simplifications that are appropriate pragmatic choices for its application area (program slicing) but not
appropriate for security analysis. Because of these differences we have chosen not to attempt to develop a unified
presentation or implementation, to ensure that focus in this article remains on provenance security. We summarize the
key differences below.
• In the ICFP paper, traces and slicing are defined in terms of an ad hoc semantics over partial values, and justified
by a Galois connection between them. Here, we instead define slices for disclosure and obfuscation in terms of
a standard operational semantics. One important consequence of these different choices is that unique minimal
disclosure slices do not exist, whereas unique minimal backwards slices do exist in the ICFP paper.
• The slicing algorithms in the ICFP paper differ from those given here in certain technical details: specifically,
we use value patterns and the hp equivalence relation instead of partial values, and we use ♦-patterns to support
slicing of primitive operations instead of tagging primitive operations with the values of their inputs in traces.
6

• The ICFP paper did not present provenance extraction or explore the connection to provenance security that is
the focus of this paper.
• The ICFP paper presents work on program slicing, differential slicing, and implementation techniques, topics
that are beyond the scope of this article.
Outline. Section 2 briefly recapitulates the framework introduced by Cheney [15] and refines some definitions. We
present the (standard) syntax and tracing semantics of TML in Section 3. In Section 4 we introduce a framework for
querying and extracting provenance views from traces, including the three models discussed above. Section 5 presents
our main results about disclosure, obfuscation, and trace slicing. Section 6 presents related work and Section 7
concludes.

2

Background

We recapitulate the main components of the provenance security framework of Cheney [15]. The framework assumes
a given set of abstract traces T , together with a collection Q of possible trace queries Q : T → B, where B = {0, 1}
is the set of Boolean truth values. These represent properties of traces that the system designer may want to protect or
that legitimate users or attackers of the system may want to learn. In the previous paper, we considered refinements to
take into account the knowledge of the principals about the possible system behaviors. In this article, we consider a
single principal and assume that all traces T are considered possible, for simplicity.
Fix a set Ω of the possible provenance views, and a function P : T → Ω mapping each trace to a provenance view
of the trace. We may write (Ω, P : T → Ω) or just (Ω, P ) for a provenance view. Also, we typically write q : Ω → B
for a provenance query, that is, a query on a provenance view.
Given this framework, we proposed the following definitions:
Definition 2.1 (Disclosure). A query Q : T → B is disclosed by a provenance view (Ω, P ) if for every t, t0 ∈ T , if
P (t) = P (t0 ) then Q(t) = Q(t0 ).
In other words, disclosure means that there can be no traces t, t0 that have the same provenance view but where
one satisfies the query and the other does not.
Definition 2.2 (Obfuscation). A query Q : T → B is obfuscated by a provenance view (Ω, P ) if for every t in T ,
there exists t0 ∈ T such that P (t) = P (t0 ) and Q(t) 6= Q(t0 ).
Thus, obfuscation is not exactly the opposite of disclosure; instead, it means that for every trace there is another
trace with the same provenance view but different Q-value. This means that a principal that has access to the provenance view but not the trace cannot be certain whether or not Q is satisfied by the underlying trace.
In the previous paper, we gave several examples of instances of this framework. Here, for illustration, we just
review one such instance, given by regular languages and finite automata.
Example 2.3 (Strings as traces). Consider the regular sublanguage of {a, b}+ consisting of nonempty strings; these
can be viewed as traces of an automaton or other sequential process. Some views of the traces of the automaton include
a transducer T1 replacing each symbol with a, a transducer T2 that deletes all of the as, and a transducer T3 that
deletes alternating symbols. A query over these traces can test whether the number of bs is even; this is obfuscated by
T1 , disclosed by T2 , and neither fully obfuscated nor fully disclosed by T3 .
When finite automata are used for queries and transducers for provenance views, we showed that disclosure is
decidable for all queries and views and that obfuscation is decidable for all queries and views whose range is finite. It
is unknown whether obfuscation is decidable in the general case.
The definitions above turn out to be too strong for our purposes; in this paper we will also consider some weaker
versions of disclosure and obfuscation.

7

Definition 2.4. A query Q : T → B is positively disclosed by provenance view (Ω, P ) via query q : Ω → B if for
every t, if q(P (t)) = 1 then Q(t) = 1.
A query Q : T → B is negatively disclosed by provenance view (Ω, P ) via query q : Ω → B if for every t, if
q(P (t)) = 0 then Q(t) = 0.
In other words, positive disclosure means that there is a query q on the provenance that safely overapproximates Q
on the underlying trace. If q(P (t)) holds then we know Q(t) holds but otherwise we may not learn anything about t.
Dually, negative disclosure means that if q(P (t)) is false then we know Q(t) is also false, but otherwise learn nothing.
Example 2.5. Suppose T = Ω = {a, b}∗ . Define query Q(t) to be true if and only if t is not of the form u · abab · v
for strings u, v, and let P (a1 a2 · · · an ) = a2 a4 · · · ab n2 c , the function that deletes alternate letters of its argument.
Finally, let q(t) be a query on Ω that is true if and only if t has no substrings of the form aa or bb. Then Q is positively
disclosed by P via q, for if P (t) has no aa or bb substring, then t can have no abab substring. However, Q is not
negatively disclosed by P (for any q 0 ), because, for example, P (abab) = bb = P (bbbb).
Definition 2.6. A query Q : T → B is positively obfuscated by (Ω, P ) if for every t satisfying Q(t) = 1 there exists
a trace t0 such that Q(t0 ) = 0 and P (t) = P (t0 ).
A query Q : T → B is negatively obfuscated by (Ω, P ) if for every t satisfying Q(t) = 0 there exists a trace t0
such that Q(t0 ) = 1 and P (t) = P (t0 ).
In other words, positive obfuscation means that the provenance never reveals that Q holds of the trace, but it may
reveal that Q fails. This weaker notion is useful for asserting that sensitive data is protected: if the sensitive data is
not present in the trace then it is harmless to reveal this, but if the sensitive data is present then the provenance should
hide enough information to make its presence uncertain. Dually, negative obfuscation means that the provenance view
does not reveal ¬Q.
Example 2.7. Again suppose T = Ω = {a, b}∗ . Define Q(t) to be true if and only if the number of a symbols in t
is odd and false otherwise. Define P (t) to be t with all as replaced by bs. (In other words, P (t) = b|t| , a string of
bs of the same length as t.) P positively obfuscates Q because if Q(t) holds, then t is a nonempty string with an odd
number of as, and we can form t0 such that P (t) = P (t0 ) by replacing one of the as of t with a b. However, P does
not negatively obfuscate Q because P () =  and there is no other string t0 with Q(t0 ) = true and P (t0 ) = .
Proposition 2.8. If P both positively discloses and negatively discloses Q via q, then P discloses Q. Similarly, if P
both positively and negatively obfuscates Q then P obfuscates Q.
Proof. For the first part, suppose P discloses Q positively and negatively via q. Let t, t0 ∈ T be given where P (t) =
P (t0 ). If q(P (t)) holds then q(P (t0 )) holds so Q(t) = 1 = Q(t0 ). If q(P (t)) = 0 then q(P (t0 )) = 0 and so
Q(t) = 0 = Q(t0 ).
The argument for obfuscation is straightforward.
Remark 2.9. It may seem surprising that positive and negative disclosure specify a provenance query q while full
disclosure does not specify such a parameter. If full disclosure holds, then there is no need to mention the provenance
query q that answers trace queries over Ω, since it is the characteristic function of {P (t) | Q(t) = 1}. However,
if we leave out (or existentially quantify over) the provenance query q in positive or negative disclosure, then both
definitions become trivial, since positive disclosure always holds for q(x) = 0 and negative disclosure always holds
for q(x) = 1. Moreover, we want to be able to decompose proving full disclosure into proving positive and negative
disclosure, but the argument given above requires that the positive and negative disclosure hold with respect to the
same q.
We now proceed to instantiate the framework with traces generated by a richer language, with corresponding
notions of trace query and provenance view.

8

Types

τ ::=

b | τ1 × τ2 | τ1 + τ2 | τ1 → τ2 | µα.τ | α

Type contexts

Γ ::=

[x1 : τ1 , . . . , xn : τn ]

κ ::=

f (x).e

Code pointers
Matches

m ::=

{inl(x1 ).e1 ; inr(x2 ).e2 }

Values

v ::=

c | (v1 , v2 ) | inl(v) | inr(v) | hκ, γi | roll(v)

Environments

γ ::=

[x1 7→ v1 , . . . , xn 7→ vn ]

Expressions

e ::=

c | x | ⊕(e) | let x = e1 in e2

Traces

|

(e1 , e2 ) | fst(e) | snd(e)

|

inl(e) | inr(e) | case e of m

|

fun κ | (e e0 )

|

roll(e) | unroll(e)

T ::=

c | x | ⊕(T ) | let x = T1 in T2

|

(T1 , T2 ) | fst(T ) | snd(T )

|

inl(T ) | inr(T ) | case T .inl x.T1 | case T .inr x.T2

|

fun κ | (T1 T2 ) .κ,Γ f (x).T

|

roll(T ) | unroll(T )

Figure 2: Abstract syntax of Core TML.

3

Core Language

We will develop a core language for provenance based on a standard, typed, call-by-value, pure language, called
Transparent ML, or TML. For the purpose of this article, we focus on terminating runs of pure computations. We
only consider terminating runs since otherwise there is no trace or end result to analyze; the question of how to deal
with provenance in nonterminating or effectful programs is interesting, but left for future work. Allowing for effects
or moving to a small-step semantics each seem likely to complicate the trace semantics (and subsequent analysis)
considerably.
The syntax of TML types, expressions, and other syntactic classes is shown in Figure 2. The syntax of expressions
and values is standard, following common textbook treatments of languages with binary pairs, binary sums, recursive
types, and recursive functions [41]; constructs such as boolean conditionals, records, datatypes, or mutually recursive
functions can be added without difficulty following the same pattern. We parameterize the syntax and semantics over
primitive operations ⊕ that take inputs of base type only; for example, equality on integers, arithmetic and boolean
operations. In f (x).e, both f and x are variable names; f is the name of the recursively defined function while x is
the name of the argument. Both f and x are bound in e in an expression of the form f (x).e; generally, we adhere to
the convention that in an expression of the form x.e, variable x is bound in e.
We abbreviate functional terms of the form f (x).e using the letter κ, when convenient; similarly, we often abbreviate the expression {inl(x1 ).e1 ; inr(x2 ).e2 } as m. We sometimes refer to κ or m as a code pointer or match pointer
respectively; in a fixed program, there are a fixed finite number of such terms and so we can share them instead of
explicitly copying them when used in traces.
The syntax of traces is also defined in Figure 2. Trace expressions T have many syntactic forms in common
with expressions; they differ primarily in the case and application trace forms, which include additional information
showing how an application or case expression was evaluated. Traces can be viewed as witnessing terms for the
operational derivation of an expression, and so their meaning is explained below along with that of the operational
semantics rules. We will refer to trace expressions T as TML-traces when necessary to distinguish them from abstract
traces T introduced in the previous section.

9

γ, e ⇓ v, T
γ, e ⇓ v, T
γ, c ⇓ c, c

γ, e1 ⇓ v1 , T1

γ, e1 ⇓ v1 , T1

ˆ
γ, ⊕(e) ⇓ ⊕(v),
⊕(T )

γ, x ⇓ γ(x), x
γ, e2 ⇓ v2 , T2

γ, (e1 , e2 ) ⇓ (v1 , v2 ), (T1 , T2 )

γ, e ⇓ (v1 , v2 ), T

γ, e ⇓ (v1 , v2 ), T

γ, fst(e) ⇓ v1 , fst(T )

γ, snd(e) ⇓ v2 , snd(T )

(inl(x1 ).e1 ∈ m)

γ, e ⇓ v, T
γ, inl(e) ⇓ inl(v), inl(T )

γ, e ⇓ inl(v), T

γ[x1 7→ v], e1 ⇓ v1 , T1

γ, case e of m ⇓ v1 , case T .inl x1 .T1

γ, e ⇓ v, T

(inr(x2 ).e2 ∈ m)

γ, inr(e) ⇓ inr(v), inr(T )

γ, e ⇓ inr(v), T

γ[x2 7→ v], e2 ⇓ v2 , T2

γ, case e of m ⇓ v2 , case T .inr x2 .T2

γ, e ⇓ v, T

γ, e ⇓ roll(v), T

γ, roll(e) ⇓ roll(v), roll(T )
0

γ, e1 ⇓ hκ, γ i, T1
γ, fun κ ⇓ hκ, γi, fun κ

γ[x 7→ v1 ], e2 ⇓ v2 , T2

γ, let x = e1 in e2 ⇓ v2 , let x = T1 in T2

γ, unroll(e) ⇓ v, unroll(T )

(κ = f (x).e)

γ, e2 ⇓ v2 , T2

γ 0 [f 7→ hκ, γ 0 i, x 7→ v2 ], e ⇓ v, T

γ, (e1 e2 ) ⇓ v, (T1 T2 ) .κ f (x).T

Figure 3: Dynamic semantics of Core TML: rules for expression evaluation.

3.1

Dynamic Semantics

We augment a standard large-step operational semantics for TML by adding a parameter T , which records a trace of
the evaluation of the expression. The judgment γ, e ⇓ v, T , defined in Figure 3, says that in environment γ, expression
e evaluates to value v with trace T .
If we ignore the trace parameter in this judgment, then the rules are essentially the standard ones for a call-by-value,
pure functional language with pairs, sums, and recursive types and functions [41]. In particular, pairs are constructed
by pairing and can be taken apart using the fst and snd operations. Values of sum type are constructed using the left
and right injection operations inl, inr and can be analyzed using the case expression, which examines a value of type
τ1 + τ2 and calls the appropriate branch with the injected value bound to a variable. Values of recursive type µα.τ
are constructed using roll and destructed using unroll; these operations indicate the explicit isomorphisms in the
isorecursive treatment of recursive types. Finally, functions are (as usual) constructed using the function expression
fun f (x).e and applied using function application e1 e2 .
Now if we consider the trace parameter, note that each rule has its own trace form, which builds the trace up from
sub-traces obtained by the hypotheses of the rule. Traces can contain bound variables, reflecting the binding structure
of the original expression. To illustrate, for let expressions, traces are similar to expressions:
let x = T1 in T2
where we bind the variable in T2 .
The case and application evaluation traces record additional information about control flow. In either case, the first
argument is evaluated to determine what expression to evaluate to obtain the final result. For case expressions, traces
are of the form:
case T .inl x1 .T1 case T .inr x2 .T2
where we record the trace of the case scrutinee T and the taken branch (T1 or T2 ), and we re-bind the variable (x1
or x2 ) in the trace of the taken branch. The subscript indicates which branch was taken. Similarly, for an application
expression:
(T1 T2 ) .κ f (x).T
we record the traces of the function subexpression T1 , the argument subexpression T2 , and the trace T of the evaluation
of the body of the function. The subscript κ = hf (x).e, Γi is a code pointer indicating the function and the typing
environment of the call. The Γ annotation is needed only to typecheck traces, so we usually elide it. Again, since the
body trace can mention the function and argument names as free variables, we re-bind these variables.
10

γ, T y v
γ, c y c

γ, x y γ(x)

γ, T1 y v1

γ, T y v
ˆ
γ, ⊕(T ) y ⊕(v)

γ, T2 y v2

γ, (T1 , T2 ) y (v1 , v2 )
γ, T y v

γ, T1 y v1

γ[x 7→ v1 ], T2 y v2

γ, let x = T1 in T2 y v2

γ, T y (v1 , v2 )

γ, T y (v1 , v2 )

γ, fst(T ) y v1

γ, snd(T ) y v2

γ, T y inl(v)

γ, inl(T ) y inl(v)

γ[x1 7→ v], T1 y v1

γ, case T .inl x1 .T1 y v1

γ, T y v

γ, T y inr(v)

γ, inr(T ) y inr(v)

γ[x2 7→ v], T2 y v2

γ, case T .inr x2 .T2 y v2

γ, T y v

γ, T y roll(v)

γ, roll(T ) y roll(v)

γ, unroll(T ) y v
0

γ, T1 y hκ, γ i

γ, T2 y v2

γ, fun κ y hκ, γi

γ 0 [f 7→ hκ, γ 0 i, x 7→ v2 ], T y v

γ, (T1 T2 ) .κ f (x).T y v

Figure 4: Dynamic semantics of Core TML: rules for trace replay.
We want to emphasize at this point that we do not necessarily expect that implementations routinely construct fully
detailed traces along the above lines. Rather, the trace semantics is proposed here as a candidate for the most detailed
form of provenance we will consider. Recording and compressing or filtering relevant information from traces in an
efficient way is beyond the scope of this paper. However, some preliminary experiments in this direction have been
performed in a recent paper on slicing for higher-order functional programs, based on a similar trace model [40].
Example 3.1. Consider the factorial program expressed in Core TML:
let f = fun f(x). if x = 0 then 1 else x*(f(x-1))
in f 4
The trace of this program has the form
let f = fun f(x). e
in f 4
|> f(x).(e |>_else x * (
f(x-1) |> f(x).(e |>_else x * (
f(x-1) |> f(x).(e |>_else x * (
f(x-1) |> f(x).(e |>_else x * (
f(x-1) |> f(x).(e |>_then 1)))))))))
where e = if x = 0 then 1 else x*(f(x-1)). The trace reflects that f calls itself four additional times
when evaluating f 4 and the else-branch is taken four times, and finally the then-branch is taken. Here, we use
subscripts then and else to indicate the branch taken instead of inl and inr.
Remark 3.2. The syntax of traces and expressions, and their corresponding evaluation rules, exhibit some redundancy. The syntax and semantics of expressions and traces could be fused so that both fall out as subsystems of one
joint syntax / semantics. We adopt an explicit treatment for clarity, despite the resulting redundancy.
The operational semantics rules in Figures 3 and 4 illustrate a recipe that appears straightforward to follow in
order to extend the system to a more realistic (pure) language; it is less clear how to extend the trace semantics
to handle effects, nontermination, or other features. It may be interesting to try to capture the recipe as a formal
construction over operational semantic specifications.

11

Trace Replay. We equip traces with a semantics that relates them to expressions. We write γ, T y v for the replay
relation that reruns a trace on an environment (possibly different from the one originally used to construct T ). Figure 4
shows the rules for replaying traces. The rules for most trace forms are the same as the standard rules for evaluating
the corresponding expression forms. Essentially, these rules require that the same control flow branches are taken as
in the original run. If the input environment is different enough that the same branches cannot be taken, then replay
fails.
Remark 3.3. This behavior should be contrasted with traces used in self-adjusting computation [4, 2]. Such traces
must always recompute the updated result; however, they typically operate at a coarser granularity by tracking reads
and writes to memory locations. Moreover, the traces are essentially graphs built in memory using references and
closures, so it is not straightforward to traverse such traces to obtain fine-grained information about what happened
at run-time, as we shall do in Section 4.
Like evaluation, replay is deterministic, in that if a trace can be replayed on an environment then the resulting
value is unique:
Theorem 3.4. If γ, T y v1 and γ, T y v2 then v1 = v2 .
Proof. Proof is by (straightforward) structural induction on the first derivation and inversion on the second.

3.2

Basic Properties of Traces

In this section, we identify key properties of traces, including type safety, and the consistency and fidelity properties
that characterize how traces record the evaluation of an expression.
Determinacy and Type Safety. We employ a standard type system for expressions. Figure 5 shows the (standard)
typing rules for expressions and Figure 6 shows the rules for values and environments. Type checking requires a
variable context Γ that maps variables to types. We write Γ ` e : τ to indicate that e has type τ in context Γ. Similarly,
we write Γ `T T : τ to indicate that T is a well-formed trace of type τ in context Γ. Figure 7 shows the typing rules
for traces. The unusual rules are those for case and application traces, whose form differs from the corresponding
expression forms. One important point is that in the rule for application traces, the trace of the function body needs to
typecheck in the same context Γ0 as the body of e. This is why we allow the annotation Γ0 indicating the environment
of the called function in application traces.
As noted above, expressions (and hence also traces) can be well-formed at more than one type, but this does not
matter since we are not concerned with typechecking algorithms here.
Theorem 3.5. If Γ ` e : τ and ` γ : Γ and γ, e ⇓ v, T then ` v : τ and Γ `T T : τ .
Proof. Proof is by induction on the structure of the evaluation derivation, using inversion on the typing derivation.
The only nonstandard cases are for the well-formedness of the trace, but these cases are straightforward.
Replay is also type-safe in the obvious sense:
Theorem 3.6. If Γ `T T : τ and ` γ : Γ and γ, T y v then ` v : τ .
Proof. Proof is by induction on the structure of the replay derivation; most cases are similar to analogous cases for
Theorem 3.5.
Consistency and Fidelity. We say that a trace T is consistent with an environment γ if there exists v such that
γ, T y v. A trace can easily be inconsistent with an environment, either because it is untyped nonsense and can never
run (e.g. fst(42)), or, more interestingly, because replaying leads to situations that disagree with the control flow of
the trace (e.g. while replaying case T .inl x1 .T1 , the replay of T yields inr(v)).
Evaluation produces consistent traces, and replaying a trace on the same input yields the same value:
Theorem 3.7 (Consistency). If γ, e ⇓ v, T then γ, T y v.
12

Γ`e:τ
c:τ ∈Σ

x:τ ∈Γ

Γ`c:τ

Γ`e:τ

Γ`x:τ
Γ ` e 1 : τ1

⊕ : τ → τ0 ∈ Σ

Γ ` ⊕(e) : τ

Γ ` e2 : τ2

Γ ` (e1 , e2 ) : τ1 × τ2
Γ ` e : τ1

Γ ` e : τ2

Γ ` inl(e) : τ1 + τ2

Γ ` inr(e) : τ1 + τ2

Γ ` e1 : τ1

0

Γ, x : τ1 ` e2 : τ2

Γ ` let x = e1 in e2 : τ2

Γ ` e : τ1 × τ2

Γ ` e : τ1 × τ2

Γ ` fst(e) : τ1

Γ ` snd(e) : τ2

Γ ` e : τ1 + τ2

Γ, x1 : τ1 ` e1 : τ

Γ, x2 : τ2 ` e2 : τ

Γ ` case x1 of {inl(e1 ).x2 ; inr(e2 ).e} : τ

Γ, f : τ1 → τ2 , x : τ1 ` e : τ2

Γ ` e1 : τ1 → τ2

Γ ` fun f (x).e : τ1 → τ2

Γ ` e2 : τ1

Γ ` (e1 e2 ) : τ2

Γ ` e : µα.τ

Γ ` e : τ [µα.τ /α]

Γ ` unroll(e) : τ [µα.τ /α]

Γ ` roll(e) : µα.τ

Figure 5: Well-typed expressions of TML.
`v:τ
c:τ ∈Σ
`c:τ
`γ:Γ

` v1 : τ1

` v 2 : τ2

` (v1 , v2 ) : τ1 × τ2

Γ, f : τ1 → τ2 , x : τ1 ` e : τ2

` hhf (x).e, Γi, γi : τ1 → τ2

` v : τ1

` v : τ2

` inl(v) : τ1 + τ2

` inr(v) : τ1 + τ2

` v : τ [µα.τ /α]
` roll(v) : µα.τ

` v1 : τ1

···

` vn : τn

` [x1 7→ v1 , . . . , xn 7→ vn ] : [x1 : τ1 , . . . , xn : τn ]

Figure 6: Value and environment typing.
Proof. Proof is by (straightforward) induction on the structure of derivations.
The converse does not hold: a trace can be consistent without ever being produced by running a program. In
particular, consistency does not check that the traces corresponding to bodies of function calls match the code pointers
recorded in the trace. It is possible to refine the definition of replay so that the function bodies are checked against
the traces, providing a stronger notion of consistency. However, this would complicate the replay semantics. In the
rest of this article we usually consider traces obtained by running the tracing semantics. When this is the case, the
derivation of γ, e ⇓ v, T is itself a witness to this, so there is no need to introduce an additional judgment that captures
this invariant.
Furthermore, the trace produced by evaluation is faithful to the original expression, in the sense that whenever the
trace can be successfully replayed on a different input, the result (and its trace) is the same as what we would obtain
by rerunning e from scratch, and the resulting trace is the same as well. We call this property fidelity.
Theorem 3.8 (Fidelity). If γ, e ⇓ v, T and γ 0 , T y v 0 then γ 0 , e ⇓ v 0 , T .
Proof. Straightforward proof by induction on the structure of derivations. The interesting cases are for case and
application expressions; in each case, the induction hypothesis ensures that the intermediate sum or function value
encountered when recomputing e in γ 0 matches that in the original derivation, so that the subtraces contingent on this
value can be reused.
Intuitively, fidelity corresponds to a repeatability or reproducibility property: it does not just guarantee that we get
the same results when the trace is replayed on the same input, it also guarantees that the trace tells us what would
happen if we rerun on inputs that are similar enough to the original input that replay can succeed. Thus, traces
correspond to a form of explanation, analogous to forms of explanation explored in causal models and workflow
provenance [14, 30, 31]. While we do not make more of this connection here, fidelity is also related to the correctness
properties for various forms of slicing, including disclosure slicing (as discussed in Section 5).
13

Γ `T T : τ
c:τ ∈Σ

x:τ ∈Γ

Γ `T c : τ

Γ `T x : τ
Γ `T T1 : τ1

⊕ : τ → τ0 ∈ Σ

Γ `T T : τ

Γ `T T2 : τ2

Γ `T (T1 , T2 ) : τ1 × τ2
Γ `T T : τ1

Γ `T T1 : τ1

Γ `T ⊕(T ) : τ 0

Γ `T T : τ1 + τ2

Γ `T inl(T ) : τ1 + τ2

Γ, x : τ1 `T T2 : τ2

Γ `T let x = T1 in T2 : τ2

Γ `T T : τ1 × τ2

Γ `T T : τ1 × τ2

Γ `T fst(T ) : τ1

Γ `T snd(T ) : τ2

Γ, x1 : τ1 ` e1 : τ

Γ, x2 : τ2 ` e2 : τ

Γ, x1 : τ1 `T T1 : τ

Γ `T case T of {inl(x1 ).e1 ; inr(x2 ).e2 } .inl x1 .T1 : τ
Γ `T T : τ1 + τ2

Γ `T T : τ2
Γ `T inr(T ) : τ1 + τ2

Γ, x1 : τ1 ` e1 : τ

Γ, x2 : τ2 ` e2 : τ

Γ, x2 : τ2 `T T2 : τ

Γ `T case T of {inl(x1 ).e1 ; inr(x2 ).e2 } .inr x2 .T2 : τ
Γ, f : τ1 → τ2 , x : τ1 ` e : τ2
Γ `T fun f (x).e : τ1 → τ2

Γ `T T1 : τ1 → τ2

0

Γ , f :τ1 → τ2 , x:τ1 ` e : τ2

Γ `T T2 : τ1

Γ0 , f :τ1 → τ2 , x:τ1 `T T : τ2

Γ `T (T1 T2 ) .f (x).e,Γ0 f (x).T : τ2
Γ `T T : µα.τ

Γ `T T : τ [µα.τ /α]

Γ `T unroll(T ) : τ [µα.τ /α]

Γ `T roll(T ) : µα.τ

Figure 7: Well-typed traces of TML.
Remark 3.9. As noted at the beginning of the section, we made two simplifying assumptions: we consider traces
only for terminating runs, and we exclude side-effects from the language. These assumptions are reasonable for
many application areas of provenance (for example, in scientific computation and databases), but it is naturally of
interest to consider extending our approaches to trace nonterminating or effectful computations. These raise potential
complications: for example, adapting the trace semantics to a small-step semantics seems nontrivial, and it is not
as clear what the appropriate correctness properties are for traces involving effects (including nondeterminism or
allocation). These are interesting areas for exploration in future work.

4

Provenance Views and Extraction

In this section we consider different kinds of views and queries over provenance traces. To be specific, we consider
a consistent triple (γ, T, v) where γ, T y v to be the “traces” in the sense of the provenance security framework.
Then queries over these triples correspond to sets of triples (generally definable using some compact syntax), and
views correspond to functions from triples to some other data. We first consider a general class of views definable
using annotation propagation, by giving a generic framework for extracting other kinds of provenance from execution
traces. These forms of provenance induce provenance views in a natural way if we allow for initial annotations that
uniquely identify each part of a value by a path.

4.1

Annotations, Paths, and Provenance Extraction

Many previous approaches to provenance can be viewed as performing a form of annotation propagation. The idea
is to decorate the input with annotations (often, initially, unique identifiers) and propagate the annotations through
the evaluation. For example, in where-provenance, annotations are optional tags that can be thought of as pointers
showing where output data was copied from in the source [11, 10]. Other techniques, such as why-, how-, and
dependency provenance, can also be defined in terms of annotation propagation [28, 27, 9, 18]. We gave similar
definitions of different forms of provenance using a common framework for XQuery [13]; some of the properties
proved are generalizations of properties shown there or in [10].

14

|[x1 7→ v1 , . . . , xn 7→ vn ]|
a

=

[x1 7→ |v1 |, . . . , xn 7→ |vn |]

|c |

=

c

|(b
v1 , vb2 )a |

=

(|b
v1 |, |b
v2 |)

|inl(b
v )a |

=

inl(|b
v |)

|inr(b
v )a |

=

inr(|b
v |)

|hκ, γ
b ia |

=

hκ, |b
γ |i

|roll(b
v )a |

=

roll(|b
v |)

Figure 8: Erasure operation.
occ(ca )

=

{ca }

occ((b
v1 , vb2 )a )

=

{(b
v1 , vb2 )a } ∪ occ(b
v1 ) ∪ occ(b
v2 )

occ((inl(b
v )) )

=

{(inl(b
v ))a } ∪ occ(b
v)

occ((inr(b
v ))a )

=

{(inr(b
v ))a } ∪ occ(b
v)

occ((roll(b
v )) )

=

{(roll(b
v ))a } ∪ occ(b
v)

occ(hκ, γ
b ia )

=

occ(b
γ)

=

{hκ, γ
bia } ∪ occ(b
γ)
[
occ(b
γ (x))

a

a

x∈dom(b
γ)

Figure 9: Occurrences of annotated values.
Based on this observation, we define a provenance extraction framework in which values are decorated with annotations and extraction functions take traces and return annotated values that can be interpreted as useful provenance
information. We first define annotated values and give a generic annotation-propagation operation. We apply this
framework to specify several concrete annotation schemes and extraction functions.
Annotations. Let A be an arbitrary set of annotations a, which we usually assume includes a blank annotation ⊥
and a countably infinite set of identifiers ` ∈ Loc, called locations. We define A-annotated values vb (or just annotated
values, when A is clear) using the following grammar:
vb ::=
γ
b ::=

wa
[x1 7→ vb1 , . . . , xn 7→ vbn ]

w

c | (b
v1 , vb2 ) | inl(b
v ) | inr(b
v ) | hκ, γ
bi | roll(b
v)

::=

We write γ
b for annotated environments mapping variables to annotated values. We define an erasure function |b
v | that
maps each annotated value to an ordinary value by erasing the annotations. Similarly, |b
γ | is the ordinary environment
obtained by erasing the annotations from the values of γ
b. This function is defined mutually recursively on annotated
values and environments as shown in Figure 8. We also introduce a notation for the set of annotated values occurring
in a value in Figure 9. Moreover, we write
occ 6⊥ (b
v ) = {wa ∈ occ(b
v ) | a 6= ⊥}
for the set of annotated values with annotation a 6= ⊥.
Paths as annotations. For annotations to be useful when the full input is unavailable, we consider annotations where
the locations ` are paths that uniquely address parts of the input environment. Paths π have syntax:
π ::=  | x.π | 1.π | 2.π
15

v[]

=

v

(v1 , v2 )[1.π]

=

v1 [π]

(v1 , v2 )[2.π]

=

v2 [π]

(inl(v))[1.π]

=

v[π]

(inr(v))[1.π]

=

v[π]

(roll(v))[1.π]

=

v[π]

(hκ, γi)[1.π]

=

γ[π]

γ[x.π]

=

γ(x)[π]

Figure 10: Path lookup operation.

pathπ (γ)

=

[x1 7→ pathπ.x1 (γ(x1 )), . . . , xn 7→ pathπ.xn (γ(xn ))]

pathπ (c)

=

cπ

pathπ ((v1 , v2 ))

=

(pathπ.1 (v1 ), pathπ.2 (v2 ))π

pathπ (inl(v))

=

inl(pathπ.1 (v))π

pathπ (inr(v))

=

inr(pathπ.1 (v))π

pathπ (hκ, γi)

=

hκ, pathπ.1 (γ)iπ

Figure 11: Path annotation operation.
and we consider path concatenation π.π 0 to be associative with unit , so that we may write π.i to construct a pattern
ending in i. Paths address parts of values or environments; we write v[π] or γ[π] for the part of v or γ addressed by π,
defined in Figure 10.
We write path(γ) for the environment γ with each component annotated with the path to that component. More
generally, we define pathπ (γ) and pathπ (v) as shown in Figure 11. Then path(v) = path (v) and path(γ) =
path (γ). For example, path([x 7→ (1, 2), y 7→ inl(4)]) = [x 7→ (1x.1 , 2x.2 )x , y 7→ inl(4y.1 )y ].
Extraction framework. We will define a family of provenance extraction functions F(T, γ
b) that take a trace T and
an environment γ
b and return an annotated value. Each such F can be specified by giving the following annotationpropagation functions:
Fc , F κ
F1 , F2 , FL , FR , Fapp , Funroll
F⊕

: A
: A×A→A
: An → A

(where ⊕ is n-ary)

Each function shows how the annotations involved in the corresponding computational step propagate to the result.
For example, F1 (a, b) gives the annotation on the result of a fst-projection, where a is the annotation on the pair and
b is the annotation of the first element. Figure 12 shows how to propagate annotations through a trace given basic
annotation-propagation functions.
Remark 4.1. The extraction framework hard-wires the behavior of certain operations such as let, inl(), inr(),roll(),
and pairing, using ⊥ to handle all of them. On the other hand, even though these constructors are hard-wired so that
the top-level annotation is always ⊥, this does not imply that the first arguments supplied to the corresponding extraction functions F1 , F2 , etc. are always ⊥; see Example 4.13 for an illustration of this point.
It would also be possible to extend the framework to allow greater customization; however, this functionality is
not needed by any of the forms of provenance in this article. We believe that the framework presented in this paper is

16

F(x, γ
b)
F(let x = T1 in T2 , γ
b)
F(c, γ
b)
F(⊕(T1 , . . . , Tn ), γ
b)
F((T1 , T2 ), γ
b)
F(fst(T ), γ
b)
F(snd(T ), γ
b)
F(inl(T ), γ
b)
F(inr(T ), γ
b)
F((case T ) .inl x.T1 , γ
b)

=
=
=
=
=
=
=
=
=
=

γ
b(x)
F(T2 , γ
b[x7→F(T1 , γ
b)])
c Fc
ˆ 1 , . . . , cn ))F⊕ (a1 ,...,an )
(⊕(c
(F(T1 , γ
b), F(T2 , γ
b))⊥
F1 (a,b)
v1
F (a,b)
v2 2
inl(F(T, γ
b))⊥
inr(F(T, γ
b))⊥
FL (a,b)
v

F((case T ) .inr y.T2 , γ
b)

=

v FR (a,b)

F(fun κ, γ
b)
F((T1 T2 ) .κ f (x).T, γ
b)

=
=

hκ, γ
b i Fκ
Fapp (a,b)
v

F(roll(T ), γ
b)
F(unroll(T ), γ
b)

=
=

roll(F(T, γ
b))⊥
v Funroll (a,b)

where

cai i = F(Ti , γ
b)

where
where

(v1b , vb2 )a = F(T, γ
b)
b a
(b
v1 , v2 ) = F(T, γ
b)

where
and
where
and

inl(b
v )a = F(T, γ
b)
b
v = F(T1 , γ
b[y7→vb])
inr(b
v )a = F(T, γ
b)
b
v = F(T2 , γ
b[y7→vb])

where
and
and

hκ, γ
b0 ia = F(T1 , γ
b)
vb2 = F(T2 , γ
b)
v b = F(T, γ
b0 [f 7→hκ, γ
b0 ia , x7→vb2 ]))

where

roll(v b )a = F(T, γ
b)

Figure 12: Generic extraction.
general enough to be of use beyond the three provenance models we considered, but we do not know how one could
prove that it is general enough for all purposes — or how one could prove that any alternative framework is general
enough for all purposes. It is also possible that there are natural forms of provenance that do not fit (a reasonable
generalization of) the framework.
Theorem 4.2. Every generic provenance extraction function is compatible with replay: that is, for any γ
b, T, v, if
|b
γ |, T y v then |F(T, γ
b)| = v.
Proof. Straightforward induction on replay derivations.
Remark 4.3. Consider the trivial annotation structure Triv with underlying annotation set {⊥}. In this setting,
the erasure function | − | is bijective; its inverse just decorates each part of a value with ⊥. Consider also a trivial instance of the generic provenance framework for {⊥} such that Trivκ = ⊥ and Trivc = ⊥ and all of the
annotation-propagation functions are constant functions returning ⊥, that is, Triv1 (x, y) = ⊥, etc. This instance of
the provenance framework is essentially the same as the trace replay semantics defined by the judgment γ, T y v.
Thus, the generic extraction framework can be viewed as a denotational presentation of the replay semantics of traces,
generalized to allow for annotated values.
Where-provenance. Where-provenance can be defined via an annotation-propagating semantics where annotations
are either labels ` or the blank annotation ⊥. Intuitively, for where-provenance, an explicit label ` annotating a part
of the input indicates that that part “comes from” a part of the input with the same label; an annotation ⊥ provides no
information about where the output part “comes from” in the input (if anywhere). We define the where-provenance
semantics W(T, γ
b) using the following annotation-propagation functions:
Wc , Wκ
W1 , W2 , WL , WR , Wapp , Wunroll
W⊕

= ⊥
= λ(x, y).y
= λ(a1 , . . . , an ).⊥

Essentially, these functions preserve the annotations of data that are copied, and annotate computed or constructed
data with ⊥. This semantics is similar to that in Buneman et al. [10] and previous treatments of where-provenance in
17

W(c, γ
b)
W(⊕(T1 , . . . , Tn ), γ
b)
W(fst(T ), γ
b)
W(snd(T ), γ
b)
W((case T ) .inl x.T1 , γ
b)
W((case T ) .inr y.T2 , γ
b)
W(fun κ, γ
b)
W((T1 T2 ) .κ f (x).T, γ
b)

=
=
=
=
=
=
=
=

c⊥
ˆ 1 , . . . , cn ))⊥
(⊕(c
vb1
vb2
W(T1 , γ
b[x7→vb])
W(T2 , γ
b[y7→vb])
hκ, γ
b i⊥
W(T, γ
b0 [f 7→hκ, γ
b0 ia , x7→vb])

W(unroll(T ), γ
b)

=

vb

where
where
where
where
where

cai i = W(Ti , γ
b)
(b
v1 , vb2 )a = W(T, γ
b)
(b
v1 , vb2 )a = W(T, γ
b)
inl(b
v )a = W(T, γ
b)
inr(b
v )a = W(T, γ
b)

where
and
where

hκ, γ
b0 ia = W(T1 , γ
b)
vb = W(T2 , γ
b)
roll(b
v )a = W(T, γ
b)

Figure 13: Where-provenance extraction (selected cases).
databases, adapted to TML. Figure 13 shows the generic semantics specialized to where-provenance. Note that for a
function like “factorial”, the where-provenance of the output is always ⊥.
Example 4.4. Recall the example program from Section 1.1:
let y = 2@L in
let f x = if x = y then y else x+1 in
map f [1@L1,2@L2,3@L3]
The result of the where-provenance extraction semantics applied to this program is [2, 2L , 4], as shown graphically in
Figure 1, showing that the second result element is copied from y and giving no information about the other two.
To state the key property of where-provenance, we use the function occ introduced earlier in this section. The key
property of where-provenance is that if an annotated value wa appears in W(T, γ
b) with annotation a 6= ⊥, then wa is
an exact copy (including any nested annotations) of a part of γ
b.
Theorem 4.5. Suppose |b
γ |, e ⇓ v, T . Then occ 6⊥ (W(T, γ
b)) ⊆ occ 6⊥ (b
γ ).
Proof. See Appendix A.1.
Remark 4.6. Buneman et al. [10] consider a where-provenance semantics for database query and update languages
(with nested collection types and pairs, but no recursion or datatypes), which we adapt here to a conventional functional language (with recursion and datatypes, but no collection types). The basic idea, propagating annotations from
the input to output when data are copied, is the same. They did not propose a tracing model of their calculus, but
instead defined where-provenance via a syntactic translation that inserts annotation propagation code. The correctness property we discuss here corresponds to their copying property [10, Prop. 5.5]. They studied additional query
normalization and semantic expressiveness properties that we do not address here.
Expression provenance. To model expression provenance, we consider expression annotations t consisting of labels
`, blanks ⊥, constants c, or primitive function applications ⊕(t1 , . . . , tn ).
t ::= ` | c | ⊕(t1 , . . . , tn ) | ⊥
Intuitively, a label ` indicates that a part of the output is copied from a part of the input with the same label; a constant
c indicates an output part that is built by evaluating constant in the program; a term ⊕(t1 , . . . , tn ) indicates a part of
the output that is computed by evaluating ⊕ on values obtained from t1 , . . . , tn , and ⊥ provides no information about
how a part of the output was computed from the input. We define expression-provenance extraction E(T, γ
b) in much
the same way as W, with the following differences:
Ec = c

E⊕ (t1 , . . . , tn ) = ⊕(t1 , . . . , tn )

Figure 14 shows the generic semantics specialized to expression-provenance.
18

E(c, γ
b)
E(⊕(T1 , . . . , Tn ), γ
b)
E(fst(T ), γ
b)
E(snd(T ), γ
b)
E((case T ) .inl x.T1 , γ
b)
E((case T ) .inr y.T2 , γ
b)
E(fun κ, γ
b)
E((T1 T2 ) .κ f (x).T, γ
b)

=
=
=
=
=
=
=
=

cc
ˆ 1 , . . . , cn ))⊕(t1 ,...,tn )
(⊕(c
vb1
vb2
E(T1 , γ
b[x 7→ vb])
E(T2 , γ
b[y 7→ vb])
hκ, γ
b i⊥
E(T, γ
b0 [f 7→hκ, γ
b0 it , x7→vb)

E(unroll(T ), γ
b)

=

vb

where
where
where
where
where

ctii = E(Ti , γ
b)
(b
v1 , vb2 )t = E(T, γ
b)
(b
v1 , vb2 )t = E(T, γ
b)
E(T, γ
b) = inl(b
v )t
E(T, γ
b) = inr(b
v )t

where
and
where

hκ, γ
b0 it = E(T1 , γ
b))
vb = E(T2 , γ
b)
roll(b
v )t = E(T, γ
b)

Figure 14: Expression provenance extraction (selected cases).
Example 4.7. Continuing with the map example from Section 1.1, the result of the expressione-provenance extraction
semantics applied to this program is [2L1 +1 , 2L , 4L3 +1 ], as shown graphically in Figure 1. This shows that the second
result element is copied from y and the other two arguments are computed by incrementing the first and last elements
of the input, respectively. Observe that this is strictly more informative than the where-provenance.
The correctness property for expression provenance states that the expression annotation correctly recomputes the
value it annotates. To formalize this, we use the auxiliary definitions occ(), occ 6⊥ () introduced for where-provenance.
Let h : Loc → Val be a function from locations to values, and let h(t) be the value obtained by evaluating annotation
term t with values from h substituted for locations in t. We say that h is consistent with vb if whenever wt ∈ occ 6⊥ (b
v ),
we have h(t) = |w|. Similarly, h is consistent with γ
b if whenever wt ∈ occ 6⊥ (b
γ ), we have h(t) = |w|. We note that
for any distinctly-annotated value, for example path(γ), there is always a consistent mapping h, obtained by mapping
` to |w| whenever w` ∈ occ(b
γ ).
Example 4.8. Consider γ = [x 7→ (1, 2), y 7→ inl(3)] and γ
b = path(γ) = [x 7→ (1x.1 , 2x.2 )x , y 7→ inl(3y .1)].
Then the consistent mapping h is defined as follows:
h(x)
h(y)

=
=

(1, 2)
inl(3)

h(x.1) = 1
h(y.1) = 3

h(x.2)

=

2

Observe in particular that this illustrates that |b
γ | is typically not a consistent mapping for γ
b (since in this example,
|b
γ | = γ 6= h).
Theorem 4.9. Suppose |b
γ |, e ⇓ v 0 , T . Then if h is consistent with γ
b, then h is also consistent with E(T, γ
b).
Proof. Similar to the proof of Theorem 4.5. See Appendix A.2.
Dependency provenance. To extract dependency provenance (adapting the definition from [17]) we will use annotations φ that are sets of source locations {`1 , . . . , `n }, and we take the default annotation ⊥ to be the empty set ∅.
Initial annotations consist of disjoint singleton sets {`}. We define (b
v )+a to mean adding annotations a to the top-level
a
a +b
a∪b
of vb = w ; that is, (w ) = w . We define D(T, γ
b) using the following propagation functions:
D c , Dκ

=

∅

D1 , D2 , DL , DR , Dapp , Dunroll

=

λ(x, y).x ∪ y

D⊕

=

λ(a1 , . . . , an ).a1 ∪ · · · ∪ an

This semantics is based on the dynamic provenance tracking semantics given by Cheney et al. [17], generalized to
TML. Figure 15 shows the generic semantics specialized to dependency-provenance.
Example 4.10. Continuing with the map example from Section 1.1, the result of the dependency-provenance extraction semantics applied to this program is [2L1 ,L , 2L1 ,L , 4L3 ,L ], as shown graphically in Figure 1. This shows that all
three arguments depend on both L and on the respective element of the input list. This information is not computable
from the where-provenance or expression-provenance, or vice versa.
19

c∅
S
ˆ 1 , . . . , cn )) i φi
(⊕(c

D(c, γ
b)
D(⊕(T1 , . . . , Tn ), γ
b)
D(fst(T ), γ
b)
D(snd(T ), γ
b)
D((case T ) .inl x.T1 , γ
b)
D((case T ) .inr y.T2 , γ
b)
D(fun κ, γ
b)
D((T1 T2 ) .κ f (x).T, γ
b)

=
=
=
=
=
=
=
=

(b
v1 )
(b
v2 )+φ
D(T1 , γ
b[x7→vb])+φ
D(T2 , γ
b[y7→vb])+φ
∅
hκ, γ
bi
D(T, γ
b0 [f 7→hκ, γ
b0 iφ , x7→vb])+φ

D(unroll(T ), γ
b)

=

(b
v )+φ

+φ

where
where
where
where
where

cφi i = D(Ti , γ
b)
(b
v1 , vb2 )φ = D(T, γ
b)
(b
v1 , vb2 )φ = D(T, γ
b)
inl(b
v )φ = D(T, γ
b)
inr(b
v )φ = D(T, γ
b)

where
and
where

hκ, γ
b0 iφ = D(T1 , γ
b)
vb = D(T2 , γ
b)
roll(b
v )φ = D(T, γ
b)

Figure 15: Dependency provenance extraction.
vb ≈` vb0

vb1 ≈` vb10
(b
v1 , vb2 )

w ≈` w 0

` ∈ φ ∩ φ0

wφ ≈` (w0 )φ

wφ ≈` (w0 )φ

vb2 ≈` vb20
≈` (b
v10 , vb20 )

0

vb ≈` vb

0

c ≈` c

0

inl(b
v ) ≈` inl(b
v0 )

vb ≈` vb

inr(b
v ) ≈` inr(b
v0 )

vb ≈` vb0

roll(b
v ) ≈` roll(b
v0 )

γ ≈` γ 0
hκ, γi ≈` hκ, γ 0 i

γ ≈` γ 0 ⇐⇒ ∀x ∈ dom(γ) ∪ dom(γ 0 ). γ(x) ≈` γ 0 (x)

Figure 16: Equal-except-at relation
This definition satisfies the dependency-correctness property introduced in [17]. As explained in Cheney et al. [17],
dependency-correctness is intuitively motivated by analogy to dependency-tracking and information flow analyses,
following the dependency core calculus of Abadi et al. [1]. Analogously to noninterference in information flow
security, we define an auxiliary relation ≈` , where v ≈` v 0 intuitively says that two annotated values are equal except
(possibly) at parts labeled by `, defined as shown in Figure 16. The ≈l relation is reflexive, symmetric and transitive,
and in particular c ≈` c for any `, since c = c, whereas c` ≈` d` holds even though c 6= d, because both are labeled
by `.
As discussed in [17], for distinctly-annotated values, v ≈` v 0 holds if and only if v and v 0 are of the form C[v0 ]
and C[v00 ], where C[] is a context capturing the common parts of v and v 0 (above `), and v0 and v00 are subvalues
showing where v and v 0 differ (below `). However, during propagation of dependency annotations, values do not
remain distinctly-annotated, and the ≈` relation is an appropriate generalization of this property.
Then we can show:
Theorem 4.11. Suppose |b
γ |, e ⇓ v, T and γ
b 0 ≈` γ
b and |b
γ 0 |, e ⇓ v 0 , T 0 . Then we have D(T, γ
b) ≈` D(T 0 , γ
b0 ).
Proof. See Appendix A.3.
This says that the label of a value in the input propagates to all parts of the output where changing the value can
have an impact on the result.
Example 4.12. Revisiting the previous example, dependency-correctness has several implications for output [2L1 ,L , 2L2 ,L , 4L3 ,L ].
Taking ` = L, dependency-correctness tells us that if the value of y were changed, all three parts of the output list
might change. If ` = L1 , then dependency-correctness implies that the output will be of the form [v, 2, 4] for some
value v (which by type-safety must be an integer also). Similarly, dependency-correctness implies that if L2 or L3
change then the output will be of the form [2, v, 4] or [2, 2, v] respectively.
Dependency-correctness does not provide a guarantee concerning the effects of multiple, independent changes at
different locations (although an approximation of this information is available by using a single location that includes

20

both changes). Also, in all cases, the structure of the output list cannot change, because we cannot change the length
of the input list by changing y or changing the values of elements of the list.
Example 4.13. Consider a trace T = fst(x) evaluated in environment γ = [x 7→ (1a , 2b )c ], whose result is
D(T, γ) = 1D1 ({a},{b}) = 1a,b . This can naturally happen if the pair is a part of the (annotated) input, rather than
being constructed by the program. This example illustrates that although the annotations of pairs, sum injections, and
other constructors are hard-wired to be ⊥, this does not mean that the binary functions F1 , F2 etc. are always called
with ⊥ as the first argument.
Remark 4.14. Cheney et al. [17] considered a query language with nested collection types (similar to that used by
Buneman et al. [10]). That language included an equality operation at all types, and the dependency provenance
semantics for equality made use of another operation kb
v k that collects all of the annotations in vb. Here, we only
consider equality at base types, and so it suffices to consider only local annotations during propagation.

5

Disclosure and obfuscation analysis

In the previous sections we have defined a trace model for Core TML and defined certain classes of trace queries,
provenance views, and introduced technical machinery such as paths and partial values. In this section we put these
components to work by investigating the disclosure and obfuscation problems for Core TML traces and provenance
views. We confine attention to queries that test properties of the input or output. Investigating queries that capture
properties of the trace is more difficult, since traces involve variable binding, whereas for values we have restricted
attention to queries formulated in terms of partial values.

5.1

Patterns, partial traces, and trace queries

In section 2, we reviewed and refined a general provenance framework with definitions of disclosure and obfuscation,
formulated in terms of abstract sets of traces. We now introduce additional concepts needed to formulate the TML
model of provenance as an instance of the abstract provenance framework in section 2, so that we can analyze the
security properties of TML-traces. Specifically, we will consider a consistent triple (γ, T, v) as an abstract trace, we
will define some provenance queries over such traces, and we will consider some approaches to defining provenance
views of the traces. The queries and views rely on notions of patterns and partial traces; specifically, we will consider
queries based on testing whether a partial value is present in the input or output, and we will consider views based on
deleting information from the trace, input or output.
We introduce patterns for values, environments and traces. The syntax of patterns (pattern environments) is similar
to that of values (respectively environments), extended with special holes:
p

::= c | (p1 , p2 ) | inl(p) | inr(p) | roll(p) | hκ, ρi | ♦ | 

ρ ::=

[x1 7→ p1 , . . . , xn 7→ pn ]

Patterns actually denote binary relations on values. The hole symbol  denotes the total relation, while the exactmatch symbol ♦ denotes the identity relation. The ♦ pattern is a technical device used later in this section in backward
disclosure slicing; we sometimes refer to ♦-free patterns that do not contain ♦.
We say that v matches v 0 modulo p (written v hp v 0 ) if v and v 0 match the structure of p, and are equal at
corresponding positions denoted by ♦. Moreover, we write p t p0 for the least upper bound (join) of two patterns and
define p v p0 to hold if p0 = p t p0 . Rules defining hp and t are given in Figures 17 and 18. In the equations defining
p t ♦, we use notation p[♦/] to denote the result of replacing all occurrences of  in p with ♦.
When p v v, we write v|p for the pattern obtained by replacing all of the ♦-holes in p with the corresponding

21

v hp v 0
v2 hp2 v20

v1 hp1 v10
v h v

0

v h♦ v

c hc c

(v1 , v2 )

v hp v 0

h(p1 ,p2 ) (v10 , v20 )

v hp v 0
0

inl(v) hinl(p) inl(v )

v hp v 0

γ hρ γ 0

roll(v) hroll(p) roll(v 0 )

hκ, γi hhκ,ρi hκ, γ 0 i

γ hρ γ 0

inr(v) hinr(p) inr(v 0 )

∀x ∈ dom(ρ). γ(x) hρ(x) γ 0 (x)

⇐⇒

Figure 17: Equality modulo patterns.
values in v, defined as follows:
v|

=



v|♦

=

v

c|c

=

c

(v1 , v2 )|(p1 ,p2 )

=

(v1 |p1 , v2 |p2 )

inl(v)|inl(p)

=

inl(v|p )

inr(v)|inr(p)

=

inr(v|p )

roll(v)|roll(p)

=

roll(v|p )

hκ, γi|hκ,ρi

=

hκ, γ|ρ i

[x1 7→ v1 , . . . , xn 7→ vn ]|[x1 7→p1 ,...,xn 7→pn ]

=

[x1 := v1 |p1 , . . . , xn := vn |pn ]

For example, (1, 2)|(♦,) = (1, ).
Lemma 5.1. For any v and p v v, we have v hp v|p .
Lemma 5.2. The set {p | p v v} of partial values matching a given value v is an upper semilattice with least element
, greatest element v and the least upper bound operation t as defined in Figure 18.
Lemma 5.3. For each p, hp is a partial equivalence relation. Moreover, whenever p t p0 is defined, we have
(hptp0 ) = (hp ) ∩ (hp0 ), and whenever p v p0 we have (hp ) ⊇ (hp0 ).
Proof. To show hp is a partial equivalence relation, we must show that it is symmetric and transitive (but not necessarily reflexive). Symmetry follows by straightforward induction on derivations. Transitivity is by induction on p. The
second part follows by induction on the (partial recursive) definition of t. The third part follows from the second by
the fact that p v p0 holds if and only if p t p0 = p0 . Full details of the proof are in Appendix A.4.
Lemma 5.4. If v hp v 0 then p v v and p v v 0 . Conversely, if p v v then v hp v.
Proof. By induction on derivations. By symmetry it suffices to show by induction that v hp v 0 implies p v v. The
second part is straightforward.
We also consider partial traces, usually written S, which are trace expressions where some subexpressions have
been replaced with :
S

::= · · · | 

As with patterns, we write S v T to indicate that T matches S, that is, S can be made equal to T by filling in some
holes.
As mentioned at the beginning of this section, for the purpose of disclosure and obfuscation analysis, we will
consider the “traces” to be triples (γ, T, v) where T is consistent with γ and v, that is, γ, T y v. We refer to such a
triple as a consistent triple. We consider trace or provenance queries built out of partial values and partial traces.
22

tp=pt

=

p

♦tp=pt♦

=

p[♦/]

(p01 , p02 )

=

(p1 t p01 , p2 t p02 )

ctc

=

c

inl(p) t inl(p0 )

=

inl(p t p0 )

0

=

inr(p t p0 )

0

roll(p) t roll(p )

=

roll(p t p0 )

hκ, ρi t hκ, ρ0 i

=

hκ, ρ t ρ0 i

0
 ρ(x) t ρ (x)
ρ(x)
 0
ρ (x)

(p1 , p2 ) t

inr(p) t inr(p )

0

(ρ t ρ )(x)

=

x ∈ dom(ρ) ∪ dom(ρ0 )
x ∈ dom(ρ)\dom(ρ0 )
x ∈ dom(ρ0 )\dom(ρ)

Figure 18: Least upper bounds of patterns and environments.
Definition 5.5.
1. Let φ(γ) be a predicate on input environments. An input query INγ.φ(γ) is defined as {(γ, T, v) |
γ, T y v and φ(γ)}. (Here, IN binds x in φ(x).) As a special case, we write INρ for INγ.(ρ v γ).
2. Let φ(v) be a predicate on output values. An output query OUTv.φ(v) is defined as {(γ, T, v) | γ, T y
v and φ(v)}. (Here, OUT binds x in φ(x).) As a special case, we write OUTp for OUTv.(p v v).
Remark 5.6. The INγ.φ(γ) and OUTv.φ(v) notations are chosen to resemble quantifiers; they should be read as “In
the input of the trace, φ holds” or “In the output of the trace, φ holds”. One can also think of them as higher-order
functions, for example IN : (Env → B) → T → B and OUT : (Val → B) → T → B, and regard INγ.φ(γ) and
OUTv.φ(v) respectively as syntactic sugar for IN(Λγ.φ(γ) and OUT(Λv.φ(v)).
To analyze forms of provenance based on annotation (as considered in Section 4) we will also consider consistent
annotated triples (b
γ , T, vb) where vb = F(T, γ
b). We will later also consider corresponding queries derived from different
forms of provenance, based on annotated triples.

5.2

Disclosure

We first consider properties disclosed by various forms of provenance considered above. Both where-provenance and
expression provenance disclose useful information about the input. Dependency provenance does not disclose input
information in an easy-to-analyze way, but is useful for obfuscation, as discussed in Section 5.3.
For where-provenance, we consider input queries
INW
v0 ,π = INγ. (γ[π] = v0 ))
and output queries
π
OUTW
v ) ∧ |w| = v0 )
v0 ,π = OUTv̂. (w ∈ occ(b

where π is a path and v0 is a value. Such a query tests whether γ or v contains a value v0 with the provided annotation.
W
Theorem 5.7. The where-provenance view (γ, T, v) 7→ W(T, path(γ)) positively discloses INW
v0 ,π via OUTv0 ,π .

Proof. If OUTW
v0 ,π holds of W(T, path(γ)) then by Theorem 4.5 we know that γ contains a copy of v0 annotated by
W
π, hence INv0 ,π holds of path(γ).
For expression-provenance, suppose t is an expression over paths (that is, locations ` in t are paths π). We define
γ(t) to be the result of evaluating t in γ with all paths π replaced by their values γ[π] in γ. This is defined as follows:
γ(x.π)
γ(c)
γ(⊕(t1 , . . . , tn ))
γ(⊥)

= γ(x)[π]
= c
ˆ
= ⊕(γ(t
1 ), . . . , γ(tn ))
= ⊥
23

We consider queries INEv0 ,t = INγ. (γ(t) = v0 ), where t is an expression provenance annotation and v0 is a
value. Such a query tests whether evaluating an expression t over γ yields the specified value. For example,
INγ. x.1 + y.2 = 4 holds for γ = [x = (1, 2), y = (2, 3)], because γ(x.1) + γ(y.2) = 1 + 3 = 4. We also
consider output queries OUTEv0 ,t = OUTb
v . (wt ∈ occ(b
v ) ∧ |w| = v0 ), that simply test whether an annotated copy of
v0 appears in the output with annotation t.
Theorem 5.8. The expression-provenance view (γ, T, v) 7→ E(T, path(γ)) positively discloses INEv0 ,t via OUTEv0 ,t .
Proof. Similarly to where-provenance, using Theorem 4.9 we show that if OUTEv0 ,t holds on E(T, γ) then γ(t) = v0 ,
which implies INEv0 ,t .
For example, if the annotated output is 42x+y , then we know that the annotated value is equal to the sum of γ(x)
and γ(y), but we do not know anything more about the values of x and y beyond the equation x + y = 42. However,
if the output is (42x+y , 17x−y ) then we know that x and y are the (unique) solution to the linear equations
x+y

=

42

x−y

=

17 ,

that is, x = 29.5, y = 12.5.
Expression provenance and where-provenance are also related in the following sense:
Theorem 5.9. Where-provenance is computable from expression-provenance.
Proof. Where-provenance annotations can be extracted from expression-provenance annotations by mapping locations
` to themselves and all other expressions to ⊥.
Hence, any query disclosed by where-provenance is disclosed by expression-provenance, and any query obfuscated
by expression-provenance is also obfuscated by where-provenance.
We now consider a form of trace slicing that takes a partial output value and removes information from the input
and trace that is not needed to disclose part of the output. We show that such disclosure slices also disclose generic
provenance views (Theorem 5.20). Thus, disclosure slices form a quite general form of provenance in their own right.
Definition 5.10. Let γ, T y v, and suppose S v T and ρ v γ. We say (ρ, S) is a disclosure slice with respect to
partial value p if for all γ 0 w ρ and T 0 w S such that if γ 0 , T 0 y v 0 , we have p v v iff p v v 0 .
The intuition is that a disclosure slice should contain enough information that any replay of a (completed) trace on
a (completed) input environment (both extending the respective components of the slice) yields a result that matches
p; in other words, the slice is a (possibly smaller) “witness” to the construction of p from the input. Note that by this
definition, minimal disclosure slices exist (since there are finitely many slices) but need not be unique. For example,
both  ∨ true and true ∨  are disclosure slices showing that true ∨ true evaluates to true, but  ∨  is not a
disclosure slice.
disc
Figure 19 shows rules defining a disclosure slicing judgment p, T −→ S, ρ. Basically, the idea is to push a partial
value backwards through a trace to obtain a partial input environment and trace slice. The partial input environment is
needed to handle local variables in traces. In the rule for let, we first slice through the body of the let, then identify
the partial value showing the needed parts of the let-bound value, and use that to slice backwards through the first
subtrace.
Example 5.11. To illustrate the behavior of let and bound variables, consider:
disc

(, 1), x −→ x, [x 7→ (, 1)]
disc

1, snd(x) −→ snd(x), [x 7→ (, 1)]

disc

, fst(x) −→ , []

disc

(1, ), (snd(x), fst(x)) −→ (snd(x), ), [x 7→ (, 1)]
disc

disc

, y −→ , []

disc

1, z −→ z, [z 7→ 1]
disc

(, 1), (y, z) −→ (, z), [z 7→ 1]

(1, ), let x = (y, z) in (snd(x), fst(x)) −→ let x = (, z) in (snd(x), ), [z 7→ 1]
24

disc

p, T −→ S, ρ
disc

disc

, T −→ , []

disc

p, x −→ x, [x 7→ p]
disc

disc

♦, T1 −→ S1 , ρ1

disc

disc

p, ⊕(T1 , . . . , Tn ) −→ ⊕(S1 , . . . , Sn ), ρ1 t · · · t ρn

disc

disc

p2 , T2 −→ S2 , ρ2
disc

(p1 , p2 ), (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2
disc

disc

(p, ), T −→ S, ρ

(, p), T −→ S, ρ

disc

p, snd(T ) −→ snd(S), ρ

disc

p, fst(T ) −→ fst(S), ρ
disc

p, T −→ S, ρ

disc

p, T −→ S, ρ

disc

p, T −→ S, ρ

disc

inl(p), inl(T ) −→ inl(S), ρ

disc

inr(p), inr(T ) −→ inr(S), ρ

roll(p), roll(T ) −→ roll(S), ρ

disc

disc

disc

p1 , T1 −→ S1 , ρ1 [x1 7→ p]

roll(p), T −→ S, ρ
disc

disc

♦, Tn −→ Sn , ρn

···

disc

p2 , let x = T1 in T2 −→ let x = S1 in S2 , ρ1 t ρ2
p1 , T1 −→ S1 , ρ1

hκ, ρi, fun κ −→ fun κ, ρ
disc

p1 , T1 −→ S1 , ρ1

p2 , T2 −→ S2 , ρ2 [x 7→ p1 ]

disc

c, c −→ c, []

inl(p), T −→ S, ρ

disc

p, unroll(T ) −→ unroll(S), ρ

p1 , case T .inl x1 .T1 −→ case S .inl x1 .S1 , ρ t ρ1

disc

p2 , T2 −→ S2 , ρ2 [x2 7→ p]

disc

inr(p), T −→ S, ρ

disc

p2 , case T .inr x2 .T2 −→ case S .inr x2 .S2 , ρ t ρ2
disc

p, T −→ S, ρ[f 7→ p1 , x 7→ p2 ]

disc

disc

p1 t hκ, ρi, T1 −→ S1 , ρ1

p2 , T2 −→ S2 , ρ2

disc

p, (T1 T2 ) .κ f (x).T −→ (S1 S2 ) .κ f (x).S, ρ1 t ρ2
disc

f vs(κ) = {x1 , . . . , xn }

♦, T1 −→ S1 , ρ1

disc

disc

♦, fun κ −→ fun κ, [x1 7→ ♦, . . . , xn 7→ ♦]

disc

disc

♦, T −→ S, ρ

♦, T2 −→ S2 , ρ2

♦, (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2

disc

♦, inl(T ) −→ inl(S), ρ

disc

♦, T −→ S, ρ

disc

♦, T −→ S, ρ

disc

♦, roll(T ) −→ roll(S), ρ

disc

♦, inr(T ) −→ inr(S), ρ

Figure 19: Disclosure slicing.
Slicing for conditionals (case expressions) follows a similar pattern to let-binding. For example, consider a trace
case T .inl x1 .T1 indicating that case expression m was executed with argument computed by T , evaluating to some
value inl(v 0 ) and the trace of the body of the inl-branch was T1 . If we wish to slice this with respect to p, then we first
slice the trace of the taken branch T1 with respect to T , yielding trace slice S1 and pattern environment ρ1 [x1 7→ p].
Since we know that the result of T must been of the form inl(v 0 ), we slice T with respect to inl(p), yielding slice S
and pattern environment ρ. The final result is slice case S .inl x1 .S1 with pattern environment ρ t ρ1 .
Slicing for application traces is similar to slicing for let and case constructs, but more complex due to the need to
propagate partial values backwards through closure environments. Specifically, a trace of the form (T1 T2 ) .κ f (x).T
is sliced with respect to output pattern p as follows. First, T is sliced with respect to p, yielding slice S and partial
environment ρ[f 7→ p1 , x 7→ v2 ]. Here, ρ is the part of the closure needed to rerun the body of the function call. We
then slice T1 , the subtrace that computed the called function, with respect to p1 t hκ, ρi, since we know from the trace
that κ was the called function and we know that the parts of the environment denoted ρ were needed in the call, and
we also know that p1 was needed to apply recursive calls of f . (In particular, if f was not called recursively in T , then
p1 = .) This yields a slice S1 and pattern environment ρ1 . We also slice T2 with respect to p2 , obtaining a slice
S2 and pattern environment ρ2 that show what part of the trace and input environment were needed to compute the
function argument. The final result is slice (S1 S2 ) .κ f (x).S with pattern environment ρ1 t ρ2 ; any dependence on
the environment in which the function closure was constructed is propagated to ρ1 via the slicing subderivation for T1 .
Note also that the special ♦ patterns are used to slice backwards through primitive operations even when we do
not know the values of the inputs or results. This necessitates additional rules that deal with the cases where p is ♦.
Another possibility is to annotate the traces of primitive operations with these values, an approach taken on related

25

Witness(p, v)

=



Witness(c , c)

=

c


Witness((p1 , p2 ), (v1 , v2 ))

=

Witness(p, (v1 , v2 ))

=

0

if p v v
(Witness(p1 , v1 ), ) if p1 v
6 v1
(, Witness(p2 , v2 )) if p1 v v1 and p2 6v v2

(, ) otherwise

Witness(inl(p), inl(v))

= inl(Witness(p, v))

Witness(p, inl(v))

= inl() otherwise

Witness(inr(p), inr(v))

= inr(Witness(p, v))

Witness(p, inr(v))

= inr() otherwise

Witness(roll(p), roll(v))
Witness(p, roll(v))
Witness(hκ, ρi, hκ, γi)

= roll(Witness(p, v))
= roll() otherwise
=

hκ, [x1 7→ Witness(ρ(x1 ), γ(x1 )), . . . , xn 7→ Witness(ρ(xn ), γ(xn ))]i
where dom(ρ) = dom(γ) = {x1 , . . . , xn }

Witness(, hκ, γi)

=

hκ, []i otherwise
Figure 20: Witness function

work on using traces for program slicing [40]; however, this approach does not work as well in this setting since our
disclosure slicing criterion involves replaying the trace on changed inputs.
disc

Lemma 5.12. If γ, T y v then for any p v v there exists S v T and ρ v γ such that p, T −→ S, ρ.
Proof. The first part follows by induction on the structure of the derivation of γ, T y v. If p =  then the conclusion
is immediate in any case. For each constructor case (pairs, inl, inr, fun, roll), if p is not  then its toplevel
constructor must match, so we can proceed by induction. The other cases, for primitive operations, pair projection,
cases, function application, and unroll, are straightforward because there is no restriction on p (though we need to
check that the invariant p v v holds for the induction hypotheses).
We define a function Discp (γ, T, v) on consistent triples (γ, T, v) as follows.
(
disc
(γ|ρ , S) if p v v and p, T −→ S, ρ
Discp (γ, T, v) =
disc
(γ|ρ , S) if p 6v v and Witness(p, v), T −→ S, ρ
The idea is that when p v v, we slice using the rules in Figure 19 and then transform ρ by filling in all ♦-holes with
the corresponding values in γ. However, when p 6v v, we do not use p to slice, but instead use Witness(p, v), a pattern
that contains enough of v to show how v fails to match p. The Witness function is defined in Figure 20.
Example 5.13. Recall the running example map f xs where
γ = [f 7→ fun f (x).if x = y then y else x + 1, xs = [1, 2, 3], y = 2]
and yielding result v = [2, 2, 4]. We write a :: l for the list construction operator, that is, [2, 2, 4] = 2 :: 2 :: 4 :: []. Let
T be the trace obtained by running this example, i.e. γ, map f xs ⇓ [2, 2, 4], T .
• If p = [, , ] then Discp (γ, T ) = ([f 7→ , xs 7→ [, , ], y 7→ ], S) where S shows three recursive
calls to map, each with a partial trace of f .
• If p = [] then Discp (γ, T ) = ([xs 7→  :: ], S) where S shows one recursive call to map f xs in which
xs is inspected and found to be of the form v :: vs, the corresponding branch is taken and a nonempty list is
constructed.
26

• If p = [2, , ] then Discp (γ, T ) = ([f 7→ fun f (x).if x = y then y else x + 1, y 7→ 2], S) where S lists all
three calls to map f xs, two partial calls to f and one complete call to f on 1.
• If p = [, 3, ] then Discp (γ, T ) = ([f 7→ fun f (x).if x = y then y else x + 1, xsmapsto :: 2 :: , y 7→
2], S) where S lists two calls to map, one partial call to f and one complete call to f on 2.
Correctness of disclosure slicing. We now establish the key properties of disclosure slicing, culminating in the main
result that Discp discloses the output query OUTp (Theorem 5.19).
Lemma 5.14. If p 6v v then p 6v Witness(p, v); moreover, for any v 0 w Witness(p, v) we have p 6v v 0 .
Proof. The first part follows by induction on the structure of v, with secondary case analysis on the possible forms of
p. The second part is immediate.
The witness function can be replaced by any other function that has this property (for example, we could alter
Witness to find a minimum-size pattern witnessing p 6v v.)
Recall the definition of v hp v 0 as shown in Figure 17. Using this relation, we can prove the correctness of the
slicing relation as follows:
disc

Lemma 5.15. Assume γ, T y v and p, T −→ S, ρ where p v v. Then for all γ 0 hρ γ and T 0 w S, if γ 0 , T 0 y v 0
then v 0 hp v.
Proof. See Appendix A.5.
Correctness follows as a consequence of the above property. To simplify the argument, we prove positive and
negative disclosure simultaneously using an auxiliary query on the provenance view. Specifically, we define a function
on sliced traces and environments called Replay that, intuitively, computes a plausible output for the slice. Given slice
(ρ, S), we define the auxiliary function Replay as follows:
Replay(ρ, S) = choose({v 0 | ∃γ 0 w ρ, T 0 w S. γ 0 , T 0 y v 0 })
In other words, Replay(ρ, S) chooses one of the possible values obtainable by replaying a complete trace extending
S on a complete environment extending ρ, if such a value exists; otherwise, the result is arbitrary. Here, choose :
P(Val) → Val is a choice function such that if X ⊆ Val and X 6= ∅ then choose(X) ∈ X. If X = ∅, then
choose(X) is an arbitrary value, say 42.
Remark 5.16. Observe that this is not a constructive definition. We can use the Axiom of Choice to define choose,
or define a linear ordering on values to avoid appealing to the Axiom of Choice; however, it is not obvious whether
Replay itself is computable. In any case, Replay is only needed as a technical device to help define the intermediate
provenance query used to prove positive and negative disclosure; we never need to try to compute it directly.
Lemma 5.17. Discp negatively discloses OUTp via OUTp ◦ Replay.
Proof. We prove the contrapositive. Suppose OUTp (γ, T, v) holds, that is, p v v. Then let (ρ, S) = Discp (γ, T, v) be
disc

the computed slice, where p, T −→ S, ρ, and suppose v 0 = Replay(ρ, S), where T 0 w S and γ 0 w ρ are the complete
trace and environment used by Replay to compute γ 0 , T 0 y v 0 . Thus, we have ρ v γ and ρ v γ 0 , which together with
the fact that ρ is ♦-free (by definition of Disc) implies γ hρ γ 0 . By Lemma 5.15 and Lemma 5.1 this implies v hp v 0
so p v v 0 .
Lemma 5.18. Discp positively discloses OUTp via OUTp ◦ Replay.
Proof. We prove the contrapositive. Suppose that OUTp (γ, T, v) fails, that is, p 6v v. We need to show that
disc

OUTp (Replay(Discp (γ, T, v))) also fails. Since p 6v v, we know that Discp (γ, T, v) = (ρ, S) where Witness(p, v), T −→
S, ρ. Thus, Replay(ρ, S) = v 0 for some v 0 obtained by replaying T 0 w S and γ 0 w ρ, that is, γ 0 , T 0 y v 0 . Since
ρ v γ and ρ is ♦-free we have that γ hρ γ 0 . So, by Lemma 5.15, we know that v hWitness(p,v) v 0 holds, which
implies Witness(p, v) v v 0 , and by Lemma 5.14 this implies p 6v v 0 . This is what we need to show to conclude
OUTp (Replay(Discp (γ, T, v))) = 0.
27

Then by Proposition 2.8 and the previous two lemmas we have:
Theorem 5.19. Discp discloses OUTp .
This is the main result about disclosure; we previously established some disclosure results for more restricted
computational models [15], but this is the first such result for a general-purpose language. It means that the disclosure
slicing algorithm can be used to identify a subset of the trace that is large enough to recompute a part of the output,
provided the parts of the input specified by ρ remain fixed. As noted elsewhere, this may not be a minimal slice, but
it can be much smaller than the original trace. In particular, let (x, e) be a program where e is an arbitrarily complex
expression, evaluated in a context with x bound to 42. If all we care about is the first component of the result then the
slice with respect to (♦, ) is ([x 7→ 42], (x, )), which can be arbitrarily smaller than the full trace.
This does not mean that there is no room for improvement in the disclosure slicing algorithm, for example by
taking advantage of program analyses that can identify dead code or subprograms whose values are constant: this
information can be used to further shrink the trace. Further investigation is needed to experiment with the syntactic
disclosure slicing algorithm on realistic examples and identify areas for improvement.
Disclosure from slices. Finally, we link disclosure for value patterns to disclosure for generic provenance views.
Essentially, we show that for any F, the disclosure slice for p positively discloses the F-provenance annotations of
values matching p. Informally, this means that disclosure slices provide a highly general form of provenance specialized to a part of the output: one can compute and reveal the disclosure slice and others can then compute any generic
provenance view from the slice, without rerunning the original computation or consulting input data or subtraces that
are dropped in the slice.
To state the desired property, we need to lift h− to apply to annotated values. The definition is similar to that for
unannotated values, with additional rules:
v hp w
v a hp w a

v a h wb

v a h♦ v a
disc

Theorem 5.20. Assume |b
γ |, T y v and p v v. Suppose p, T −→ S, ρ. Suppose that F is a generic extraction
function. Then the annotations associated with p in F(T, γ
b) can be correctly extracted from S using only input parts
needed by ρ. That is, suppose we have γ
b hρ γ
b0 and T 0 w S, where |b
γ 0 |, T 0 y v 0 . Then we have F(T, γ
b) hp F(T 0 , γ
b0 ).
disc

Proof. Straightforward induction on the structure of derivations of p, T −→ S, ρ. See Appendix A.6.
Observe that some minimal slices discard information needed for provenance extraction. For example, given
expression ∨(x, true), the minimal slice with respect to true is (, true). However, this slice makes it impossible
for dependency or expression provenance extraction to produce the right answer, since in both cases the annotation
on x is needed. Moreover, if we ignore code and match pointers, our slicing algorithm appears to be minimal with
respect to provenance extraction (that is, removing any more from a trace would produce slices that do not satisfy
Theorem 5.20). This supports our view that the trace slicing algorithm is a natural one for the purpose of generating
provenance or explanations, despite its non-minimality with respect to the semantic replayability criterion.
An alternative approach to slicing based on a criterion for which minimal slices exist is explored in another recent
paper [40]. Intuitively, the difference arises because disclosure slices are defined in terms of a fixed semantics, whereas
Perera et al. [40] define a correct backward slice as one that contains enough information to recompute a given part of
the output using an ad hoc replay semantics defined over expressions with holes. This makes a nice theory but means
that we are required to include information in the slice that is not required in a disclosure slice.
Note that it is typical for a notion oftypical for a notion of witness to lack unique minimal solutions (e.g. whyprovenance in databases is defined as the set of minimal witnesses to a query result [11]) and for minimal slices to be
non-computable. For example, in the original work on slicing by Weiser [49] minimal slices are shown to exist but
are not computable. Similarly, since TML is Turing-complete, it is easy to show that it is undecidable to determine
whether a given partial trace is a (minimal) disclosure slice.

28

5.3

Obfuscation

We now consider obfuscating properties of the input. We first consider what can be obfuscated by the standard
provenance views. Where-provenance, essentially, obfuscates anything that can never be copied to the output or affect
the control flow of something that is copied to the output. Similarly, expression provenance obfuscates any part of the
input that never participates in or influences expression annotations. In both cases, we can potentially learn about parts
of the input that affected control flow, however. For example, if x = 1 then 1 else y does not obfuscate the value
of x in either model, provided y comes from the input, since we can inspect the annotation of the result to determine
that x = 1 or x 6= 1.
This illustrates a possibly counterintuitive fact: obfuscation of the query that tests whether x = 1 fails if we can
ever learn anything about the result of the query, even if we cannot determine the exact value of x. Thus, whereprovenance and expression-provenance do not provide particularly strong obfuscation properties, since they do not
take control-flow into account. Given that we want to ensure obfuscation, we consider conservative techniques that
accept (or construct) only provenance views that successfully obfuscate, but may reject some views or construct views
that are unnecessarily opaque.
There are several ways to erase information from traces (or other provenance views) to ensure obfuscation of input
properties. One way is to re-use the static analysis of dependency provenance (in [17], for example) to identify and
elide parts of the output that suffice to make it impossible to guess sensitive parts of the input. Alternatively we can
use dynamic dependency provenance to increase precision, by propagating dependency tracking information from the
input to the output.
This is similar to using static analysis or dynamic labels for information flow security; the difference is one of
emphasis. In information flow security, we usually identify high- or low-security locations and try to certify that highsecurity data does not affect the computation of low-security data; here, instead, we identify a high-security property of
the trace (e.g. that the input satisfies a certain formula) and try to determine what parts of the output do not depend on
sensitive inputs, and hence can be safely included in the provenance view. However, these techniques do not provide
guidance about what parts of the trace can be safely included in the provenance view.
Here, we develop an alternative approach based on directly analyzing and slicing traces. Consider a pattern ρ v γ,
in which the parts of γ that are considered confidential have been replaced by . We construct an obfuscation slice by
re-evaluating T on ρ as much as possible, to compute a sliced trace S and partial value p. We erase parts of T and of
the original output value that depend on the erased parts of ρ. Thus, any part of the trace or output value that remains
in the obfuscation slice is irrelevant to the sensitive part of the input, and cannot be used to guess it.
Figure 21 shows a syntactic algorithm for computing obfuscation slices as described above, defined via a judgment
obf
ρ, T −→ p, S, which takes a partial input environment ρ and trace T as input and computes a partial output p and
sliced trace S. Many rules are essentially generalizations of the rules for evaluation to allow for partial inputs, outputs
and traces. The rules of interest, near the bottom of the figure, show how to handle attempts to compute that encounter
holes in places where a value constructor is expected. When this happens, we essentially propagate the hole result and
return a hole trace. This may be unnecessarily draconian for some cases, but is necessary for the case and application
traces where the trace form gives clues about the control flow.
obf

Example 5.21. To illustrate the behavior of −→, consider again a simple program that swaps the elements of a pair:
obf

obf

obf

[z 7→ 1], y −→ , 

[z 7→ 1], z −→ 1, z
obf

[z 7→ 1], (y, z) −→ (, 1), (, z)

obf

γ, x −→ (, 1), x

γ, x −→ (, 1), x

obf

γ, fst(x) −→ , fst(x)

γ, snd(x) −→ 1, snd(x)

obf

obf

γ, (snd(x), fst(x)) −→ (1, ), (snd(x), fst(x))
obf

[z 7→ 1], let x = (y, z) in (snd(x), fst(x)) −→ (1, ), let x = (, z) in (snd(x), fst(x))

where γ = [z 7→ 1, x 7→ (, 1)]. Notice that it is impossible to guess the value of y used in the original run from the
slice let x = (, z) in (snd(x), fst(x)) or partial result (1, ).
Correctness of obfuscation slicing. We now show the correctness of obfuscation slicing in the sense that the slicing
algorithm supports positive obfuscation.

29

obf

ρ, T −→ p, S
obf

obf

ρ, T1 −→ p1 , S1
obf

obf

ρ, x −→ ρ(x), x

obf

ρ, T1 −→ v1 , S1

obf

obf

ρ, c −→ c, c

ρ, let x = T1 in T2 −→ p2 , let x = S1 in S2

ρ, fun κ −→ hκ, ρi, fun κ

···

obf

ρ, T2 −→ p2 , S2

ρ, T1 −→ p1 , S1

obf

obf

ρ, ⊕(T1 , . . . , Tn ) −→ ⊕(v1 , . . . , vn ), ⊕(S1 , . . . , Sn )

ρ, (T1 , T2 ) −→ (p1 , p2 ), (S1 , S2 )

obf

obf

ρ, T −→ (p1 , p2 ), S

ρ, T −→ (p1 , p2 ), S

ρ, T −→ p, S

obf

ρ, snd(T ) −→ p2 , snd(S)

obf

ρ, inl(T ) −→ inl(p), inl(S)

ρ, fst(T ) −→ p1 , fst(S)
obf

obf

obf

ρ, case T .inl x1 .T1 −→ p1 , case S .inl x1 .S1
obf

ρ, T −→ inr(p), S

obf

ρ[x2 7→ p], T2 −→ p2 , S2

ρ, T −→ p, S

obf

obf

ρ, case T .inr x2 .T2 −→ p2 , case S .inr x2 .S2
obf

obf

ρ, T −→ roll(p), S
obf

(for some i ∈ 1, . . . , n)

ρ, roll(T ) −→ roll(p), roll(S)
obf

ρ, T1 −→ hκ, ρ0 i, S1

obf

obf

ρ, T −→ , S

ρ, T −→ , S

ρ, T −→ , S

obf

ρ, case T .inl x1 .T1 −→ , 

obf

ρ, T −→ , S

ρ, fst(T ) −→ , 

obf

ρ0 [f 7→ hκ, ρ0 i, x 7→ p2 ], T −→ p, S

ρ, (T1 T2 ) .κ f (x).T −→ p, (S1 S2 ) .κ f (x).S

obf

ρ, ⊕(T1 , . . . , Tn ) −→ , 

obf

ρ, T2 −→ p2 , S2
obf

ρ, unroll(T ) −→ p, unroll(S)
ρ, Ti −→ , Si

obf

ρ[x1 7→ p], T1 −→ p1 , S1

ρ, T −→ inl(p), S

ρ, inr(T ) −→ inr(p), inr(S)
obf

obf

obf

ρ, T −→ p, S

obf

obf

obf

ρ, Tn −→ vn , Sn

obf

ρ[x 7→ p1 ], T2 −→ p2 , S2

obf

obf

ρ, T −→ , S

ρ, snd(T ) −→ , 

obf

obf

ρ, case T .inr x1 .T1 −→ , 

obf

ρ, unroll(T ) −→ , 
obf

ρ, T1 −→ , S1
obf

ρ, (T1 T2 ) .κ f (x).T −→ , 

Figure 21: Obfuscation slicing.
obf

Lemma 5.22. If γ, T y v and ρ v γ is ♦-free then there exist unique p v v and S v T such that ρ, T −→ p, S.
obf

Proof. First, we show that if γ, T y v and ρ v γ is ♦-free then there exists p v v and S v T such that ρ, T −→ p, S.
obf
Uniqueness is straightforward by induction over derivations of ρ, T −→ p, S.
obf

Accordingly, we define a partial function Obf ρ (γ, T, v) as (p, S) where ρ, T −→ p, S and p v v. We can show
that this function is total for well-formed, partial traces and ♦-free input environments.
Example 5.23. Consider again the running map f xs example, with γ, T, v as in Example 5.21.
• If ρ = [f 7→ fun f (x).if x = y then y else x + 1, xs = [1, 2, 3], y = ] then Obf ρ (γ, T, v) = ([, , ], S)
where S shows three recursive calls to map f and three partial calls to f where the parts of the trace showing
the results of the conditional tests x = y in f are deleted.
• If ρ = [f 7→ , xs = [1, 2, 3], y = 2] then Obf ρ (γ, T, v) = ([, , ], S) where S shows three recursive calls
to map f where the traces showing the execution of f are deleted.
• If ρ = [f 7→ fun f (x).if x = y then y else x + 1, xs =  :: ], y = 2] then Obf ρ (γ, T, v) = ( :: , S)
where S shows two recursive calls to map f and one call to f , where information about the control flow branch
taken after testing x = y is omitted.
obf

obf

Lemma 5.24. If γ, e ⇓ v, T and ρ v γ and ρ, T −→ p, S then for all γ 0 w ρ, if γ 0 , e ⇓ v 0 , T 0 then ρ, T 0 −→ p, S
and p v v 0 .
Proof. See Appendix A.7.
30

Finally, before considering the main correctness result for Obf ρ , we note a technical issue: In our language, every
base type happens to have at least two values, so we can always instantiate a hole at base type in at least two ways.
Similarly, pairs, functions and so on involving base types can always be instantiated in several ways. However, in
general we cannot assume that every type has more than one ground value. We say that a type is nonsingular if it has
at least two different values, and in the following result we restrict attention to patterns containing holes of nonsingular
types:
Theorem 5.25. For traces generated by terminating expressions, and ρ with holes of nonsingular types, and ρ0 A ρ,
we have Obf ρ positively obfuscates INρ0 .
Proof. Suppose INρ0 holds of (γ, T, v) where ρ0 A ρ. Then ρ @ ρ0 v γ. Moreover, since the inclusion is strict,
and since ρ contains holes of nonsingular type, ρ must contain holes that can be replaced with different values, so
there exists another γ 0 w ρ that differs from ρ0 . Since T was generated by a terminating expression, we know that
obf
γ 0 , e ⇓ v 0 , T 0 can be derived for some v 0 , T 0 . By Lemma 5.24 we know that ρ, T 0 −→ p, S, hence Obf ρ (γ 0 , T 0 , v 0 ) =
(p, S) = Obf ρ (γ, T, v), as required.
This is the main result about obfuscation. As with disclosure, previously some properties of obfuscation were
established for limited computational models [15], but this is the first such result to be established for a generalpurpose programming language. This result shows that the obfuscation slicing algorithm (a syntactic traversal of the
trace that propagates “holes” forward) provides a safe approach to positive obfuscation. This means that given a pattern
ρ0 identifying a sensitive part of the input, for any triple (γ, T, v), the syntactic algorithm yields a subtrace (p, S) such
that there exists (γ 0 , T 0 , v 0 ) whose obfuscation slice is also (p, S) but such that γ 0 does not contain ρ. Thus, we cannot
deduce that ρ0 is present in γ 0 from (p, S).
Negative obfuscation may also hold for the obfuscation slicing algorithm, but if so it appears more difficult to
prove: we would have to show that if ρ does not match the input γ, then there is another γ 0 that does match ρ but
produces the same obfuscation slice as ρ. Calculating such a γ 0 is not straightforward if the expression e can diverge,
because even finding a different input on which e terminates is generally an undecidable problem. However, even
under an assumption of termination, it is not clear how to compute obfuscation slices to ensure that all traces on inputs
that avoid a certain pattern are indistinguishable from traces on inputs that do contain the pattern.

5.4

Discussion

The analysis in section 5.1 gives novel characterizations of what information is disclosed by where-provenance and
expression provenance. Essentially, where-provenance discloses information about what parts of the input are copied
to the output, while expression provenance additionally discloses information about how parts of the input can be
combined to compute parts of the output. Both forms ignore the control flow of the program. The analysis in section
5.1 also shows (in a formal sense) that where-provenance and expression provenance are closely related: one can
obtain where-provenance from expressions simply by erasure. Moreover, we can obtain a number of other intermediate
provenance models, by extracting information compositionally from expression-provenance annotations.
The disclosure slicing algorithm is based on an interesting insight (which we are exploring in concurrent work on
slicing [40]): at a technical level, the information we need for program comprehension via slicing (to understand how
a program has evaluated its inputs to produce outputs) is quite similar to what we need for provenance. Our past work
on dependency provenance identified connections between provenance and slicing [17] which we have explored in
more recent work [40] that employs slicing techniques similar to disclosure slicing.
Obfuscation seems to be fundamentally more difficult to obtain than disclosure. From an intuitive point of view,
this is not surprising; however, it is interesting to see where the complications arise at a technical level, and how these
interact with conventional forms of provenance. For example, both where- and expression provenance effectively
disclose certain information about the output given the input (or vice versa), while dependency provenance does
not appear to disclose information in a particularly direct way. On the other hand, since it was inspired in part by
information flow security techniques, dependency provenance does seem to obfuscate information about the input, but
cannot directly tell us how much of the trace it is safe to provide while still obfuscating a part of the input.
Obfuscation slicing, which is based on a similar idea to dependency provenance, does allow us to provide part of
the trace in the provenance view while obfuscating sensitive input. However, we were only able to obtain a positive
31

obfuscation result for slicing. We do not currently have either a proof of negative obfuscation or a counterexample to it
for the obfuscation slicing algorithm. This means that whenever the query actually holds, we cannot be certain of this
from the provenance view; however, when the input query fails it may be possible to tell this from the view. Negative
obfuscation seems more difficult to prove than positive obfuscation, at least for the input queries we considered. This
is unsurprising, since as also found in [15], the definition of obfuscation is more complex.
It is interesting to consider whether alternative definitions of disclosure or obfuscation could lead to more satisfying
results. As explained at the end of Section 5.3, the root of the difficulty with negative obfuscation seems to be the
difficulty of analyzing the program to find alternative inputs that enable the program to complete and lead to the same
obfuscation slice.
One alternative could be to model the knowledge of the attacker about the possible traces more explicitly (e.g.
assume the attacker knows the original program). This seems orthogonal to the problem of proving negative obfuscation: it should complicate both positive and negative problems. Another alternative could be to adopt a probabilistic or
information-theoretic definition of obfuscation that makes it easier to provide both positive and negative obfuscation.
These are possibilities for future work.

6

Related Work

There is a huge, and growing, literature on provenance [8, 18, 44, 38], but there is little work on formal models
of provenance and no previous work on provenance in a general-purpose higher-order language. Since we already
covered prior work on provenance security in the introduction, we confine our comparison to closely related work on
formal techniques for provenance, and on related ideas in programming languages and language-based security.
Provenance. This work differs from previous work on provenance in databases in several important ways. First,
we consider a general purpose, higher-order language, whereas previous work considers database query languages
of limited expressiveness (e.g., monotone query languages), which include unordered collection types with monadic
iteration operations but not sum types, recursive types or first-class functions. Second, we aim to record traces adequate
to answer a wide range of provenance queries in this general setting, whereas previous work has focused on particular
kinds of queries (e.g., where-provenance [11, 10], why-provenance [11], how-provenance [28, 27]).
Provenance has also been studied extensively for scientific workflow systems [8, 44, 22]. Many workflow provenance systems record additional information to support replaying the computation (analogous to our fidelity property)
or provenance queries focusing on explaining parts of the result (analogous to our extraction and slicing techniques).
Most work in this area describes the provenance tracking behavior of a system through examples and does not give
a formal semantics that could be used to prove correctness properties; furthermore, there has been little work (and
there is currently no consensus) on what the appropriate correctness properties are. An exception is Hidders et al. [33],
which is the closest workflow provenance work to ours. They model workflows using a core database query language
extended with nondeterministic, external function calls, and partially formalize a semantics of runs, or sets of triples
(γ, e, v) labeling an operational derivation tree. They also discuss extracting subruns which seem similar to slices,
and extracting provenance information from runs. However, their definitions of subrun and provenance extraction are
complex, incomplete, and not accompanied by precise statements or proofs of correctness properties. Further progress
on formalizing their approach has been made recently in a workshop paper by Acar et al. [5]; however, provenance
extraction and trace slicing are not addressed in [5].
Other related topics. Our trace model is partly inspired by previous work on self-adjusting computation [4], where
execution traces are used to efficiently recompute functional programs under arbitrary modifications to their inputs.
Previous work on self-adjusting computation has not investigated trace slicing techniques or a relationship between
traces and provenance. Unlike self-adjusting traces, our traces are intended as data that can be manipulated and queried
by users, with recomputation just one of many competing requirements. Provenance-like ideas have also appeared in
the context of alignment in bidirectional computation [7] and language-based techniques for audit [34, 48] More
recently, Dimoulas et al. identified an intriguing connection between provenance and notions of correctness for blame
assignment in contracts. They introduce semantic properties that, they suggest, may be related to provenance [25].

32

However, to our knowledge no formal relationships between provenance and self-adjusting computation, bidirectional
computation, or blame have been developed.
Finally, our model of execution traces for TML is closely related to that used in a recent publication [40]; however,
the technical contributions, slicing algorithms and the correctness criteria are different. In this paper, we consider
trace slicing algorithms that provide disclosure or obfuscation properties, while in [40] we consider trace and program
slicing techniques that satisfy a different consistency property, aimed at comparing different runs of a program for
debugging or program understanding. At a semantic level, the most important difference is that in this article our
definitions are in terms of a standard operational semantics over standard values, which partial and annotated values
need to respect; in the work on program slicing we consider a variant operational semantics over partial values (which is
similar in some respects to the obfuscation slicing algorithm). Perera et al. [40] make several additional contributions,
including algorithms for extracting program slices from trace slices and for constructing differential slices that can
highlight the exact location of a bug in the source program. Investigating the applicability of these ideas to provenance
or provenance security is future work.

7

Conclusions

While the importance of understanding provenance and its security characteristics has been widely documented, to date
there has been little work on formal modeling of either provenance or its security. In this article, we elaborate upon the
ideas introduced in previous work [15], by instantiating the formal framework proposed there with a general-purpose
functional programming language and a natural notion of execution traces. We showed how more conventional forms
of provenance can be extracted from such traces via a generic provenance extraction mechanism. Furthermore, we
studied the key notions of disclosure and obfuscation in this context. In the process we identified weaker positive and
negative variants of disclosure and obfuscation, based on the observation that the original definitions seem too strong
to be satisfied often in practice. Our main results include algorithms for disclosure slicing, which traverses a trace
backwards to retain information needed to certify how an output was produced, and obfuscation slicing, which reruns
a trace on partial input (excluding sensitive parts of the input), yielding a partial trace and partial output that excludes
all information that could help a principal learn sensitive data.
To summarize, our main contribution is the development of a general model of provenance in the form of a core
calculus that instruments runs of programs with detailed execution traces. We validated the design of this calculus
by showing that traces generalize other known forms of provenance and by studying their disclosure and obfuscation
properties. There are many possible avenues for future work, including:
• identifying richer languages for defining trace queries or provenance views
• developing and implementing practical algorithms for trace slicing, and relating these to program slicing [40]
• developing a more uniform approach to the different forms of replay, extraction, and slicing
• extending trace and provenance models to handle references, exceptions, input/output, concurrency, nondeterminism, communication, etc.
Acknowledgments Effort sponsored by the Air Force Office of Scientific Research, Air Force Material Command,
USAF, under grant number FA8655-13-1-3006. The U.S. Government and University of Edinburgh are authorized
to reproduce and distribute reprints for their purposes notwithstanding any copyright notation thereon. Cheney is
supported by a Royal Society University Research Fellowship, by the EU FP7 DIACHRON project, and EPSRC grant
EP/K020218/1. Parts of this research were done while Acar and Perera were at Max-Planck Institute for Software
Systems, Kaiserslautern, Germany, and while Perera was a PhD student at the University of Birmingham. Acar is
partially supported by an EU ERC grant (2012-StG 308246—DeepSea) and an NSF grant (CCF-1320563).

33

References
[1] M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In POPL, pages 147–160,
1999.
[2] U. A. Acar. Self-adjusting computation (an overview). In PEPM, pages 1–6, 2009.
[3] U. A. Acar, A. Ahmed, J. Cheney, and R. Perera. A core calculus for provenance. In P. Degano and J. D.
Guttman, editors, POST, volume 7215 of LNCS, pages 410–429. Springer-Verlag, 2012.
[4] U. A. Acar, G. E. Blelloch, and R. Harper. Adaptive functional programming. ACM Trans. Program. Lang. Syst.,
28(6):990–1034, 2006.
[5] U. A. Acar, P. Buneman, J. Cheney, N. Kwasnikowska, J. Van den Bussche, and S. Vansummeren.
A graph model of data and workflow provenance.
In TAPP, 2010.
Online informal proceedings:
http://www.usenix.org/event/tapp10.
[6] B. T. Blaustein, A. Chapman, L. Seligman, M. D. Allen, and A. Rosenthal. Surrogate parenthood: Protected and
informative graphs. PVLDB, 4(8):518–527, 2011.
[7] A. Bohannon, J. N. Foster, B. C. Pierce, A. Pilkiewicz, and A. Schmitt. Boomerang: resourceful lenses for string
data. In POPL, pages 407–419, New York, NY, USA, 2008. ACM.
[8] R. Bose and J. Frew. Lineage retrieval for scientific data processing: a survey. ACM Comput. Surv., 37(1):1–28,
2005.
[9] P. Buneman, J. Cheney, W.-C. Tan, and S. Vansummeren. Curated databases. In PODS, pages 1–12, 2008.
[10] P. Buneman, J. Cheney, and S. Vansummeren. On the expressiveness of implicit provenance in query and update
languages. ACM Transactions on Database Systems, 33(4):28, November 2008.
[11] P. Buneman, S. Khanna, and W. Tan. Why and where: A characterization of data provenance. In ICDT, number
1973 in LNCS, pages 316–330, 2001.
[12] S. Carey and G. Rogow. UAL shares fall as old story surfaces online. Wall Street Journal, September 2008.
http://online.wsj.com/article/SB122088673738010213.html.
[13] J. Cheney. Provenance, XML and the Scientific Web.
http://db.ucsd.edu/planx2009.

In PLAN-X, 2009.

Informal proceedings at:

[14] J. Cheney. Causality and the semantics of provenance. In Proceedings of the 2010 Workshop on Developments
in Computational Models, 2010.
[15] J. Cheney. A formal framework for provenance security. In CSF, pages 281–293. IEEE, 2011.
[16] J. Cheney, U. A. Acar, and A. Ahmed. Provenance traces. CoRR, abs/0812.0564, 2008.
[17] J. Cheney, A. Ahmed, and U. A. Acar. Provenance as dependency analysis. Mathematical Structures in Computer
Science, 21(6):1301–1337, 2011.
[18] J. Cheney, L. Chiticariu, and W. C. Tan. Provenance in databases: Why, how, and where. Foundations and Trends
in Databases, 1(4):379–474, 2009.
[19] J. Cheney, S. Chong, N. Foster, M. Seltzer, and S. Vansummeren. Provenance: A future history. In OOPSLA
Companion (Onward! 2009), pages 957–964, 2009.
[20] S. Chong. Towards semantics for provenance security. In Workshop on the Theory and Practice of Provenance,
2009. Informal online proceedings: http://www.usenix.org/events/tapp09/.

34

[21] A. Cirillo, R. Jagadeesan, C. Pitcher, and J. Riely. Tapido: Trust and authorization via provenance and integrity
in distributed objects. In ESOP, volume 4960 of LNCS, pages 208–223, 2008.
[22] S. B. Davidson and J. Freire. Provenance and scientific workflows: challenges and opportunities. In SIGMOD,
pages 1345–1350, New York, NY, USA, 2008.
[23] S. B. Davidson, S. Khanna, T. Milo, D. Panigrahi, and S. Roy. Provenance views for module privacy. In PODS,
pages 175–186, 2011.
[24] S. C. Dey, D. Zinn, and B. Ludäscher. ProPub: Towards a declarative approach for publishing customized,
policy-aware provenance. In SSDBM, pages 225–243, 2011.
[25] C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen. Correct blame for contracts: no more scapegoating.
In POPL, pages 215–226, New York, NY, USA, 2011. ACM.
[26] C. Dwork. A firm foundation for private data analysis. Commun. ACM, 54:86–95, January 2011.
[27] J. N. Foster, T. J. Green, and V. Tannen. Annotated XML: queries and provenance. In PODS, pages 271–280,
2008.
[28] T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In PODS, pages 31–40, 2007.
[29] N. Guts, C. Fournet, and F. Z. Nardelli. Reliable evidence: auditability by typing. In ESORICS, pages 168–183,
2009.
[30] J. Halpern and J. Pearl. Causes and explanations: A structural-model approach–part I: Causes. British J. Philos.
Sci., 56:843–887, 2005.
[31] J. Halpern and J. Pearl. Causes and explanations: A structural-model approach–part II: Explanations. British J.
Philos. Sci., 56:889–911, 2005.
[32] R. Hasan, R. Sion, and M. Winslett. Preventing history forgery with secure provenance. Trans. Storage, 5:12:1–
12:43, December 2009.
[33] J. Hidders, N. Kwasnikowska, J. Sroka, J. Tyszkiewicz, and J. Van den Bussche. A formal model of dataflow
repositories. In DILS, volume 4544 of LNCS, pages 105–121, 2007.
[34] L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. Aura: a programming
language for authorization and audit. In ICFP, pages 27–38, New York, NY, USA, 2008.
[35] Z. Liu, S. B. Davidson, and Y. Chen. Generating sound workflow views for correct provenance analysis. ACM
Trans. Database Syst., 36(1):6, 2011.
[36] J. Lyle and A. Martin. Trusted computing and provenance: better together. In Proceedings of the 2nd conference
on Theory and practice of provenance (TAPP 2010), Berkeley, CA, USA, 2010. USENIX Association.
[37] A. Martin, J. Lyle, and C. Namilkuo.
Provenance as a security control.
In TaPP. USENIX,
2012.
Online proceedings:
http://www.usenix.org/system/files/conference/tapp12/tapp12-final17.pdf.
[38] L. Moreau. The foundations for provenance on the web. Foundations and Trends in Web Science, 2(2–3), 2010.
[39] R. Perera. Interactive functional programming. PhD thesis, University of Birmingham, 2013.
[40] R. Perera, U. A. Acar, J. Cheney, and P. B. Levy. Functional programs that explain their work. In ICFP, pages
365–376. ACM, 2012.
[41] B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

35

[42] A. C. Revkin. Hacked e-mail is new fodder for climate dispute. New York Times, November 20 2009.
[43] S. Schneider. Formal analysis of a non-repudiation protocol. In Proceedings of the 11th IEEE workshop on
Computer Security Foundations, pages 54–65, Washington, DC, USA, 1998. IEEE Computer Society.
[44] Y. Simmhan, B. Plale, and D. Gannon. A survey of data provenance in e-science. SIGMOD Record, 34(3):31–36,
2005.
[45] N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with
value-dependent types. In ICFP, pages 266–278, 2011.
[46] N. Swamy, B. J. Corcoran, and M. Hicks. Fable: A language for enforcing user-defined security policies. In
IEEE Symposium on Security and Privacy, pages 369–383, 2008.
[47] S. Varghese. UK government gets bitten by Microsoft Word. Sydney Morning Herald, July 2003.
http://www.smh.com.au/articles/2003/07/02/1056825430340.html.
[48] J. A. Vaughan, L. Jia, K. Mazurak, and S. Zdancewic. Evidence-based audit. In CSF, pages 177–191, 2008.
[49] M. Weiser. Program slicing. In ICSE, pages 439–449, 1981.
[50] J. Zhang, A. Chapman, and K. Lefevre. Do you know where your data’s been? — tamper-evident database
provenance. In Proceedings of the 6th VLDB Workshop on Secure Data Management (SDM 2010), pages 17–32,
Berlin, Heidelberg, 2009. Springer-Verlag.

36

A

Proofs

A.1

Proof of Theorem 4.5

Proof of Theorem 4.5. We prove by induction on the structure of derivations that if |b
γ |, e ⇓ v, T , then occ 6⊥ (W(T, γ
b)) ⊆
6⊥
occ (b
γ ).
• Base cases involving constants and variables are trivial.
• Cases involving constructors (pairs, inl, inr, roll, closures) and primitive operations (⊕) are straightforward
since the newly-constructed value is annotated with ⊥.
• Cases involving pair projections (fst, snd) and unroll are straightforward, since the returned value is a subvalue of the value returned by a subexpression.
• For a derivation of the form:
inl(x1 ).e1 ∈ m
|b
γ |, e1 ⇓ inl(v), T
|b
γ |[x1 7→ v], e1 ⇓ v1 , T1
|b
γ |, case e of m ⇓ v1 , case T .inl x1 .T1
By induction, occ 6⊥ (W(T, γ
b)) ⊆ occ 6⊥ (b
γ ). Moreover, W(T, γ
b) = inl(b
v )a for some vb with |b
v | = v. So,
occ 6⊥ (b
v ) ⊆ W(T, γ
b) ⊆ occ 6⊥ (b
γ ). Also by induction, occ 6⊥ (W(T1 , γ
b[x1 7→ vb]) ⊆ occ 6⊥ (b
γ [x1 7→ vb]). Hence,
occ 6⊥ (W(case T .inl x1 .T1 , γ
b[x1 7→ vb]) = occ 6⊥ (W(T1 , γ
b[x1 7→ vb]) ⊆ occ 6⊥ (b
γ [x1 7→ vb]) = occ 6⊥ (b
γ )∪occ 6⊥ (b
v ) ⊆ occ 6⊥ (b
γ)
• The case for case where the right branch is taken is symmetric.
• For function application, if the derivation is of the form:
|b
γ |, e1 ⇓ hf (x).e, γ0 i, T1

|b
γ |, e2 ⇓ v2 , T2
γ0 [f 7→ hf (x).e, γ0 i, x 7→ v2 ], e ⇓ v, T
|b
γ |, (e1 e2 ) ⇓ v, (T1 T2 ) .f (x).e f (x).T

then by validity we know that W(T1 , γ
b) = hf (x).e, γ
b0 ia with |b
γ0 | = γ
b and W(T2 , γ
b) = vb2 with |b
v2 | = v2 . By
induction, we also know:
occ 6⊥ (hf (x).e, γ
b0 ia ) ⊆ occ 6⊥ (b
γ)

occ 6⊥ (b
v2 ) ⊆ occ 6⊥ (b
γ)

Hence,
γ0 [f 7→ hf (x).e, γ0 i, x 7→ v2 ] = |b
γ0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ]|
So the induction hypothesis applies to the third subderivation, yielding:
W(T, γ
b0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ]) ⊆ occ 6⊥ (b
γ0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ])
Thus, by the definition of W for application-traces, we have:
W((T1 T2 ) .f (x).e f (x).T, γ
b)

= W(T, γ
b0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ])
⊆ occ 6⊥ (b
γ0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ])

= occ 6⊥ (b
γ0 ) ∪ occ 6⊥ (hf (x).e, γ
b0 ia ) ∪ occ 6⊥ (b
v2 )

⊆

occ 6⊥ (b
γ)

37

A.2

Proof of Theorem 4.9

Proof of Theorem 4.9. We prove by induction on the structure of derivations that if |b
γ |, e ⇓ v, T , then for any h
consistent with γ
b, we have that h is also consistent with E(T, γ
b).
• Base cases involving constants and variables are trivial.
• Cases involving constructors (pairs, inl, inr, roll, closures) are straightforward since the newly-constructed
value is annotated with ⊥.
• For primitive operations, consider a primitive function evaluation:
|b
γ |, e1 ⇓ v1 , T1
···
|b
γ |, en ⇓ vn , Tn
ˆ
|b
γ |, ⊕(e1 , . . . , en ) ⇓ ⊕(v1 , . . . , vn ), ⊕(T1 , . . . , Tn )
Suppose h is consistent with γ
b. By induction, h is consistent with E(Ti , γ
b) for each i. This means that each of the
ˆ 1 , . . . , vn ) = ⊕(h(t
ˆ
b)| = vi . Thus, ⊕(v
results viti satisfies h(ti ) = |E(Ti , γ
1 ), . . . , h(tn )) = h(⊕(t1 , . . . , tn )),
ˆ 1 , . . . , vn ))⊕(t1 ,...,tn ) , as desired.
which implies that h is consistent with E(T, γ
b) = (⊕(v
• The remaining cases follow similar reasoning to that for where-provenance.
• For a derivation of the form:
inl(x1 ).e1 ∈ m
|b
γ |, e1 ⇓ inl(v), T
|b
γ |[x1 7→ v], e1 ⇓ v1 , T1
|b
γ |, case e of m ⇓ v1 , case T .inl x1 .T1
Suppose h is consistent with γ
b. By induction, h is consistent with E(T, γ
b). Moreover, E(T, γ
b) = inl(b
v )a
for some vb with |b
v | = v. Thus, h is consistent with vb and γ
b[x1 7→ vb], so by induction, h is consistent with
E(T1 , γ
b[x1 7→ vb]). Since E(case T .inl x1 .T1 , γ
b)) = E(T1 , γ
b[x1 7→ vb]), it follows that h is consistent with
E(case T .inl x1 .T1 , γ
b)).
• The case for case where the right branch is taken is symmetric.
• For function application, if the derivation is of the form:
|b
γ |, e1 ⇓ hf (x).e, γ0 i, T1

|b
γ |, e2 ⇓ v2 , T2
γ0 [f 7→ hf (x).e, γ0 i, x 7→ v2 ], e ⇓ v, T
|b
γ |, (e1 e2 ) ⇓ v, (T1 T2 ) .f (x).e f (x).T

then by validity we know that E(T1 , γ
b) = hf (x).e, γ
b0 ia with |b
γ0 | = γ
b and E(T2 , γ
b) = vb2 with |b
v2 | =
v2 . By induction, we also know h is consistent with hf (x).e, γ
b0 ia and vb2 , so h is consistent with γ
b0 [f 7→
hf (x).e, γ
b0 ia , x 7→ vb2 ]. By induction on the third subderivation, we have that h is consistent with E(T, γ
b0 [f 7→
hf (x).e, γ
b0 ia , x 7→ vb2 ]). To conclude, since
E((T1 T2 ) .f (x).e f (x).T, γ
b) = E(T, γ
b0 [f 7→ hf (x).e, γ
b0 ia , x 7→ vb2 ]) ,
we know that h is consistent with E((T1 T2 ) .f (x).e f (x).T, γ
b).

A.3

Proof of Theorem 4.11

Lemma A.1.
1. If vb1 ≈` vb2 then vb1+a ≈` vb2+a .
2. If ` ∈ a ∩ b then vb1+a ≈` vb2+b .
38

Proof. Similar to a property proved in [17]; the only new cases are for closures, and are straightforward.
Proof of Theorem 4.11. Proof proceeds by induction on the structure of the derivation of |b
γ |, e ⇓ v, T . There are many
straightforward cases, similar to those proved in [17]. We show the proof cases for case and application traces; the
other cases use similar techniques.
• If the derivation is of the form:
(inl(x1 ).e1 ∈ m)
|b
γ |, e ⇓ inl(v), T
|b
γ |[x1 7→ v], e1 ⇓ v1 , T1
|b
γ |, case e of m ⇓ v1 , case T .inl x1 .T1
then by inversion of |b
γ 0 |, case T .inl x1 .T1 y v 0 the derivation must be of the form:
|b
γ 0 |, T y inl(v)
|b
γ 0 |[x1 7→ v], T1 y v1
|b
γ 0 |, case T .inl x1 .T1 y v1
Then by validity of D and induction we know that inl(b
v )a = D(T, γ
b) ≈` D(T 0 , γ
b) = inl(b
v 0 )b , where |b
v| = v
and |b
v 0 | = v 0 . Then |b
γ [x 7→ vb]| = |b
γ |[x 7→ v] and |b
γ 0 [x 7→ vb0 ]| = |b
γ 0 |[x 7→ v 0 ]. Now, if ` ∈ a ∩ b then we are
done: it follows immediately that
D(case T .inl x1 .T1 , γ
b) = (b
v1 )+a ≈` (b
v10 )+b = D(case T 0 .inl x1 .T10 , γ
b0 )
Otherwise, we must have vb ≈` vb0 and a = b; hence, γ
b[x 7→ vb] ≈` γ
b0 [x 7→ vb0 ]. So, by induction, vb1 =
D(T1 , γ
b[x 7→ vb]) ≈` D(T10 , γ
b0 [x 7→ vb0 ]) = vb10 . Then it follows immediately that
D(case T .inl x1 .T1 , γ
b) = (b
v1 )+a ≈` (b
v10 )+a = D(case T 0 .inl x1 .T10 , γ
b0 )
• Application: Suppose the derivation is of the form:
|b
γ |, e1 ⇓ hκ, γ0 i, T1

(κ = f (x).e)
|b
γ |, e2 ⇓ v2 , T2
γ0 [f 7→ hκ, γ0 i, x 7→ v2 ], e ⇓ v, T
|b
γ |, (e1 e2 ) ⇓ v, (T1 T2 ) .κ f (x).T

By validity we know that D(T1 , γ
b) = hκ, γ
b0 ia for some a, γ
b0 with |b
γ0 | = γ0 . Similarly, D(T2 , γ
b) = vb2 for some
vb2 with |b
v2 | = v2 . Finally, D(T, γ
b0 [f 7→ hκ, γ
b0 ia , x 7→ vb2 ]) = vb for some vb with |b
v | = v.
Then the replay derivation is of the form:
|b
γ 0 |, T1 y hκ, γ00 i

|b
γ 0 |, T2 y v20
γ00 [f →
7 hκ, γ00 i, x 7→ v20 ], T y v 0
0
|b
γ |, (T1 T2 ) .κ f (x).T y v 0

First, note that by fidelity and validity D(T10 , γ
b0 ) = hκ, γ
b00 ib for some b, γ
b00 with |b
γ00 | = γ00 . Similarly, D(T20 , γ
b0 ) =
0
0
0
0
0
0
0 b
0
0
0
0
0
vb2 for some vb2 with |b
v2 | = v2 . Finally, D(T , γ
b0 [f 7→ hκ, γ
b0 i , x 7→ vb2 ]) = vb for some vb with |b
v|=v.
Then, by induction, we know that
hκ, γ
b0 ia = D(T1 , γ
b) ≈` D(T10 , γ
b0 ) = hκ, γ
b00 ib

vb2 = D(T2 , γ
b) ≈` D(T20 , γ
b0 ) = vb20

Now, there are two cases. If ` ∈ a ∩ b, then we are done since we can derive:
D((T1 T2 ) .κ f (x).T, γ
b) = vba ≈` (b
v 0 )b = D((T10 T20 ) .κ f (x).T 0 , γ
b0 )
Otherwise, we know that a = b and γ
b0 ≈` γ
b00 , hence also:
γ
b0 ≈` γ
b00
hκ, γ
b0 ia ≈` hκ, γ
b00 ib
vb2 ≈` vb20
a
0
γ
b0 [f 7→ hκ, γ
b0 i , x 7→ vb2 ] ≈` γ
b0 [f 7→ hκ, γ
b00 ia , x 7→ vb20 ]
Then by induction on the remaining subderivations, we have vb ≈` vb0 , from which we can infer vb+a ≈` (b
v 0 )+a .

39

A.4

Proof of Lemma 5.1

Lemma A.2. For any p, we have (hp[♦/] ) = (h♦ ) ∩ (hp ).
Proof. Induction on p.
• If p = , then the result is immediate since (h♦ ) ∩ (h ) = (h♦ ).
• If p = ♦, then the result is immediate.
• If p = (p1 , p2 ), then p[♦/] = (p1 [♦/], p2 [♦/]), so we reason as follows:
(v1 , v2 ) h(p1 [♦/],p2 [♦/]) (v10 , v20 )

⇐⇒

v1 hp1 [♦/] v10 and v2 hp2 [♦/] v20

⇐⇒

v1 h♦ v10 and v1 hp1 v10 and v2 h♦ v20 and v2 hp2 v20

⇐⇒

(v1 , v2 ) h(♦,♦) (v10 , v20 ) and (v1 , v2 ) h(p1 ,p2 ) (v10 , v20 )

⇐⇒

(v1 , v2 ) h♦ (v10 , v20 ) and (v1 , v2 ) h(p1 ,p2 ) (v10 , v20 )

• The cases for p = C(p0 ) or p = hκ, ρi are similar to the case for pairing.

Proof of Lemma 5.1. Symmetry of (hp ) follows by straightforward induction on derivations.
We show transitivity by induction on p.
• If p = , then transitivity is obvious as (hp ) is the total relation.
• If p = ♦, then transitivity is obvious as (h♦ ) is the identity relation.
• If p = c then suppose v1 hc v2 and v2 hc v3 . Then v1 , v2 , v3 are all constants. By inversion, we must have
v1 = v2 = v3 = c so we have v1 = c hc c = v3 .
• If p = C(p0 ), then suppose v1 hC(p0 ) v2 and v2 hC(p0 ) v3 . By inversion, we must have
v10 hp0 v20
hC(p0 ) C(v20 )

C(v10 )

v20 hp0 v30
hC(p0 ) C(v30 )

C(v20 )

where vi = C(vi0 ) for each i. In this case, by induction we have v10 hp0 v30 so we can conclude C(v10 ) hC(p0 )
C(v30 ) as desired.
• If p = (p1 , p2 ) then transitivity follows immediately by induction.
• If p = hκ, ρi, then the reasoning is similar to that for p = C(p0 ).
We show by induction on pairs (p, p0 ) such that p t p0 exists, that (hptp0 ) = (hp ) ∩ (hp0 ).
• If one of the patterns (say, p) is  then  t p0 = p0 , so (htp0 ) = (hp0 ) = (h ) ∩ (hp0 ) since h is total.
• If one of the patterns (say, p) is ♦ then ♦ t p0 = p0 [♦/], so (h♦tp0 ) = (hp0 [♦/] ) = (h♦ ) ∩ (hp0 ), where the
second equation is Lemma A.2.
• If (p1 , p2 ) t (p01 , p02 ) = (p1 t p01 , p2 t p02 ) then
(v1 , v2 ) h(p1 tp01 ,p2 tp02 ) (v10 , v20 )

⇐⇒

v1 hp1 tp01 v10 and v2 hp2 tp02 v20

⇐⇒

v1 hp1 v10 and v1 hp01 v10 and v2 hp2 v20 and v2 hp02 v20

⇐⇒

(v1 , v2 ) h(p1 ,p2 ) (v10 , v20 ) and (v1 , v2 ) h(p01 ,p02 ) (v10 , v20 )

• For the cases C(p) t C(p0 ) and hκ, ρi t hκ, ρ0 i the reasoning is similar to the case for pairing.

40

A.5

Proof of Lemma 5.15
disc

Proof of Lemma 5.15. The proof is by induction on the derivation of p, T −→ S, ρ and inversion on γ, T y v. We
use Lemma 5.1 freely without comment to infer, for example, γ hρi γ 0 from γ hρ1 tρ2 γ 0 .
Empty pattern. If the derivation is of the form:

disc

, T −→ , 
then clearly, for any γ 0 h γ and T 0 w , if γ
b0 , T 0 y v 0 then v 0 h v.
Variable. If the derivations are of the form:
and

disc

γ, x y γ(x)

p, x −→ x, [x 7→ p]
Then T 0 w x implies T 0 = x, so
γ 0 , x ⇓ γ 0 (x)

Since by assumption γ 0 h[x7→p] γ, we conclude that γ 0 (x) hp γ(x), as desired.
Let. If the derivations are of the form:
disc

p2 , T2 −→ S2 , ρ2 [x 7→ p1 ]

disc

p1 , T1 −→ S1 , ρ1

disc

and

p2 , let x = T1 in T2 −→ let x = S1 in S2 , ρ1 t ρ2

γ, T1 y v1
γ[x 7→ v1 ], T2 y v2
γ, let x = T1 in T2 y v2

Then by inversion we must have T 0 = let x = T10 in T20 where Ti0 w Si , and:
γ 0 , T10 y v10
γ 0 [x 7→ v10 ], T20 y v20
γ 0 , let x = T10 in T20 y v20
We also know that γ hρ1 γ 0 and γ hρ2 γ 0 . Then, by induction, we have v1 hp1 v10 , hence we know that γ[x 7→
disc

v1 ] hρ1 [x7→p1 ] γ 0 [x 7→ v10 ]. So, the induction hypothesis applies to p2 , T2 −→ S2 , ρ2 [x 7→ p1 ], and we can conclude
that v2 hp2 v20 .
Constant trace. If the trace has the form c, then we have:

disc

and

p, c −→ c, 

γ, c y c

Then clearly γ 0 , c y c and c hp c.
Primitives. If the trace has the form ⊕(T ) = ⊕(T1 , . . . , Tn ), then we have:
disc

♦, T1 −→ S1 , ρ1

...

disc

♦, Tn −→ Sn , ρn

disc

p, ⊕(T1 , . . . , Tn ) −→ ⊕(S1 , . . . , Sn ), ρ1 t · · · t ρn
41

and

γ, T1 y v1
...
γ, Tn y vn
.
ˆ 1 , . . . , vn )
γ, ⊕(T1 , . . . , Tn ) y ⊕(v

Suppose T 0 w ⊕(S1 , . . . , Sn ). This implies T 0 = ⊕(T10 , . . . , Tn0 ) where Ti0 w Si for each i. Moreover, by inversion
we must have:
γ, T10 y v10
...
γ, Tn0 y vn0
ˆ 10 , . . . , vn0 ).
γ, ⊕(T10 , . . . , Tn0 ) y ⊕(v
By induction, we have for all 1 ≤ i ≤ n, that vi0 h♦ vi , that is, vi0 = vi . Hence, we can conclude that
ˆ 10 , . . . , vn0 ) hp ⊕(v
ˆ 1 , . . . , vn ) since both sides are equal.
⊕(v
Pairs/pair patterns. If the derivation is of the form:
disc

disc

p1 , T1 −→ S1 , ρ1

p2 , T2 −→ S2 , ρ2
disc

and

(p1 , p2 ), (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2

γ, T1 y v1
γ, T2 y v2
.
γ, (T1 , T2 ) ⇓ (v1 , v2 )

Then, as in the previous case we know T 0 = (T10 , T20 ) where Ti0 w Si and
γ 0 , T10 y v10
γ 0 , T20 y v20
.
γ 0 , (T10 , T20 ) y (v10 , v20 )
By induction, we have v1 hp1 v10 and v2 hp2 v20 , from which it follows that (v1 , v2 ) h(p1 ,p2 ) (v10 , v20 ).
First. If the derivation is of the form:
disc

(p, ), T −→ S, ρ

and

disc

p, fst(T ) −→ fst(S), ρ

γ, T y (v1 , v2 )
γ, fst(T ) y v1

then, by inversion, we know that T 0 = fst(T00 ) for some T00 w S, such that
γ 0 , T00 ⇓ (v10 , v20 ), T 00
γ 0 , fst(T00 ) ⇓ v10 , fst(T 00 )
By induction, we have (v10 , v20 ) h(p,) (v1 , v2 ), which implies that v10 hp v1 .
Second.

Symmetric to fst case.

Inl. Suppose the derivations are of the form:
disc

p, T −→ S, ρ

and

disc

inl(p), inl(T ) −→ inl(S), ρ

γ, T y v
γ, inl(T ) y inl(v)

Then we must have T 0 = inl(T00 ) where T00 w S, and:
γ 0 , T00 y v 0
γ 0 , inl(T00 ) y inl(v 0 )
So, by induction, we know that v hp v 0 and so inl(v) hinl(p) inl(v 0 ).
Inr. Symmetric to inl case.

42

Case/L. If the derivations are of the form:
disc

disc

p1 , T1 −→ S1 , ρ1 [x1 7→ p]

inl(p), T −→ S, ρ

disc

p1 , case T .inl x1 .T1 −→ case S .inl x1 .S1 , ρ t ρ1
and
γ, T y inl(v)
γ[x1 7→ v], T1 y v1
γ, case T .inl x1 .T1 y v1
Then T 0 = case T00 .inl x1 .T10 where T00 w S and T10 w S1 . The only way for the replay judgment γ, T 0 y v 0 to be
derived is:
γ 0 , T00 y inl(v00 )
γ[x1 7→ v00 ], T10 y v 0
γ, case T00 .inl x1 .T10 y v 0
so by induction we can conclude inl(v) hinl(p) inl(v00 ), which in turn implies v hp v00 . Thus, γ[x 7→ v] hρ1 [x7→p]
γ 0 [x 7→ v00 ], from which it follows by induction that v1 hp1 v 0 .
Case/R.

Symmetric to the previous case.

Function abstraction. If the derivations have the form:
and

disc

hκ, ρi, fun κ −→ fun κ, ρ

γ, fun κ y hκ, γi

then T 0 must be of the form fun κ, with derivation:
γ 0 , fun κ y hκ, γ 0 i
Hence, we can conclude hκ, γi hhκ,ρi hκ, γ 0 i immediately from γ hρ γ 0 .
Application. If the derivations are of the form:
disc

p, T −→ S, ρ[f 7→ p1 , x 7→ p2 ]

disc

p1 t hκ, ρi, T1 −→ S1 , ρ1

disc

p2 , T2 −→ S2 , ρ2

disc

p, (T1 T2 ) .κ f (x).T −→ (S1 S2 ) .κ f (x).S, ρ1 t ρ2
γ, T1 y hκ, γ0 i

and
γ, T2 y v2
γ0 [f 7→ hκ, γ0 i, x 7→ v2 ], T y v
γ, (T1 T2 ) .κ f (x).T y v

Then we know that T 0 = (T10 T20 ) .κ f (x).T00 where T10 w S1 and T20 w S2 and T00 w S. The replay derivation of
γ 0 , T 0 y v 0 must be of the form:
γ 0 , T10 y hκ, γ00 i

γ 0 , T20 y v20
γ00 [f 7→ hκ, γ00 i, x 7→ v20 ], T00 y v 0
γ 0 , (T10 T20 ) .κ f (x).T00 y v 0

First, by induction on the first subderivation we know that hκ, γ0 i hp1 thκ,ρi hκ, γ00 i. Here, recall that p1 is a value
pattern for the function argument obtained from slicing the body. By inversion, we have
hκ, γ0 i hp1 hκ, γ00 i

γ0 hρ γ00

By induction, we also have that v2 hp2 v20 . Hence, putting the above observations together, we have:
γ0 [f 7→ hκ, γ0 i, x 7→ v2 ] hρ[f 7→p1 ,x7→p2 ] γ00 [f 7→ hκ, γ00 i, x 7→ v20 ]
Thus, the induction hypothesis applies again and we can conclude that v hp v 0 .
43

Roll and unroll. These cases are straightforward, similar to those for pairs and projection.
Pairs/wildcard. If the trace has the form (T1 , T2 ), then we have:
disc

♦, T1 −→ S1 , ρ1

disc

♦, T2 −→ S2 , ρ2

disc

and

♦, (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2

γ, T1 y v1
γ, T2 y v2
.
γ, (T1 , T2 ) y (v1 , v2 )

Then T 0 w (S1 , S2 ) so T 0 must be of the form (T10 , T20 ) with T1 w S1 and T2 w S2 , and we must have
γ 0 , T1 y v10
γ 0 , T2 y v20
.
0
0
0
γ , (T1 , T2 ) y (v10 , v20 )
By induction, we have v1 h♦ v10 and v2 h♦ v20 , which implies (v1 , v2 ) h♦ (v10 , v20 ), as required.
Other wildcard cases Other cases involving wildcards are similar to the above.

A.6

Proof of Theorem 5.20
disc

Proof of Theorem 5.20. The proof is by induction on the structure of the derivation of p, T −→ S, ρ. We show that if
|b
γ |, T y |F(T, γ
b)| then for any T 0 , γ
b0 , if γ
b hρ γ
b0 and S v T 0 and |b
γ 0 |, T 0 y |F(T 0 , γ
b0 )| then F(T, γ
b) hp F(T 0 , γ
b0 ).
• If the slicing derivation is of the form:
disc

, T −→ , 
then we are done: the conclusion is trivial since F(T, γ
b) h F(T 0 , γ
b0 ).
• If the slicing derivation is of the form:
disc

p, x −→ x, [x 7→ p]
then we reason as follows:
F(x, γ
b) = γ
b(x) hp γ
b0 (x) = F(x, γ
b0 )
where γ
b(x) hp γ
b0 (x) follows from the assumption that γ
b h[x7→p] γ
b0 .
• If the slicing derivation is of the form:
disc

p2 , T2 −→ S2 , ρ2 [x 7→ p1 ]

disc

p1 , T1 −→ S1 , ρ1

disc

p2 , let x = T1 in T2 −→ let x = S1 in S2 , ρ1 t ρ2
then let T10 w S1 , T20 w S2 and γ
b 0 hρ γ
b be given. By induction and validity we have
vb1 = F(T1 , γ
b) hp1 F(T10 , γ
b0 ) = vb10
thus, we also know that γ
b[x 7→ vb1 ] hρ1 [x7→p1 ] γ
b0 [x 7→ vb10 ]. So, by induction, we also have:
vb2 = F(T2 , γ
b[x 7→ vb1 ]) hp2 F(T20 , γ
b0 [x 7→ vb10 ]) = vb20
Thus,
F(let x = T1 in T2 , γ
b) = vb2 hp2 vb20 = F(let x = T10 in T20 , γ
b0 )

44

• If the slicing derivation is of the form:
disc

p, c −→ c, 
then again we are done as F(c, γ
b) = cFc = F(c, γ
b0 ).
• If the slicing derivation is of the form:
disc

♦, T −→ S, ρ
disc

p, ⊕(T ) −→ ⊕(S),

G

ρ

then let γ
b0 , T 0 be given with γ
b 0 hF ρ γ
b and T 0 w S. By induction, we know that F(Ti , γ
b) h♦ F(Ti0 , γ
b0 ) (that is,
0
0
0
0
F(Ti , γ
b) = F(Ti , γ
b )) holds for each i. Let vbi = F(Ti , γ
b) = F(Ti , γ
b ) for each i. Then we can reason as follows:
ˆ v1 |, . . . , |b
ˆ v1 |, . . . , |b
F(⊕(T ), γ
b)) = ⊕(|b
vn |)F⊕ (a1 ,...,an ) hp ⊕(|b
b0 )
vn |)F⊕ (a1 ,...,an ) = F(⊕(T 0 ), γ
• If the slicing derivation is of the form:
disc

disc

p1 , T1 −→ S1 , ρ1

p2 , T2 −→ S2 , ρ2
disc

(p1 , p2 ), (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2
then let γ 0 , T10 , T20 be given with T10 w S1 , T20 w S2 and γ
b0 hρ1 tρ2 γ
b. By induction we know that F(T1 , γ
b ) hp 1
0
0
0
0
F(T1 , γ
b ) and F(T2 , γ
b) hp2 F(T2 , γ
b ) so we can conclude:
F((T1 , T2 ), γ
b)

(F(T1 , γ
b), F(T2 , γ
b))⊥

=

(F(T10 , γ
b0 ), F(T20 , γ
b0 ))⊥

h(p1 ,p2 )

F((T10 , T20 ), γ
b0 )

=
• If the slicing derivation is of the form:

disc

(p, ), T −→ S, ρ
disc

p, fst(T ) −→ fst(S), ρ
then fix T 0 w S and γ
b0 hρ γ
b. If p = , then the conclusion is immediate. By induction we know that
0
F(T, ρ) h(p,) F(T , ρ). Then by inversion on the replay derivation and validity we know that
0

F(T, ρ) = (b
v1 , vb2 )a h(p,) (b
v10 , vb20 )a = F(T 0 , γ
b0 )
0

Since p 6= , this implies a = a0 and v1b = vb1 hp vb10 = (v10 )b , hence, v1 hp v10 and b = b0 . We can conclude
by reasoning as follows:
F (a,b)

F(fst(T ), γ
b ) = v1 1

0

0

hp (v10 )F1 (a ,b ) = F(fst(T 0 ), ρ)

• If the slicing derivation is of the form:
disc

(, p), T −→ S, ρ
disc

p, snd(T ) −→ snd(S), ρ
then the reasoning is symmetric to the previous case.

45

• If the slicing derivation is of the form:
disc

p, T −→ S, ρ
disc

inl(p), inl(T ) −→ inl(S), ρ
then fix T 0 w S and γ
b 0 hρ γ
b. By induction we know that F(T, γ
b) hp F(T 0 , γ
b0 ), so it follows directly that
F(inl(T ), γ
b) = inl(F(T, γ
b))⊥ hinl(p) inl(F(T 0 , γ
b0 ))⊥ = F(inl(T 0 ), γ
b0 )
• If the slicing derivation is of the form:
disc

p, T −→ S, ρ
disc

inr(p), inr(T ) −→ inr(S), ρ
then the reasoning is symmetric to the previous case.
• If the slicing derivation is of the form:
disc

p1 , T1 −→ S1 , ρ1 [x1 7→ p]

disc

inl(p), T −→ S, ρ

disc

p1 , case T .inl x1 .T1 −→ case S .inl x1 .S1 , ρ t ρ1
then fix T00 w S, T10 w S1 and γ
b0 hρtρ1 γ
b. If p =  then the conclusion is immediate. By induction we know
0
that F(T, γ
b) hinl(p) F(T0 , γ
b), and by validity this means that F(T, γ
b) = (inl(b
v ))a and F(T00 , γ
b0 ) = (inl(b
v 0 ))a
0
0
0
where vb hp vb . Thus, γ
b[x1 7→ vb] hρ1 [x1 7→p] γ
b [x1 7→ vb ], so by induction we also have
0

v1b = F(T1 , γ
b[x1 7→ vb]) hp1 F(T10 , γ
b0 [x1 7→ vb0 ]) = (v10 )b .
Moreover, since p 6=  we know b = b0 and v1 hp1 v10 , so:
F (a,b)

F(case T .inl x1 .T1 , γ
b ) = v1 L

0

hp1 (v10 )FL (a,b ) = F(case T00 .inl x1 .T10 , γ
b0 )

• If the slicing derivation is of the form:
disc

p2 , T2 −→ S2 , ρ2 [x2 7→ p]

disc

inr(p), T −→ S, ρ

disc

p2 , case T .inr x2 .T2 −→ case S .inr x2 .S2 , ρ t ρ2
then the reasoning is symmetric to the previous case.
• If the slicing derivation is of the form:

disc

hκ, ρi, fun κ −→ fun κ, ρ
b 0 hρ γ
b be given; note that T 0 = fun κ. We can conclude immediately that
then let T 0 w fun κ and γ
F(fun κ, γ
b) = hκ, γ
bi⊥ hρ hκ, γ
b0 i⊥ = F(fun κ, γ
b0 )
• If the slicing derivation is of the form:
disc

p, T −→ S, ρ[f 7→ p1 , x 7→ p2 ]

disc

p1 t hκ, ρi, T1 −→ S1 , ρ1
disc

p, (T1 T2 ) .κ f (x).T −→ (S1 S2 ) .κ f (x).S, ρ1 t ρ2
46

disc

p2 , T2 −→ S2 , ρ2

Let T10 , T20 , T00 and γ
b0 be given with T10 w S1 , T20 w S2 and T00 w S, and γ
b0 hρ1 tρ2 γ
b. If p = , then the
conclusion is immediate. Otherwise, by induction, validity, and inversion of h− derivations, we know that:
hκ, γ
b0 ia = F(T1 , γ
b) hp1 thκ,ρi
vb2 = F(T2 , γ
b)

hp2

F(T10 , γ
b0 ) = hκ, γ
b00 ia
F(T20 , γ
b0 ) = vb20

Thus, we also have γ
b0 hρ γ
b00 , so we can obtain:
γ
b0 [f 7→ hκ, γ
b0 ia , x 7→ vb2 ] hρ[f 7→p1 ,x7→p2 ] γ
b00 [f 7→ hκ, γ
b00 ia , x 7→ vb20 ]
By induction, it follows that
v b = F(T, γ
b0 [f 7→ hκ, γ
b0 i, x 7→ vb2 ]) hp F(T00 , γ
b00 [f 7→ hκ, γ
b00 i, x 7→ vb20 ] = v 0

b0

This, together with the fact that p 6= , implies that v hp v 0 and b = b0 , so:
0

F((T1 T2 ) .κ f (x).T, γ
b) = v Fapp (a,b) hp (v 0 )Fapp (a,b ) = F((T10 T20 ) .κ f (x).T00 , γ
b0 )
• The cases for roll and unroll are analogous to the cases for pairing and projection.
• If the slicing derivation is of the form:
disc

disc

♦, T1 −→ S1 , ρ1

♦, T2 −→ S2 , ρ2

disc

♦, (T1 , T2 ) −→ (S1 , S2 ), ρ1 t ρ2
then fix γ
b0 , T10 , T20 with Ti0 w Si and γ
b0 hρ1 tρ2 γ
b. By induction we know that F(Ti , γ
b) h♦ F(Ti0 , γ
b0 ) (that is,
0
0
F(Ti , γ
b) = F(Ti , γ
b )) holds for each i ∈ {1, 2}. We reason as follows:
F((T1 , T2 ), γ
b)

=
=

(F(T1 , γ
b), F(T2 , γ
b))⊥

(F(T10 , γ
b0 ), F(T20 , γ
b0 ))⊥

= F((T10 , T20 ), γ
b)

• The other cases in which p = ♦ are straightforward, following similar reasoning to the above cases where p
starts with a value constructor.

A.7

Proof of Lemma 5.24
obf

Proof of Lemma 5.24. The proof is by induction on the structure of derivations of ρ, T −→ p, S, and inversion on
derivations of γ, e ⇓ v, T .
• If the derivations are of the form:
obf

ρ, x −→ ρ(x), x

γ, x ⇓ γ(x), x

then suppose γ 0 w ρ and γ 0 , x ⇓ v 0 , T 0 . Then v 0 = γ 0 (x) and T 0 = x, so it suffices to observe that

obf

ρ, x −→ ρ(x), x
hold.
47

ρ(x) v γ 0 (x)

• If the derivations are of the form:
obf

ρ, c −→ ρ(x), c
0

0

0

γ, c ⇓ c, c

0

then suppose γ w ρ where γ , c ⇓ v , T . By inversion the only way the latter can be derived is if v 0 = c and
T 0 = c. So we can conclude by observing:
obf

ρ, c −→ c, c

cvc

• If the derivations are of the form:
obf

ρ, fun κ −→ hκ, ρi, fun κ

γ, fun κ ⇓ hκ, γi, fun κ

then suppose γ 0 w ρ is given where γ 0 , fun κ ⇓ v 0 , T 0 . By inversion we must have v 0 = hκ, γ 0 i and T 0 = fun κ.
Thus, we can conclude by observing:
obf

ρ, fun κ −→ hκ, ρi, fun κ

hκ, ρi v hκ, γ 0 i

• If the derivations are of the form:
obf

ρ, T1 −→ p1 , S1

obf

ρ[x 7→ p1 ], T2 −→ p2 , S2
obf

ρ, let x = T1 in T2 −→ p2 , let x = S1 in S2

γ, e1 ⇓ v1 , T1
γ[x 7→ v1 ], e2 ⇓ v2 , T2
γ, let x = e1 in e2 ⇓ v2 , let x = T1 in T2

then suppose γ 0 v ρ and γ 0 , let x = e1 in e2 ⇓ v 0 , T 0 . By inversion, this derivation is of the form:
γ 0 , e1 ⇓ v10 , T10
γ 0 [x 7→ v10 ], e2 ⇓ v20 , T20
γ 0 , let x = e1 in e2 ⇓ v20 , let x = T10 in T20
obf

and v 0 = v20 and T 0 = let x = T10 in T20 . By induction, we have ρ, T10 −→ p1 , S1 and p1 v v10 . Thus,
obf

γ 0 [x 7→ v10 ] w ρ[x 7→ p1 ], so by induction, we have ρ[x 7→ p1 ], T20 −→ p2 , S2 where p2 v v20 . To conclude, we
have:
obf
obf
ρ, T10 −→ p1 , S1
ρ[x 7→ p1 ], T20 −→ p2 , S2
obf

ρ, let x = T10 in T20 −→ p2 , let x = S1 in S2

p2 v v20

• If the derivations are of the form:
obf

ρ, T1 −→ v1 , S1

obf

···

ρ, Tn −→ vn , Sn

obf

ρ, ⊕(T1 , . . . , Tn ) −→ ⊕(v1 , . . . , vn ), ⊕(S1 , . . . , Sn )

γ, e1 ⇓ v1 , T1
···
γ, en ⇓ vn , Tn
ˆ
γ, ⊕(e1 , . . . , en ) ⇓ ⊕(v1 , . . . , vn ), ⊕(T1 , . . . , Tn )

then suppose γ 0 w ρ and γ 0 , ⊕(e1 , . . . , en ) ⇓ v 0 , T 0 . By inversion the derivation must be of the form:
γ 0 , e1 ⇓ v10 , T10
···
γ 0 , en ⇓ vn0 , Tn0
ˆ 10 , . . . , vn0 ), ⊕(T10 , . . . , Tn0 )
γ 0 , ⊕(e1 , . . . , en ) ⇓ ⊕(v
obf

ˆ 10 , . . . , vn0 ) and T 0 = ⊕(T10 , . . . , Tn0 ). By induction, we know that for each i, ρ, Ti0 −→ vi , Si
where v 0 = ⊕(v
0
and vi v vi . The latter implies vi = vi0 since vi is a constant value. Thus, we can conclude:
obf

ρ, T10 −→ v1 , S1

···

obf

ρ, Tn0 −→ vn , Sn

obf

ρ, ⊕(T10 , . . . , Tn0 ) −→ ⊕(v1 , . . . , vn ), ⊕(S1 , . . . , Sn )
48

ˆ 1 , . . . , vn ) = ⊕(v
ˆ 10 , . . . , vn0 ) = v 0
⊕(v

• If the derivations are of the form:
obf

ρ, Ti −→ , Si

(for some i ∈ 1, . . . , n)

γ, e1 ⇓ v1 , T1
···
γ, en ⇓ vn , Tn
ˆ 1 , . . . , vn ), ⊕(T1 , . . . , Tn )
γ, ⊕(e1 , . . . , en ) ⇓ ⊕(v

obf

ρ, ⊕(T1 , . . . , Tn ) −→ , 

then suppose γ 0 w ρ and γ 0 , ⊕(e1 , . . . , en ) ⇓ v 0 , T 0 . By inversion the derivation must be of the form:
γ 0 , e1 ⇓ v10 , T10
···
γ 0 , en ⇓ vn0 , Tn0
ˆ 10 , . . . , vn0 ), ⊕(T10 , . . . , Tn0 )
γ 0 , ⊕(e1 , . . . , en ) ⇓ ⊕(v
obf
ˆ 10 , . . . , vn0 ) and T 0 = ⊕(T10 , . . . , Tn0 ). By induction, we know that ρ, Ti0 −→
where v 0 = ⊕(v
, Si and  v vi0 .
Thus, we can conclude:
obf

ρ, Ti0 −→ , Si

(for some i ∈ 1, . . . , n)
obf

ρ, ⊕(T10 , . . . , Tn0 ) −→ , 

ˆ 10 , . . . , vn0 ) = v 0
 v ⊕(v

• Suppose the derivations are of the form:
obf

obf

ρ, T1 −→ p1 , S1

ρ, T2 −→ p2 , S2

obf

ρ, (T1 , T2 ) −→ (p1 , p2 ), (S1 , S2 )

γ, e1 ⇓ v1 , T1
γ, e2 ⇓ v2 , T2
γ, (e1 , e2 ) ⇓ (v1 , v2 ), (T1 , T2 )

and suppose γ 0 w ρ is given, where γ 0 , (e1 , e2 ) ⇓ v 0 , T 0 . By inversion, the derivation must have the form:
γ 0 , e1 ⇓ v10 , T10
γ 0 , e2 ⇓ v20 , T20
0
0
γ , (e1 , e2 ) ⇓ (v1 , v20 ), (T10 , T20 )
obf

obf

so v 0 = (v10 , v20 ) and T 0 = (T10 , T20 ). By induction we have ρ, T10 −→ p1 , S1 and p1 v v10 and ρ, T20 −→ p2 , S2
and p2 v v20 . So we can conclude:
obf

obf

ρ, T10 −→ p1 , S1

ρ, T20 −→ p2 , S2

obf

ρ, (T10 , T20 ) −→ (p1 , p2 ), (S1 , S2 )

(p1 , p2 ) v (v10 , v20 )

• Suppose the derivations are of the form:
obf

ρ, T −→ (p1 , p2 ), S
obf

ρ, fst(T ) −→ p1 , fst(S)

γ, e ⇓ (v1 , v2 ), T
γ, fst(e) ⇓ v1 , fst(T )

and suppose γ 0 w ρ is given, where γ 0 , fst(e) ⇓ v 0 , T 0 . By inversion, the derivation must have the form:
γ 0 , e ⇓ (v10 , v20 ), T 0
γ , fst(e) ⇓ v10 , fst(T 0 )
0

obf

so v 0 = v10 and T 0 = fst(T 0 ). By induction, we know that ρ, T 0 −→ (p1 , p2 ), S where (p1 , p2 ) v (v10 , v20 ). So
we can conclude:
obf
ρ, T 0 −→ (p1 , p2 ), S
obf

ρ, fst(T 0 ) −→ p1 , fst(S)

49

p1 v v10

• Suppose the derivations are of the form:
obf

ρ, T −→ , S

γ, e ⇓ (v1 , v2 ), T
γ, fst(e) ⇓ v1 , fst(T )

obf

ρ, fst(T ) −→ , 

and suppose γ 0 w ρ is given, where γ 0 , fst(e) ⇓ v 0 , T 0 . By inversion, the derivation must have the form:
γ 0 , e ⇓ (v10 , v20 ), T 0
γ 0 , fst(e) ⇓ v10 , fst(T 0 )
obf

so v 0 = v10 and T 0 = fst(T 0 ). By induction, we know that ρ, T 0 −→ (p1 , p2 ), S where  v (v10 , v20 ). So we
can conclude:
obf
ρ, T 0 −→ , S
obf

ρ, fst(T 0 ) −→ , 

 v v10

• The cases for snd(e) are symmetric.
• Suppose the derivations are of the form:
obf

ρ, T −→ p, S
obf

ρ, inl(T ) −→ inl(p), inl(S)

γ, e ⇓ v, T
γ, inl(e) ⇓ inl(v), inl(T )

and suppose γ 0 w ρ is given, where γ 0 , inl(e) ⇓ v 0 , T 0 . By inversion, the derivation must have the form:
γ 0 , e ⇓ v00 , T00
γ , inl(e) ⇓ inl(v 0 ), inl(T00 )
0

obf

so v 0 = inl(v00 ) and T 0 = inl(T00 ). By induction we have ρ, T00 −→ p, S and p v v00 . So we can conclude:
obf

ρ, T 0 −→ p, S
obf

ρ, inl(T 0 ) −→ inl(p), inl(S)

inl(p) v inl(v00 )

• The case for inl(e) is symmetric.
• Suppose the derivations are of the form:
obf

obf

ρ, T −→ inl(p), S

ρ[x1 7→ p], T1 −→ p1 , S1
obf

ρ, case T .inl x1 .T1 −→ p1 , case S .inl x1 .S1
(inl(x1 ).e1 ∈ m)
γ, e ⇓ inl(v), T
γ[x1 7→ v], e1 ⇓ v1 , T1
γ, case e of m ⇓ v1 , case T .inl x1 .T1
and suppose γ 0 w ρ is given, where γ 0 , case e of m ⇓ v 0 , T 0 . By inversion of this derivation, there are two
cases. If the derivation is of the form:
(inl(x1 ).e1 ∈ m)
γ 0 , e ⇓ inl(v00 ), T00
γ 0 [x1 7→ v00 ], e1 ⇓ v10 , T10
0
0
0
γ , case e of m ⇓ v1 , case T .inl x1 .T10
obf

then v 0 = v10 and T 0 = case T 0 .inl x1 .T10 . By induction, we have ρ, T00 −→ inl(p), S and inl(p) v inl(v00 ),
obf

so p v v00 and γ 0 [x 7→ v00 ] w ρ[x 7→ p]. Again by induction, we have ρ[x 7→ p], T10 −→ p1 , S1 where p1 v v10 .
So we can conclude:
obf

ρ, T 0 −→ inl(p), S

obf

ρ[x1 7→ p], T10 −→ p1 , S1
obf

ρ, case T 0 .inl x1 .T10 −→ p1 , case S .inl x1 .S1
50

p1 v v10

If the derivation of γ 0 , case e of m ⇓ v 0 , T 0 is of the form
(inr(x2 ).e2 ∈ m)
γ, e ⇓ inr(v), T
γ[x2 7→ v], e2 ⇓ v2 , T2
γ, case e of m ⇓ v2 , case T .inr x2 .T2
obf

then by induction we can derive ρ, T 0 −→ inl(p), S and inl(p) v inr(v00 ), which is absurd, so this case is
vacuous.
• Suppose the derivations are of the form:
obf

ρ, T −→ , S
obf

ρ, case T .inl x1 .T1 −→ , 

(inl(x1 ).e1 ∈ m)
γ, e ⇓ inl(v), T
γ[x1 7→ v], e1 ⇓ v1 , T1
γ, case e of m ⇓ v1 , case T .inl x1 .T1

and suppose γ 0 w ρ is given, where γ 0 , case e of m ⇓ v 0 , T 0 . By inversion of this derivation, there are two
cases. If the derivation is of the form:
(inl(x1 ).e1 ∈ m)
γ 0 , e ⇓ inl(v00 ), T00
γ 0 [x1 7→ v00 ], e1 ⇓ v10 , T10
0
0
0
γ , case e of m ⇓ v1 , case T .inl x1 .T10
obf

then v 0 = v10 and T 0 = case T 0 .inl x1 .T10 . By induction, we know that ρ, T00 −→ , S and  v inl(v00 ), so
we can conclude:
obf
ρ, T00 −→ , S
obf

ρ, case T00 .inl x1 .T10 −→ , 

 v v10

If the derivation of γ 0 , case e of m ⇓ v 0 , T 0 is of the form
(inr(x2 ).e2 ∈ m)
γ, e ⇓ inr(v00 ), T00
γ[x2 7→ v], e2 ⇓ v20 , T20
0
0
γ, case e of m ⇓ v2 , case T .inr x2 .T20
obf

then the same reasoning applies: by induction on the first subderivation we can obtain ρ, T00 −→ , S and
 v inr(v00 ), and conclude:
obf

ρ, T00 −→ , S
obf

ρ, case T00 .inr x1 .T10 −→ , 

 v v20

• The cases for case T .inr x2 .T2 are symmetric.
• If the derivations are of the form:
obf

ρ, T1 −→ hκ, ρ0 i, S1

obf

ρ, T2 −→ p2 , S2

obf

ρ0 [f 7→ hκ, ρ0 i, x 7→ p2 ], T −→ p, S

obf

ρ, (T1 T2 ) .κ f (x).T −→ p, (S1 S2 ) .κ f (x).S
γ, e1 ⇓ hκ, γ0 i, T1

(κ = f (x).e)
γ, e2 ⇓ v2 , T2
γ0 [f 7→ hκ, γ0 i, x 7→ v2 ], e ⇓ v, T
γ, (e1 e2 ) ⇓ v, (T1 T2 ) .κ f (x).T

then suppose γ 0 w ρ and γ 0 , (e1 e2 ) ⇓ v 0 , T 0 . Then by inversion the derivation must have the form:
γ 0 , e1 ⇓ hκ0 , γ00 i, T10

(κ0 = f (x).e0 )
γ 0 , e2 ⇓ v20 , T20
γ00 [f 7→ hκ0 , γ00 i, x 7→ v20 ], e0 ⇓ v 0 , T00
γ 0 , (e1 e2 ) ⇓ v 0 , (T10 T20 ) .κ0 f (x).T00
obf

so T 0 = (T10 T20 ) .κ0 f (x).T00 . By induction, we know that ρ, T10 −→ hκ, ρ0 i, S1 and hκ, ρ0 i v hκ0 , γ00 i, from
obf

which it follows that κ = κ0 and γ00 w ρ0 . Similarly, by induction we know that ρ, T20 −→ p2 , S2 . Furthermore,
51

note that ρ0 [f 7→ hκ, ρ0 i, x 7→ p2 ] v γ00 [f 7→ hκ, γ00 i, x 7→ v20 ], and since κ = κ0 , we have e = e0 so by
induction on the third subderivation we have
obf

ρ0 [f 7→ hκ, ρ0 i, x 7→ p2 ], T00 −→ p, S
and p v v 0 . To conclude, we have:
obf

obf

ρ, T10 −→ hκ, ρ0 i, S1

obf

ρ, T20 −→ p2 , S2

ρ0 [f 7→ hκ, ρ0 i, x 7→ p2 ], T00 −→ p, S

obf

ρ, (T10 T20 ) .κ f (x).T00 −→ p, (S1 S2 ) .κ f (x).S

p v v0

as desired.
• If the derivations are of the form:

obf

ρ, T1 −→ , S1
obf

ρ, (T1 T2 ) .κ f (x).T −→ , 
γ, e1 ⇓ hκ, γ0 i, T1

(κ = f (x).e)
γ, e2 ⇓ v2 , T2
γ0 [f 7→ hκ, γ0 i, x 7→ v2 ], e ⇓ v, T
γ, (e1 e2 ) ⇓ v, (T1 T2 ) .κ f (x).T

then suppose γ 0 w ρ and γ 0 , (e1 e2 ) ⇓ v 0 , T 0 . Then by inversion the derivation must have the form:
γ 0 , e1 ⇓ hκ0 , γ00 i, T10

(κ0 = f (x).e0 )
γ 0 , e2 ⇓ v20 , T20
γ00 [f 7→ hκ0 , γ00 i, x 7→ v20 ], e0 ⇓ v 0 , T00
γ 0 , (e1 e2 ) ⇓ v 0 , (T10 T20 ) .κ0 f (x).T00
obf

so T 0 = (T10 T20 ) .κ0 f (x).T00 . By induction, we know that ρ, T10 −→ , S1 and  v hκ0 , γ00 i. To conclude, we
have:
obf
ρ, T10 −→ , S1
obf

ρ, (T10 T20 ) .κ f (x).T00 −→ , 

 v v0

as desired.
• If the derivations are of the form:
obf

ρ, T −→ p, S
obf

ρ, roll(T ) −→ roll(p), roll(S)

γ, e ⇓ v, T
γ, roll(e) ⇓ roll(v), roll(T )

then let γ 0 w ρ be given, and assume γ 0 , roll(e) ⇓ v 0 , T 0 . By inversion the derivation must be of the form:
γ 0 , e ⇓ v00 , T00
γ 0 , roll(e) ⇓ roll(v00 ), roll(T00 )
obf

so by induction we have ρ, T00 −→ p, S and p v v00 . We can conclude that:
obf

ρ, T00 −→ p, S
obf

ρ, roll(T00 ) −→ roll(p), roll(S)

roll(p) v roll(v00 )

• If the derivations are of the form:
obf

ρ, T −→ roll(p), S
obf

ρ, unroll(T ) −→ p, unroll(S)

52

γ, e ⇓ roll(v), T
γ, unroll(e) ⇓ v, unroll(T )

then let γ 0 w ρ be given and assume γ 0 , unroll(e) ⇓ v 0 , T 0 . By inversion this derivation must be of the form:
γ 0 , e ⇓ roll(v 0 ), T00
γ 0 , unroll(e) ⇓ v 0 , unroll(T00 )
obf

so T 0 = unroll(T00 ). By induction we have that ρ, T00 −→ roll(p), S where roll(p) v roll(v 0 ), so we can
conclude:
obf
ρ, T00 −→ roll(p), S
obf

ρ, unroll(T00 ) −→ p, unroll(S)

p v v0

• If the derivations are of the form:
obf

ρ, T −→ , S

γ, e ⇓ roll(v), T
γ, unroll(e) ⇓ v, unroll(T )

obf

ρ, unroll(T ) −→ , 

then let γ 0 w ρ be given and assume γ 0 , unroll(e) ⇓ v 0 , T 0 . By inversion this derivation must be of the form:
γ 0 , e ⇓ roll(v 0 ), T00
γ , unroll(e) ⇓ v 0 , unroll(T00 )
0

obf

so T 0 = unroll(T00 ). By induction we have that ρ, T00 −→ , S where  v roll(v 0 ), so we can conclude:
obf

ρ, T00 −→ , S
obf

ρ, unroll(T00 ) −→ , 

53

 v v0

