Declassification Policy for Program Complexity Analysis

Emmanuel Hainry Bruce M. Kapron Jean-Yves Marion Romain Péchoux

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class $\FP$ of functions computable in polynomial time. These characterizations are also extensionally complete – they capture all functions – but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization.
To overcome this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving $\FP$-soundness and  capturing strictly more programs than existing noninterference-based systems.
We show the versatility of the approach:  it also provides a new characterization of the class $\BFF$ of second-order polynomial time  computable functions in a second-order imperative language, with first-order procedure calls.
Type inference is tractable: it can be done in polynomial time.

§ INTRODUCTION

§.§.§ Motivations.

Noninterference-based type disciplines have been applied to the field of static analysis to ensure complexity properties of programs (e.g., bounded runtime, bounded memory), noting that a stratification between iterable and not iterable data is key to preventing exponential behavior [26].
The main intuition is as follows: data on which it is safe to iterate cannot increase and are annotated with level $1$ and data that can increase with level $0$. A variable of level $0$ is not safe for iteration, i.e., it  cannot be used to control loops. Data can flow from $1$ to $0$, under the hypothesis that it is passed-by-value. Flows in the opposite direction are strictly prohibited.
Under a termination hypothesis, safety implies polynomial time soundness by ensuring  that the space of level $1$ data is polynomially bounded in the size of the program input.

This approach, also known as safe recursion, ramified recursion,  cons-free programs, or tiering, depends on the cornerstone works of [1, 24] that provided the first implicit characterizations of  (first-order) polynomial time $\FP$.
The methodology was also adapted not only to characterize polytime [21, 26, 2, 7] but also other well-known complexity classes, such as (first-order) polynomial space $\FPSPACE$ [21, 16], second-order polynomial time $\BFF$ [14], or probabilistic polynomial time $\PP$ [8].
The main advantage of the underlying type systems is the tractability of their type inference, which can be done in polynomial time. Consequently, it has led to practice-oriented extensions such as the development of type systems for Java programs to statically ensure that their heap and their stack have a polynomially bounded size or that their runtime is polynomially bounded [17, 19]. The software ComplexityParser introduced in [13] ensures this kind of property.

This main advantage also implies their main weakness: while these characterizations are sound and  extensionally complete, i.e., all functions of the target complexity class are captured, they are not  intensionally complete. This means that there exist false negatives, e.g., algorithms that run in polynomial time but are wrongly rejected. This incompleteness is no great surprise for the theoretician who knows, for example, that the set of programs running in polynomial time is not decidable (and in fact has been proven to be $\Sigma^0_2$-complete in [12]) and that a tractable characterization of FP must therefore reject some of these polytime programs.

Since then, a number of studies have sought to increase the expressive power of these characterizations. For example, [19] extended  levels to any positive integer and has program flows to pass-by-reference data by combining noninterference-based typing with shape-analysis.
Despite the extensions made to date, the restrictions encountered with the complexity framework can be too rigid, similar to the problems encountered with traditional information-flow security and privacy applications of noninterference [30, 4]. The security community has tried to solve this issue by introducing relaxed versions, as in [28, 31] which, in order to provide more expressive power allow some forms of information flow that violate the noninterference principle, by making it possible to release some information in a controlled way.
Such control takes the form of declassification or downgrading policies allowing for instance the publishing of  some part of the secret data. A classic example of declassification is hashing: a password is strictly private but its hash must be shared for password verification to work. Allowing intentional information release while avoiding attack vectors is a challenge that has been studied under various frameworks.
In this respect, [29] presents a list of principles that declassification should preserve and a taxonomy of those frameworks on what can be declassified, who may receive the declassified data, where declassification is allowed, and when, in the sense of how often, or under which complexity constraints.

A natural question, then, is whether similar declassification policies can be defined and implemented in the context of complexity analysis.
At present, the only declassification options under consideration are far too limited. [17] considered declassification outside loops. Hence only a constant number of declassifications can be performed at runtime.
In [26], declassification is a priori restricted to a given type level, à la [27].
In general, declassifying any predetermined finite number of times will be acceptable as it preserves polynomial soundness; but declassifying data in a loop can lead to exponential program behavior. Indeed, declassifying one single bit of data is not a big deal but repeating this process breaks polytime soundness.

[caption=exponential 1, captionpos=b, label=ex:exp1,numbers=none]
//x,y,z: unary

[caption=exponential 2, captionpos=b, label=ex:exp2,numbers=none]
//y: binary, x: bool

\begin{align*}
\quad &\text{level 0: increasing/noniterable}\\
&\text{level 1: nonincreasing/iterable}
\end{align*}

To illustrate the danger linked with declassification when trying to control polynomial complexity, let us introduce two code samples in Listings <ref> and <ref>, where the syntactic elements are annotated by their level as a superscript. Declassification is used as a primitive construct to raise data from $0$ to $1$.
The program of Listing <ref> typechecks wrt. a control-flow based policy with 2 levels but computes the exponential $y=2^x$ in unary, hence in exponential time. This illustrates why the addition of declassification should not be treated superficially at the risk of breaking polytime soundness.
Naively, we might think that it is enough to limit information leaks to a restricted number of bits to avoid such examples. This hope is dashed by the example of Listing <ref>, one single loop manipulating a binary number  where the declassification only leaks a boolean value:
this loop explores all integers smaller than y, hence is exponential in the size of y.

There is therefore a need not only to develop declassification techniques that preserve the soundness of noninterference policies for complexity analysis, but also to demonstrate that they can be used to drastically increase the expressive power of these methods.

§.§.§ Contributions.

We introduce a new declassification policy for complexity analysis.
This policy preserves polynomial time soundness and answers a question already posed in [26] for having a more general form of declassification.
This policy consists of two ingredients; a  operator and an aperiodicity condition.
Similarly to [28],  takes 2 arguments: the expression to declassify and an expression whose level will bound the level up to which the value will be declassified.
In effect, the declassified value loses some information as the output is a unary representation of the length of the first argument and is bounded in size by the length of the second argument.
The aperiodicity condition checks that loops do not encounter a configuration more than once, hence do not enter a periodic state.
This is necessary to prevent abuses such as in Listing <ref> above.
We can say that the declassification policy acts on the where dimension in the taxonomy of [29].
We illustrate the use of this declassifying policy and its tamed power in two programming languages:

* a simple imperative language with a while loop construct,

* a programming language with second-order imperative procedures.

The declassification policy is expressed through a type system, which defines a safety property.
A safe program is a program that can be typed.
Additional properties are required to ensure polynomial time soundness: aperiodicity and, in the second-order case, termination. A program is aperiodic if in the guard of each while loop, no two equivalent states can be reached in (the depth of) the derivation tree; a program terminates if it halts on all inputs. Aperiodicity  implies termination on safe first-order programs and this explains why termination is only required for second-order programs.

The main contributions of this paper are:

* a new declassification policy (Figure <ref>), called safety,  for program complexity analysis, that corresponds to a partial release of information: only the length of data can be declassified. This policy extends the expressive power of previous work [26] by allowing to consider programs with restricted interference.

* a new characterization of the class of polytime computable functions $\FP$ that captures strictly more programs (like Example <ref>) than the ones implementing a strict noninterference policy. All functions in $\FP$ can be expressed by safe and aperiodic programs (Theorem <ref>) and, conversely, only polynomial time computable functions can be expressed this way (Theorem <ref>).

* a proof that safety is tractable: it can be decided in polynomial time (Theorem <ref>).

* a proof that aperiodicity is $\Pi^0_1$-complete (Theorem <ref>). Hence, aperiodicity is not more difficult than termination, known to be $\Pi^0_2$-complete [11], used as a condition in previous work [26]. Moreover, we show in Theorem <ref> that a decidable and completeness-preserving criterion trivially ensuring aperiodicity can be designed at the price of reduced expressive power. Consequently, our methodology is automatable.

* an application of the declassification policy: a new characterization of the class of second-order polytime computable functions $\BFF$ implementing the Strongly PolyTime ($\spt$) criterion of [23]. In this setting, safety remains tractable (Theorem <ref>) and aperiodicity is $\Pi^0_1$-hard (Corollary <ref>).

§.§.§ Application example of the declassification policy.

One of the latest characterizations of $\BFF$, introduced in [23], cannot be obtained without declassification. $\spt$ is defined as the class of second-order functionals computable by an oracle Turing machine with

* Polynomial Step Count: the machine works in time polynomial in the size of the input and the maximum size of an oracle answer,

* Finite Length Revision: there exists a natural number $n$ s.t. for any oracle and any input, in the run of the machine, it happens at most $n$ times that an oracle answer has size that exceeds the size of all previous answers.

The class of functionals  with polynomial step counts is named $\opt$ (for Oracle Polynomial Time, see [5]), and the class of functionals with finite length revision is named $\flr$. By definition, $\spt = \opt \cap \flr$. Let $\lambda(X)_2$ be the restriction to second-order functions of the simply-typed lambda-closure of terms with constants in the set $X$. The class $\BFF$ can be recovered from $\spt$ as follows:

$\lambda(\spt)_2 =  \BFF$.

As the above characterization relies on a purely semantic criterion ($\flr$) and only deals with machines, it was an open issue to know to what extent a similar and tractable characterization of $\BFF$ could be obtained for a programming language using noninterference-based analysis.  However this issue cannot be resolved in a strictly noninterfering system for the simple reason that $\spt$ needs interferences. Indeed, in the definition of $\flr$ the control flow needs to be guarded by the oracle answers (or at least a counter that keeps information on the number $n$ of times an answer size has exceeded the size of all previous answer). Hence the loop can be controlled by increasing data (oracle answers are not known in advance and cannot be trusted), which breaks noninterference.
In other words, since in $\spt$, it is the number of increases for the outputs of oracles that needs to be observed,
those outputs need to be declassified in order to manage the control flow.
Therefore, an application of interest is whether declassification techniques could help in capturing the
$\spt$ characterization. We give a positive answer to this question in the paper.

§.§.§ Related work.

Our results build upon work on declassification, noninterference type-based approaches in implicit computational complexity, and $\BFF$ characterizations.
The typing system we define has roots in [30] and the declassification policy was inspired from works on downgrading, endorsement, and declassification [31, 25, 29, 32].
In contrast, our aim is to characterize tractable programs rather than prove security or confidentiality properties, which accounts for the additional restrictions of aperiodicity and termination.
On the other side, our framework provides the possibility of declassifying in a loop which is challenging when only partial release of data is allowed.
The implicit complexity line of work draws from  noninterference ideas applied  to  data ramification/safe recursion [1, 24] to characterize complexity classes such as $\FP$ or $\FPSPACE$, e.g., [26, 21].

In contrast to [5, 22, 6, 23], that study $\BFF$ on machines, the current work characterizes $\BFF$ in the setting of programming languages. Hence it follows the approach of [20, 10] but differs from the latter in the sense that the bounds do not need to be explicitly provided in the language. This work is also linked to higher-order complexity analysis based on costs and potentials of [9], although the theoretical and practical objectives differ.
[14, 15] provide characterizations of $\BFF$ based on another noninterfering criterion (called $\mpt$ in [23]) and, hence, do not capture algorithmic schemes based on $\spt$. Several work [18, 3] have designed alternative elegant characterizations of $\BFF$ using higher-order polynomial interpretations. However, contrarily to safety, these interpretation methods are not tractable.

\[
\begin{array}{rrcl}
\texttt{Expr} & \e   & := &  \x\ |\ \op(\bar{\e})\ |\ \declass(\e, \e) \\
\texttt{Stmt} & \cmd & := & \skp\ |\ \x \asg \e\ |\ \cmd \sep \cmd\ \ | \  \ifar{\e}{\cmd}{\cmd}\ |\ \\
& & & \whar{\e}{\cmd}\ |\ \brar{\e} \\
\texttt{Prg} & \prog & := & \main(\bar{\x})\{\cmd\ \ret \x\}
\end{array}\]

§ DECLASSIFYING POLICY FOR COMPLEXITY

In this section, we show how declassification for complexity analysis can be adapted to a simple imperative programming language.

§.§ Imperative Language with Declassification

§.§.§ Syntax.

The syntax of the considered imperative language is provided  in Figure <ref>, where $\x$ is a variable in a fixed set of variables $\Var$ and where $\bar{\e}$ (resp: $\bar{\x}$) represents a finite sequence of expressions (resp: variables). Let $\ell(\bar{\x})$ be the length of the sequence $\bar{\x}$.

Operators $\op$ are basic operations of fixed arity $ar(\op)$ in the set $\Operator$. We assume that $\Operator$ includes some basic boolean and arithmetic operators such as  $\{=, <, \leq, 0, +1, -1, \non, \et, \ou\}$. Any constant can be viewed as an operator of arity $0$.

An expression $\e$ can be a variable $\x$, an operator application $\op(\bar{\e})$ or the result of a declassification $\declass(\e_1, \e_2)$. Operators will be used in infix, postfix, or prefix notations and they will always be fully applied, i.e., in $\op(\bar{\e})$, it always holds that $\ell(\bar{\e})=ar(\op)$.
We will say that an expression is declassified, if it appears as a subexpression of some $\e_1$ in $\declass(\e_1,\e_2)$.

Statements in Stmt are standard imperative constructs with assignments, conditionals, loops, and breaks.

Finally, a program takes a list of parameter variables $\bar{\x}$, executes a (body) statement $\body(\prog) \triangleq \cmd$, and returns one output variable $\x$.

In Listing <ref>, we have implemented bubble sort of a string with some type annotations as superscript. Bubble uses the following arity-2 operators:  to append a character to a string,  to compare two characters,  and  to get respectively the first character and the rest of the string. An explicit call to $\declass$ is performed on line $14$ inside a loop and we will see shortly (see Example <ref>) that the program cannot type without this feature. Such a program cannot be typed through the discipline of [26, 17].

\[
\begin{prooftree}
\hypo{\phantom{(\store, \overline{\e}) \toe \overline{\w}}}
\infer1{(\store, \x) \toe \store(\x)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \overline{\e}) \toe \overline{\w}}
\infer1{(\store, \op(\overline{\e})) \toe \sem{\op}(\overline{\w})}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \e_1) \toe \w_1}
\hypo{(\store, \e_2) \toe \w_2}
\infer2{(\store, \declass(\e_1, \e_2)) \toe 1^{\min(|\w_1|, |\w_2|)}}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\phantom{(\store, \e_i) \toe \w_1}}
\infer1{(\store, \skp) \tos (\top, \store)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \e) \toe \w}
\infer1{(\store, \x \asg \e)\tos (\top, \store[\x \lar \w])}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\store, \cmd_1)\tos(\top, \store')}
\hypo{(\store', \cmd_2)\tos(\square, \store'')}
\infer2[($\square \in \{\top,\bot\}$)]{(\store, \cmd_1 \sep \cmd_2) \tos (\square, \store'')}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \cmd_1)\tos(\bot, \store')}
\infer1{(\store, \cmd_1 \sep \cmd_2) \tos (\bot, \store')}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\store, \e) \toe \w}
\hypo{(\store, \cmd_{\w}) \tos (\square, \store')}
\infer2[($\square \in \{\top,\bot\}, \w \in \{\underline{\false}, \true\}$)]{\ifar{\e}{\cmd_{\true}}{\cmd_{\underline{\false}}} \tos (\square, \store')}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \e) \toe \underline{\false}}
\infer1{(\store, \whar{\e}{\cmd}) \tos (\top, \store)}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\store, \e) \toe \true}
\hypo{(\store, \cmd \sep \whar{\e}{\cmd}) \tos (\square, \store')}
\infer2[($\square \in \{\top,\bot\}$)]{(\store, \whar{\e}{\cmd}) \tos (\top, \store')}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\store, \e) \toe \underline{\false}}
\infer1{(\store, \brar{\e}) \tos (\top, \store)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\store, \e) \toe \true}
\infer1{(\store, \brar{\e}) \tos (\bot, \store)}
\end{prooftree}
\]

[basicstyle=,linewidth=0.92, caption= Bubble sort, label=bubble, captionpos=b,float=h,belowcaptionskip=-21pt]
$\while$(list1$^1$ $\neq$ $\epsilon$)
$\while$(len1$^1$ > 0)
$\ifa$(x < y)$^0$

§.§.§ Semantics.
Let $\W\triangleq \Sigma^{*}$ be the set of words, also called values, over the finite alphabet $\Sigma$ such that $\{0, 1\} \subseteq \Sigma$.
$\epsilon$ denotes the empty word; $\v\cdot\w$ denotes the concatenation of words $\v$ and $$; for $n ∈ℕ$, $^̌n$ is defined inductively as $^̌0≜ϵ$ and $^̌n+1≜·̌^̌n$.
Let $$ be the sub-word relation defined by $$ if there exist words $$̆ and $\u'$ such that $\w=\u\cdot\v\cdot\u'$.
The size of word $\w$ is denoted by $|\w|$.

The semantics assigns a total function $\sem{op}: \W^{ar(\op)}\to \W$  to each operator $\op\in\Operator$.
For example, $+1$ and $-1$ are operators on unary numbers, computing increment $\sem{+1} : \W \to \W$ and decrement $\sem{-1}:\W \to \W$ , respectively,  and outputting $\epsilon$ in case of failure (if the input word is not a unary number). I.e., for $n \in \mathbb{N}$, $\sem{+1}(1^n)\triangleq 1^{n+1}$ and $\sem{+1}(\w)\triangleq \epsilon$, if $\w \neq 1^n$.
The output of Boolean operators is either false ($0$) or true ($1$).
By extension, any value that is not $\true$, including $\epsilon$, will be denoted by $\underline{\false}$ and considered as false.
The semantics assigned to comparison operators is the standard shortlex order.

A memory store $\store\in\texttt{Stores}$ is a total map from variables in $\Var$ to values in $\W$.
Let $dom(\store)$ be the domain of the store $\store$.
Given $\x \in \Var$, and a value $\w\in\W$, let $\store[\x \leftarrow \w]$ denote the store obtained from $\store$ by updating the value of $\x$ to $\w$.
This notation is extended naturally to sequences $\store[\bar{\x} \leftarrow \bar{\w}]$, whenever $\ell(\bar{\x})=\ell(\bar{\w})$.
Finally, let $\store_\emptyset$ denote the empty store, mapping each variable to $\epsilon$.

The operational semantics is described in Figure <ref> as a standard big-step semantics with control flow breaks.
The semantics of expressions and statements are defined by the maps

\begin{align*}
\toe &: (\texttt{Stores}\times\texttt{Expr}) \to \W \\
\tos &: (\texttt{Stores} \times \texttt{Stmt})\to (\{\top, \bot\}\times\texttt{Stores}).
\end{align*}

Evaluating a $\declass(\e_1,\e_2)$ yields the value $1^{\min(|\w_{1}\!|, |\w_2\!|)}$, provided that $\e_i$ evaluates to the value $\w_i$, for $i \in \{1,2\}$.
Though this evaluation treats both operands symmetrically, as we will see shortly, the first operand $\e_1$ is the one to declassify and the second operand $\e_2$ bounds the length that is transmitted.
When evaluating a guard expression $\e$, assumed to evaluate to a boolean, we write $(\store, \e) \toe \underline{\false}$ to denote that $(\store, \e) \toe \w$ with $\w \neq \true$.

The first component in the codomain of $\tos$ is a flag encoding whether the flow has to be broken ($\bot$) or not ($\top$).
In rules describing the semantics of a sequence $\cmd_1\sep \cmd_2$, it is implicitly assumed that $\cmd_1 \neq \cmd'_1 \sep \cmd''_1$.

For a configuration $c \in ({\tt Stores} \times {\tt Stmt}) \cup (\texttt{Stores}\times\texttt{Expr})$, let $\pi_c$ be the (evaluation) tree with root $c$ obtained by evaluating $c$ using the rules of Figure <ref>. $\pi_c$ can be infinite if the program does not terminate.
We write $\pi_c \sqsubseteq \pi_{c'}$ (resp. $\pi_c \sqsubset \pi_{c'}$) when $\pi_c$ is a (strict) subtree of $\pi_{c'}$.

\[
\begin{prooftree}
\hypo{\typenv(\x)=\sla}
\infer1[(VAR)]{\pbl \x: \sla}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\sla_1 \to \cdots \to \sla_{ar(\op)+1} \in \Delta(\op)(\slain, \slaout)}
\hypo{\forall i \leq ar(\op),\ \pbl \e_i: \sla_i}
\infer2[(OP)]{\pbl \op(\bar{\e}): \sla_{ar(\op)+1} }
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\pbl \e_1: \sla_1}
\hypo{\pbl \e_2: \slaout}
\hypo{\sla_1 \ord \sla \ord \slaout}
\infer3[(DCL)]{\pbl  \declass(\e_1,\e_2): \sla}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\pbl  \cmd\ : \sla_1}
\hypo{\sla_1 \leq \sla_2}
\infer2[(SUB)]{\pbl  \cmd\ : \sla_2}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\phantom{\pbl  \cmd\ : \slb}}
\infer1[(SKP)]{\pbl \skp\ : \levela}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\typenv(\x)= \sla_1}
\hypo{\pbl \e: \sla_2}
\hypo{(\slaout = \levela) \vee (\sla_1  \ord \sla_2)}
\infer3[(ASG)]{\pbl \x \asg \e \ : \sla_1}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\pbl  \cmd_1 :\sla}
\hypo{\pbl \cmd_2:\sla}
\infer2[(SEQ)]{\pbl \cmd_1 \sep \cmd_2 \ :\sla}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\pbl \e: \sla}
\hypo{\pbl \cmd_{\true}: \sla}
\hypo{\pbl \cmd_{\false}:\sla}
\infer3[(CND)]{\pbl \ifa (\e) \{\cmd_{\true}\} \elsea \{\cmd_{\false}\}\ :\sla}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\typenv,\typop \vdash^\sla_{\slaout} \e: \sla}
\hypo{\typenv,\typop \vdash^\sla_{\slaout} \cmd : \sla}
\hypo{\levelb \ord \sla \ord \slaout}
\infer3[(WH)]{\pbl  \while (\e) \{\cmd\}\ :\sla}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\typenv,\typop \vdash^{\sla}_\sla \e: \sla}
\hypo{\typenv,\typop \vdash^\sla_\sla \cmd : \sla}
\hypo{\levelb \ord \sla}
\infer3[(WI)]{\typenv,\typop \vdash^{\levela}_\levela  \while (\e) \{\cmd\}\ :\sla}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\pbl \e  : \sla}
\hypo{ \slain \ord \sla}
\infer2[(BRK)]{\pbl \brk(\e)  : \slain}
\end{prooftree}
\]

Level-based typing rules

§.§.§ Restriction on Operators.

Following [26], we define three classes of operators called neutral, positive, and polynomial depending on the total function they compute.
This classification of operators will be used by the type system as the admissible types for operators will depend on their category.

An operator $\op \in \Operator$ of arity $k$ is:

–neutral if:
1) either $\sem{\op} \in \W^{k} \to \{\false, \true\}$,

–neutral if: 2) or  $\exists i  \leq k,\ \forall \bar{\w} \in \W^{k},\ \sem{\op}(\bar{\w}) \dord {\w_i}$;

– positive if $\exists c_{\op} \in \mathbb{N}, \ \forall \bar{\w} \in \W^{k},\ \size{\sem{\op}(\bar{\w})}  \leq \max_i \size{\w_i} + c_{\op}

–polynomial if $ \exists P \in \mathbb{N}[X],\
\forall \bar{\w} \in \W^{k},\ \size{\sem{\op}(\bar{\w})}  \leq P(\max_i \size{\w_i})

The basic intuition behind this classification is that neutral operators are iterable; positive operators are polynomially iterable; and polynomial operators are not iterable. Each operator that does not fall in these categories will be rejected by the type system.
A neutral operator is always positive and a positive operator is always polynomial but the converse properties are not true.
In the sequel, we reserve the name positive (resp. polynomial) for those operators that are positive but not neutral (resp. polynomial but not positive).

In Listing <ref>, operators $\neq$, $>$, $<$ compute boolean predicates, hence they are neutral.
, , and $-1$ (unary) are subword operations, as such, they are neutral.
$+1$ adds one character, it is hence a positive operator (with $c_{+1}$ equal to $1$).
The $+$ operator (line 26) takes a word $\w \in \W$ and a character $a \in \Sigma$ and outputs the word $\w\cdot a$, it is hence a positive operator as $\size{\w\cdot a}=\size{\w}+1$.

§.§ Type System and Safe Programs

We now describe the type discipline implementing the noninterference policy with declassification.

§.§.§ Levels and Typing Environments.

Levels are types that belong to the set of non-negative integers $ \SL$. Let $\ord$ (resp. $\ordst$) be the standard (strict) order on $\SL$ and let $\join$ and $\meet$ denote the max and min of a set of integers.
Variables $\sla,\sla',\tau_1,\ldots$ will be used to denote levels.
Variables $\slain$ and $\slaout$ will be used to denote the innermost and outermost levels.
The innermost (resp. outermost) level is the level of the innermost (resp. outermost) while loop under consideration. Outside of loops, $\slain$ and $\slaout$ are set to $\levela$.
In essence, the outermost level $\slaout$ will be used to restrict declassification, whereas the innermost level $\slain$ will restrict the type of the admissible operators in the corresponding statement.

An operator $\op$ will be associated to functional levels of the shape $\sla_1 \to \ldots \to \sla_{ar(\op)+1}$. They can be viewed as a tuples in $\SL^{ar(\op)+1}$.

The type system uses two kinds of typing environments:

* a variable typing environment $\typenv$ is a finite maps in $\Var \to \SL$;

* an operator typing environment $\typop$ maps each operator $\op \in \Operator$ to a finite map $\Delta(\op) \in \SL^2 \to\mathcal{P}(\SL^{ar(\op)+1})$.

Intuitively, given an operator $\op$ applied in a context of  innermost level $\slain\in \SL$ and an outermost level $\slaout \in \SL$, $\typop(\op)(\slain,\slaout)$ is the set of functional levels of the shape $\sla_1 \to \ldots \to \sla_{ar(\op)+1}$ that are admissible in the caller context. See Example <ref> for an illustrating use of typing environments.
Given a typing environment $\typenv$ (resp. $\typop$), $\dom(\typenv)$ (resp. $\dom(\typop)$) denotes the domain of $\typenv$ (resp. $\typop$).

§.§.§ Typing Judgments and Typing Rules.
Expression/Statement typing judgments are of the shape $\pbl b : \sla$, with $b \in {\tt Expr} \cup {\tt Stmt}$.
The meaning is that under the innermost level $\slain$ and the outermost level $\slaout$, the level of $b$ is $\sla$.

The typing rules are detailed in Figure <ref>.
Rule (OP) restricts the functional levels of the operator depending on the current innermost and outermost levels.
Rule (DCL) gives the possibility of declassifying the value of an expression of level $\sla_1$ to any level less or equal to $\slaout$.
As we have seen in the semantics, the value $\e_1$ is not declassified as is, only its length (in unary) is transmitted and the $\slaout$ compatibility is ensured by bounding this value by the second argument $\e_2$.
Those constraints will ensure that the set of possible values for variables of level $\slaout$ will not be exponential in their size.
In effect, it prevents the first dangerous code sample of Listing <ref> in the introduction.
The other rules enforce the noninterference discipline, preventing data to flow from a lower level to a strictly higher level inside loops.
Notice that it is possible to subtype statements, that is consider them to be of higher level.
On the other hand, inside a loop (i.e.,  when  $\slaout \neq \levela$), it is possible to put values of higher level into variables of lower level in Rule (ASG). This is the reason why we do not explicitly add subtyping for expressions. Notice that there are no constraints on flows outside loops (when $\slaout= \levela$) as there are no complexity concerns.
Rule (WI) sets the innermost and outermost levels $\slain$ and $\slaout$ of an outermost while loop, rule (WH) propagates the outermost level $\slaout$ and sets the new innermost level $\slain$ for nested loops.
Rule (BRK) requires  a break statement to be controlled by an expression of level at least $\slain$ to enforce the noninterference policy.

§.§.§ Safe Programs.

To ensure soundness, we put restrictions on admissible operator types, depending on their computational power.

An operator typing environment $\typop$ is safe if for each $\op \in \dom(\typop)$, $\op$ is either neutral, positive, or polynomial, $\sem{\op}$ is a polynomial time computable function, and for each $(\sla_{in},\sla_{out}) \in \SL^2$, and each $\sla_1 \to \ldots \to \sla_{ar(\op)+1} \in \typop(\op)(\sla_{in},\sla_{out})$, it holds that:

* if $\op$ is a neutral operator then
$\sla_{ar(\op)+1} \ord \meet_{i=1}^{ar(\op)} \sla_i$;

* if $\op$ is a positive operator then
$\sla_{ar(\op)+1} \ord \meet_{i=1}^{ar(\op)} \sla_i$  and either $\sla_{ar(\op)+1} \ordst \slain$ or $\sla_{ar(\op)+1} = \levela$;

* if $\op$ is a polynomial operator then $\slaout=\levela$.

The intuition is as follows. An operator typing environment is safe if the flow cannot go in the wrong direction for neutral and positive operators ($\sla_{ar(\op)+1} \ord \meet_{i=1}^{ar(\op)} \sla_i$); for positive operators, the computed output cannot be reused in the calling loop ($\sla_{ar(\op)+1} \ordst \slain$ or $\sla_{ar(\op)+1} = \levela$); for polynomial operators, the outermost level is enforced to be $\levela$. Hence, it is not called in a loop.

\[\scalebox{1}{\begin{prooftree}
\hypo{\typenv(\mathtt{len1})=\levelb}
\hypo{\typenv(\mathtt{len})=\levela}
\infer1[(VAR)]{\typenv, \typop \vdash_{\levela}^{\levela}\mathtt{len}:\levela}
\infer2[(ASG)]{\typenv, \typop \vdash_{\levela}^{\levela}\mathtt{len1}\asg\mathtt{len}:\levelb}
\hypo{\levelb\to\levelb \in \typop(>\levela)(\levelb, \levelb)}
\hypo{\typenv(\mathtt{len1})=\levelb}
\infer1[(VAR)]{\typenv, \typop\vdash_{\levelb}^{\levelb}\mathtt{len1}:\levelb}
\infer2[(OP)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\mathtt{len1}>0:\levelb}
\hypo{\romanoframedeux{$\rho$}}
%\infer1[(SEQ)]{\typenv, \typop\vdash_{\levelb}^{\levelb}\cmd 1 : \levelb}
\infer2[(WI)]{\typenv, \typop\vdash_{\levela}^{\levela}\whar{\mathtt{len1}>0}{\cmd 1}:\levelb}
\infer2[(SEQ)]{\typenv, \typop \vdash_{\levela}^{\levela}\mathtt{len1}\asg\mathtt{len}\sep\whar{\mathtt{len1}>0}{\cmd 1}: \levelb}
\end{prooftree}}\]

\[\rho \triangleq \romanoframe{\scalebox{0.87}{\begin{prooftree}
\hypo{\vdots}
\hypo{\typenv(\mathtt{len2})=\levelb}
\hypo{\typenv(\mathtt{len})=\levela}
\infer1[(VAR)]{\typenv, \typop\vdash_{\levelb}^{\levelb}\mathtt{len}:\levela}
\hypo{\typenv(\mathtt{list})=\levelb}
\infer1[(VAR)]{\typenv, \typop\vdash_{\levelb}^{\levelb}\mathtt{list}:\levelb}
\infer2[(DCL)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\declass(\mathtt{len},\mathtt{list}):\levelb}
\infer2[(ASG)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\mathtt{len2}\asg\declass(\mathtt{len}, \mathtt{list}):\levelb}
\hypo{\vdots}
\hypo{\vdots}
\infer2[(WH)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\whar{...}{...}:\levelb}
\infer2[(SEQ)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\mathtt{len2}\asg\declass(\mathtt{len},\mathtt{list})\sep\whar{\ldots}{\ldots}:\levelb}
\infer1[(SEQ)]{\ldots}
\infer2[(SEQ)]{\typenv, \typop \vdash_{\levelb}^{\levelb}\cmd 1
\end{prooftree}}}\]

Typing derivation of program bubble (Listing <ref>)

Given a safe operator typing environment $\typop$, a program $\prog$ is $\typop$safe if there are a level $\sla$, a variable typing environment $\typenv$ such that  $\typenv, \typop \vdash_{\levela}^{\levela} \body(\prog): \sla$ holds. Let $\typop\saf$ be the set of $\typop$safe programs.

A program $\prog$ is safe if there exists a safe operator typing environment $\typop$ such that $\prog$ is $\typop$safe.
Let $\saf$ be the set of safe programs.

The  program from Listing <ref> can be typed with $\typenv,\typop$ such that $\typenv(\texttt{list})=\typenv(\texttt{list1})=\typenv(\texttt{len1})=\typenv(\texttt{len2})=\levelb$ and $\typenv(\texttt{list2})=\typenv(\texttt{len})=\typenv(\texttt{x})=\typenv(\texttt{y})=\typenv(\texttt{r})=\levela$, and

\{\levelb\to\levelb\to\levelb\} & \subset& \typop(=)(\levelb,\levelb)\cap\typop(>)(\levelb,\levelb)\cap \typop(\neq)(\levelb,\levelb),\\
\{\levelb\to\levelb\}          & \subset& \typop(\texttt{tl})(\levelb,\levelb)\cap\typop(-\levelb)(\levelb,\levelb),\\
\{\levela\to\levela\to\levela\} & \subset& \typop(+)(\levelb,\levelb),\\
\{\levela\to\levela\}          & \subset& \typop(+\levelb)(\levelb,\levelb)\cap\typop(\texttt{hd})(\levelb,\levelb)\cap\typop(\texttt{tl})(\levelb,\levelb).
%\{\levela \to \levelb\}        & \subset& \typop(\texttt{copy})(\levela, \levela).
\end{array}$$

is safe:
its typing derivation tree is sampled in Figure <ref>, presenting the typing of the main loop preceded by the assignment of its guard variable . In Figure <ref>, the statement $\cmd_1$ is the body of the loop (line 11-28 in Listing <ref>). In Listing <ref>, we have also provided the typing of each expression as superscript notations.

§.§ Aperiodicity

Safety is not enough on its own to ensure polytime  soundness since the declassification of one bit of information in a loop can lead to an exponential behavior as illustrated by the example of Listing <ref>.
In order to avoid this phenomenon, we complement safety with a fairly simple and natural notion of aperiodicity.

Given an expression $\e$, we define the set of undeclassified variables of $\e$, ${U}(\e)$, by structural induction on expressions

\begin{align*}
{U}(\x)&\triangleq \{\x\},  & {U}(\op(\bar{\e}))&\triangleq \underset{i=1}{\overset{\ell(\bar\e)}{\cup}} {U}(\e_i), \\
{U}(\declass(\e_1, \e_2))&\triangleq  {U}(\e_2). && &
\end{align*}

Two stores $\store$ and $\store'$ are $\e$-equivalent, noted $\store \equiv_\e \store'$, if $\forall \x \in {U}(\e)$, $\store(\x)=\store'(\x)$.

A program $\prog$ is aperiodic if for each store $\store$ there are no $\pi_{(\store',\cmd')}$, $\pi_{(\store'',\cmd')}\sqsubseteq \pi_{(\store,\body(\prog))}$, such that

\[
\cmd' = \whar{\e}{\cmd''},\quad \pi_{(\store'',\cmd')}   \sqsubset  \pi_{(\store',\cmd')},\quad \text{and}\qquad \store' \equiv_\e \store''.
\]

Let $\ap$ be the set of aperiodic programs.

In other words, for any input store of an aperiodic program, there cannot be a subtree of root $(\store',\whar{\e}{\cmd''})$ with a strict subtree of root $(\store'',\whar{\e}{\cmd''})$ such that the stores $\store'$ and $\store''$ match on undeclassified variables.
Hence, this notion of aperiodicity is very natural as it means that a given while loop is never evaluated twice under ($\e$-)equivalent stores.
Declassified variables in $\e$ are treated differently as the domain of their value is bounded by the declassification semantics.
Hence there is no need to require aperiodicity on them for the result to hold. This can be done, but it would reduce the expressive power of the analysis.

Consider the dangerous code sample from Listing <ref> in the introduction. This program is safe by taking the variable typing environment $\typenv$ defined by $\typenv(\x)\triangleq \levelb$ and $\typenv(\y)\triangleq \levela$.
However, it is not aperiodic as the undeclassified $\x$ will have value $1$ more than once in the guard of line 3.

The program  of Listing <ref> is aperiodic.

§.§ Properties of Safe and Aperiodic Programs

§.§.§ Polytime Soundness and Completeness.

A program $\prog$ of the shape $\main(\bar{\x})\{\cmd\ \ret \y\}$ computes a partial function $\sem{\prog}: \W^{\ell(\bar{\x})} \to \W$ defined as

\[
\sem{\prog}(\bar{\w}) = \v\text{ iff }(\store[\bar{x}\leftarrow\bar{\w}], \cmd) \toe (\top, \store')\text{ and }\store'(\y)=\v.
\]

If $\sem{\prog}$ is a total function, we say that the program is terminating. Let $\TERM$ be the set of terminating programs. Given a set of programs $S$, we define $\sem{S}$ by $\sem{S} \triangleq \{ \sem{\prog} \ | \ \prog \in S\}$.

We now show a completeness result stating that for each function $f$ in $\FP$, the class of functions computable in polynomial time by a Turing machine, there exists a safe and aperiodic program $\prog$ such that $f=\sem{\prog}$. This completeness result relies on simulating any Turing machine that halts in polynomial time with a safe and aperiodic terminating program.

$\FP \subseteq \sem{\saf \cap \ap}$.

For soundness, the intuition is as follows.
For a fixed loop of level $\sla$, the safety property implies a polynomial bound on the set of potentially computed values for variables of level greater than or equal to $\sla$.
Aperiodicity then makes it impossible to reach twice the same configuration of variables of level at least $\sla$.
Hence the number of iterations is polynomially bounded. Moreover, variables of strictly lower level can only increase polynomially by a constant (using positive operators). Repeating the reasoning for any level, the total runtime is polynomially bounded in the program input. This bound is obtained by a constant composition of polynomials.

$ \sem{\saf \cap \ap}\subseteq \FP $.

As a corollary, this implies termination. Indeed, on any input store, the space of reachable values (and hence reachable stores) corresponding to the program derivation tree is polynomially bounded.

$ \sem{\saf \cap \ap}\subsetneq \TERM $.

Safe and aperiodic programs contain polytime programs with loops guarded by data that may increase.
For example, the program $\tt bubble$ of Listing <ref> has an inner loop controlled by $\tt len2$, which is reinitialized at the size of $\tt len$ at each iteration of the outer loop.
Such programs cannot be captured by existing criteria, e.g., [26]. Consequently, this result improves greatly on the expressive power of noninterference-based type systems for complexity.

§.§.§ Complexity of Type Inference and Aperiodicity.

We now show that type inference can be decided in polynomial time in the size of a program $\size{\prog}$ (i.e., number of symbols) , which implies that type inference can be efficiently implemented.
[Type inference]theoremthmtiproc
Given a safe operator typing environment $\typop$, deciding whether $\prog \in \typop\saf$ can be done in time $\mathcal{O}(\size{\prog}^3)$.

Now we show that aperiodicity  is a $\Pi_1^0$-complete problem in the arithmetical hierarchy.

Deciding whether a program  $\prog$ is aperiodic (i.e., $\prog \in \ap$) is $\Pi^0_1$-complete.

This undecidability result is not a negative result as the set of programs in the class $\FP$ is known to be $\Sigma^0_2$-complete [12]. Hence aperiodicity is a strictly simpler problem. Moreover, the termination hypothesis in previous work (e.g.,  [26, 17]) is $\Pi^2_0$-complete ( [11]), thus strictly harder than aperiodicity as a consequence of Post's Theorem.

§.§.§ Sound and Complete Criterion with Decidable Aperiodicity.

Last but not least, it is possible to specify a decidable aperiodicity condition that preserves the completeness of Theorem <ref>.
We define a for loop statement $\ifor \x = \e \ito \d\ \{ \cmd \}$ as syntactic sugar for the statement $\x \asg \d \sep \while(\x \geq \e)\{\cmd \sep \x \asg \x -1\}$, under the proviso that $\x$ does not occur in $\cmd$.
Let $\emph{for-programs}$ be programs that only contains for loop (and no other while loop). For-programs are trivially aperiodic, by definition. Let $\forp$ be the set of for-programs.
We can show that safe for-programs are sound and complete for $\FP$.

$ \sem{\saf \cap \forp } =\FP$

Soundness and tractability of type inference are obtained as a direct corollary of Theorems <ref> and <ref> as for-programs are aperiodic programs. Completeness is also obtained easily as the programs used in the proof of Theorem <ref> are all for-programs.

§ APPLICATION EXAMPLE: CHARACTERIZING THE CLASS BFF

We now enrich the language introduced in Section <ref> with procedures,  oracle calls, and closures with the aim of characterizing the second-order complexity class of Basic Feasible Functionals, $\BFF$.
The language additions are minimal and aim at extending the language to second-order – a prerequisite to characterize $\BFF$ – and are in no way linked to noninterference or declassification issues.

§.§ Type-2 Programming Language

\begin{array}{llll}
\texttt{Expr}          \qquad & \e
& \rgl &\x
\ |\ \op(\bar{\e})  \ | \
\declass(\e,\e)\ | \   \X (\bar{\e}) \\
\texttt{Stmt}                  &  \cmd
& \rgl &\skp   \ | \  \x  \asg \e   \ | \  \cmd \sep \cmd \ |\  \ifa (\e) \{\cmd\} \elsea \{\cmd\} \ |\ \\
& &  &\while(\e)\{ \cmd \}  \ | \ \brk(\e)\\
\texttt{Proc}                & \procn    & \rgl & \proc(\bar{\X},\bar{\x})\{[\var \bar{\y}\sep\!\!]\ \cmd  \ \ret \x\} \\
\texttt{Terms}                 & \term   & \rgl & \x  \ | \   %\X \app {\term} \ | \
\callcc\proc(\bar{\clos},\bar{\term}) \\
\texttt{Closures}              & \clos   & \rgl & \X \ | \ \abs{\bar{\x}}.\term \\
\texttt{Prg}             & \prog
& \rgl &  \term \ | \ \letin{{\procn}} \prog \ | \ \boite{[\va]}{\prog}
\end{array}

Syntax of second-order programs

§.§.§ Syntax.

[basicstyle=,firstnumber=2,caption=Procedure , captionpos=b,  label=ex:J]
$\niceinstr{declare} \verb!J!$($\Y$,l,m,n)
$\var$b$\sep \var$t$\sep \var$z$\sep \var$l0$\sep\var$n0$\sep$

[basicstyle=,firstnumber=19, caption=Procedure , captionpos=b, label=ex:K]
$\niceinstr{declare} \verb!K!$($\X$,p,q,r,s)
$\var$i$\sep \var$j$\sep$

[basicstyle=,caption=Program ,label=fig:bruce,captionpos=b]
$\niceinstr{box}[\F,\text{u},\text{v},\text{w}]\ \niceinstr{in}$
$\niceinstr{declare} \verb!J!$($\Y$,l,m,n)... $\niceinstr{in}$
$\niceinstr{declare} \verb!K!$($\X$,p,q,r,s)... $\niceinstr{in}$
$\callcc \verb!J!$($\abs{\!\!\text{x},\!\text{y}}.\callcc \verb!K!$($\F$,v,w,x,y),u,v,w)

Programs are defined by the grammar of Figure <ref> and can be either a term, a procedure declaration within a program, or the declaration of a boxed variable, called box, followed by a program. Boxed variables represent program inputs and can be either order-$1$ upper-case variables $\X \in \Var_1$ or order-$0$ lower-case variables $\x \in \Var_0$. In a box, the variable $\va \in \Var \triangleq \Var_0 \uplus \Var_1$ can be of arbitrary order.

Terms $\term$ are order-$0$ constructs and can be either a variable $\x$
or a procedure call $\callcc\proc(\bar{\clos},\bar{\term})$ corresponding to the application of procedure of name $\proc$ to order-$1$ inputs $\bar{\clos}$ and order-$0$ inputs $\bar{\term}$.

A procedure declaration $\proc(\bar{\X},\bar{\x})\{[\var \bar{\y}\sep\!]\ \cmd  \ \ret \x\}$ is the corresponding order-2 abstraction. It maps order-$1$ and order-$0$ parameters $\param(\proc) \triangleq \{\bar{\X},\bar{\x}\}$ to a order-$0$ output $\x$ and consists of a body statement $\body(\proc)\triangleq \cmd $ with optional declaration of local variables $\local(\proc)\triangleq\{\bar{\y}\}$. For convenience, we identify a procedure declaration with its procedure name. Moreover, we assume that each order-$1$ procedure parameter comes with a fixed arity $ar(\X)$.

Statements are the same as in Figure <ref> and thus can still only assign to order-$0$ variables.
Similarly, expressions include those of Figure <ref> plus a new construct $\X(\bar{\e})$, named oracle call, consisting in the application of a order-$1$ variable $\X$ to some sequence of expressions $\bar{\e}$, called the input data. We assume that they are always fully applied, i.e., that $\ell(\bar{\e})=ar(\X)$.

Closures are order-$1$ abstractions corresponding to oracle calls and can be written
either as an order-$1$ variable $\X$ or
as $\abs{\bar{\x}}.\term$, where the order-$0$ term $\term$ may contain free variables. Notice that procedure calls can only take closures as order-$1$ parameters and that procedure declarations with no oracle call are exactly the first-order programs of Section <ref>.

A variable is free if it is neither boxed nor bound by one of the two possible abstractions.  A program is closed if it has no free variable.
We define the following syntactic sugar:

\begin{align*}
\letin{\bar{\procn}}\prog&\triangleq \letin{\procn_1}\ldots\letin{\procn_n}\prog\\
\boite{[\bar \va]}{\prog}&\triangleq \boite{[\bar \va_1]}{\ldots \boite{[\bar \va_m]}{\prog}}
\end{align*}

with $\bar{\procn} \triangleq \procn_1,\ldots,\procn_n$ and $\bar{\va}\triangleq \bar \va_1,\ldots,\bar\va_m$.

Throughout the rest of the paper, we will restrict attention to closed  programs in normal form. These consist of programs that can be written as follows $\boite{[\bar{\X},\bar{\x}]}{\letin{\bar{\procn}} \term},$
for some term $\term$ such that the following well-formedness conditions hold:

* no name clash: the set of the term free variables, each set of procedure parameters, and each set of procedure local variables are all pairwise distinct,

* closed procedures: each variable of a procedure body is either a procedure parameter or a local variable,

* determinism: each procedure name called in $\term$  is declared exactly once in $\procn$.

A program in normal form computes a second-order functional.

Program  in Listing <ref> is closed and in normal form and computes  a variant of Cook-Urquhart's second-order bounded iterator [6]

\begin{align*}
\mathcal{I}& :  (\W \to \W) \times \W^3 \to \W \\
\mathcal{I}(f,\u,\v,\w) &\triangleq (\lambda x.\!\! \upharpoonright\!\!(f(x),\v))^{\size{\w}}(\u),
\end{align*}

where $f^n$ is the $n$-iterate of $f$ and $\upharpoonright \ : \W \times \W \to \W$, defined by

\[
\upharpoonright\!\!(\v ,\w)\triangleq \begin{cases} \v &\text{if }\size{\v} \leq \size{\w} \\ \v' \text{ s.t. } \size{\v'} =\size{\w} \wedge \v =\v'\cdot\v'' & \text{otherwise,}\end{cases}
\]

is a function truncating its first operand with respect to the size of its second operand.

In this example, words can encode lists to represent pairs and triples. To account for this, the alphabet $\Sigma$ on which words are defined includes a constructor symbol $\#$ in addition to $1$ and $0$.
On boolean and arithmetic operators, the function $\sem{\op}$ behaves as expected on suitable data and returns the empty word $\epsilon$ in case of failure, e.g., $\sem{\sz}(100\#11)=110$, $\sem{\leq}(110,111)=1$, and $\sem{+1}(1\#0)=\epsilon$.
Constructor and destructor semantics function can be defined similarly: $\sem{\pair}(\u,\v)\triangleq  \u\cdot\#\cdot\v$, if $ # ∉$̆, $\sem{\pair}(\u,\v)\triangleq \epsilon$, otherwise,
$\sem{\gauche}(\sem{\pair(\u,\v)})\triangleq \u$ and $((,̆)̌ ) ≜$̌.
The operator $\pad$ is a padding operator defined by: $\sem{\pad}(\u,\v)\triangleq \sem{\pair(\v,0^n)}$, if $ \exists n \geq 0,\ \size{\v} + n+1 = \size{\u}$, and $\sem{\pad}(\u,\v)\triangleq \epsilon$, otherwise. We use this operator in procedure  to produce outputs of non-decreasing size (line 27).
Finally, the operator $\truncate$ is the syntactic counterpart of the function $\upharpoonright$ defined by $\sem{\truncate}(\v,\w) \triangleq \upharpoonright\!\!(\v ,\w)$ and is used in the two procedures to bound the oracle outputs.

Program   makes use of two intermediate procedures   and   defined in Listings <ref> and <ref>.   iterates at most $s$ times an oracle call $\X(\text{i})$ (hence computes $(\lambda x.\!\!\upharpoonright\!\!(f(x),\v))^{\size{s}}(\u)$), for some $s$ up to which $f$ outputs does not exceed the size of the first call to $f$. This check is performed using a break statement. Hence   computes a functional in $\flr$.  iterates $\size{\w}$ times , using a closure.

Procedure  uses the $\declass$ construct. This will be required for the program to type as, in the loop, the output of an oracle call is assigned to the variable  that guards the loop. In general, such behaviors will be prohibited as there may be exponentially many oracle calls  (even for a fixed size) unless an explicit declassification is performed. Here the declassification has the effect of restricting the output of the oracle call into a polynomially bounded domain.

\[\begin{prooftree}
\hypo{\phantom{ \Imp \x  \asg \e\to } }
\infer1[]{(\sigma,\store,\phi \Imp \x) \toexp \store(\x)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\sigma,\store,\phi,\bar{\e}) \toexp \bar{\w}}
\infer1[]{(\sigma,\store,\phi \Imp \op(\bar{\e})) \toexp \sem{\op}(\bar{\w})}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\forall i \leq 2, \ (\sigma,\store,\phi,\e_i) \toexp \w_i}
\infer1[]{(\sigma,\store,\phi \Imp \declass(\e_1,\e_2)) \toexp 1^{\min(|w_1|, |w_2|)}}
\end{prooftree}
\]

\[
\romanobox{
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \bar \e) \toexp {\bar \v}}
\hypo{\phi(\X)= \abs{\bar{\x}}.\term}
\hypo{(\sigma,\store[\bar{\x} \leftarrow  \bar{\v}],\term ) \toenv \w }
\infer3[(Orc)]{(\sigma,\store,\phi \Imp \X(\bar{\e})) \toexp \w}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{\phantom{ \Imp \x  \asg \e^O \to }  }
\infer1[]{(\sigma,\store,\phi \Imp \skp) \tost (\top,\store)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp \w }
\infer1[]{(\sigma,\store,\phi \Imp \x  \asg \e) \tost (\top, \store[\x  \leftarrow \w])}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \cmd_1) \tost (\bot,\store') }
\infer1[]{(\sigma,\store,\phi \Imp \cmd_1 \sep \cmd_2) \tost (\bot,\store')}
\end{prooftree}
\]

\[
\scalebox{0.9}{
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \cmd_1) \tost (\top,\store') }
\hypo{(\sigma,\store',\phi \Imp \cmd_2) \tost (\square,\store'')}
\infer2[($\square \in \{\top,\bot\}$)]{(\sigma,\store,\phi \Imp \cmd_1 \sep \cmd_2) \tost (\square,\store'')}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp \w}
\hypo{(\sigma,\store,\phi \Imp \cmd_\w) \tost (\square,\store')}
\infer2[($\square \in \{\top,\bot\}, \w \in \{\underline{\false},\true\}$)]{(\sigma,\store,\phi \Imp \ifa (\e) \{\cmd_{\true}\} \elsea \{\cmd_{\underline{\false}}\} ) \tost (\square,\store')}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp \underline{\false}}
\infer1[]{(\sigma,\store,\phi \Imp \while (\e) \{\cmd\}) \tost (\top, \store)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp \true}
\hypo{(\sigma,\store,\phi \Imp \cmd \sep  \while (\e) \{\cmd\}) \tost (\square,\store')}
\infer2[($\square \in \{\top,\bot\}$)]{(\sigma,\store,\phi \Imp  \while (\e) \{\cmd\}) \tost (\top,\store')}
\end{prooftree}
\]

\[
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp\underline{\false}}
\infer1[]{(\sigma,\store,\phi \Imp \brk(\e)) \tost (\top,\store)}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{(\sigma,\store,\phi \Imp \e) \toexp\true}
\infer1[]{(\sigma,\store,\phi \Imp \brk(\e)) \tost (\bot,\store)}
\end{prooftree}
\qquad
\romanobox{
\begin{prooftree}
\hypo{\phantom{(\sigma,\store)}}
\infer1[(Var)]{(\sigma,\store,\x) \toenv \store(\x)}
\end{prooftree}
%\hypo{(\sigma,\store,\term )\toenv \w}
%\infer1[(App)]{(\sigma,\store,\X \app \term) \toenv \store(\X)(\w)}
\]

\[
\romanobox{
\scalebox{1}{\begin{prooftree}
\hypo{\proc(\bar{\X},\bar{\x})\{ \cmd  \ \ret \z\}  \in \sigma}
\hypo{(\sigma,\store,\bar{\term}) \toenv \bar{\w}}
\hypo{(\sigma,\store[\bar{\x} \leftarrow \bar{\w},\bar{\y} \leftarrow \bar{\epsilon}],\bar{\X} \mapsto \bar{\clos},\cmd ) \tost (\square,\store') }
\infer3[($\square \in \{\top,\bot\}$)\ (Call)]{(\sigma,\store  \Imp \callcc \proc(\bar{\clos},\bar{\term})) \toenv \store'(\z)}
\end{prooftree}}
\]

\[
\romanobox{
\begin{prooftree}
\hypo{(\sigma\cup\{\procn\},\store,\prog) \toenv \w}
\infer1[(Dec)]{(\sigma,\store,\letin{\procn} \prog) \toenv \w}
\end{prooftree}
\qquad
\romanobox{
\begin{prooftree}
\hypo{(\sigma,\store,\prog) \toenv \w}
\infer1[(Box)]{(\sigma,\store,\boite{[\va]}{\prog}) \toenv \w}
\end{prooftree}
\]

Semantics of second-order programs

§.§.§ Operational Semantics.

In what follows, let $f,g,\ldots$ denote total functions in $\W \to \W$. Stores $\store$ and environments $\phi$ are defined by

\begin{align*}
&({\tt Stores})   &&\store \in (\Var_0 \to \W) \uplus   \Var_1 \to (\W \to \W)  \\
&({\tt Env})     &&\phi \in \Var_1 \to {\tt Closures}
\end{align*}

Stores are total functions assigning words or functions on words to a variable, depending on its order. Environments assign a closure to an order-1 variable $\X$.  Again, $\store_\emptyset$ will denote the empty store, mapping each order-$0$ variable $\x$ to $\varepsilon$ and each order-$1$ variable $\X$ to the constant function $\lambda \w.\varepsilon$. In the same vein, $\store[\bar{\x} \leftarrow \bar{\w},\bar{\X} \leftarrow \bar{f}]$
denotes a store update. We now introduce the following judgments

\begin{align*}
\toexp &\in (\mathcal{P}({\tt Proc}) \times {\tt Stores} \times {\tt Env} \times {\tt Expr}) \to \W \\
\tost &\in (\mathcal{P}({\tt Proc}) \times {\tt Stores} \times {\tt Env} \times {\tt Stmt}) \to (\{\top,\bot\} \times {\tt Stores}) \\
\toenv &\in (\mathcal{P}({\tt Proc}) \times {\tt Stores} \times {\tt Prg} ) \to \W
\end{align*}

The judgment $(\sigma,\store,\phi,\e) \toexp  \w$ means that the expression $\e$ evaluates to the word $\w \in \W$ wrt. the set of procedure declarations $\sigma$, the store $\store$, and the environment $\phi$.
The judgment $(\sigma,\store,\phi,\cmd) \tost (\square,\store')$, with $\square \in \{\top,\bot\}$, expresses that, under the set of procedure declarations $\sigma$, the store $\store$, and the environment $\phi$, the statement $\cmd$ terminates and outputs the store $\store'$. As in Section <ref>, the symbol $\bot$ indicates that a break instruction has been executed.
The judgment $(\sigma,\store,\prog)\toenv \w$ deterministically maps a set $\sigma$ of procedure declarations, a store $\store$, and a program $\prog$ in normal form to a word $\w \in \W$.

The operational semantics is defined in Figure <ref>. Most rules are very similar to that of Figure <ref>. The new rules, corresponding to the new syntactic constructs, are highlighted with boxes. We provide an intuition for each of them. Rule (Orc) deals with an oracle calls. The rules evaluates the order-$0$ term $\term$ of the closure $\abs{\bar \x}.\term$ corresponding to the order-$1$ variable $\X$ in the environment $\phi$ wrt. the values $\bar\v$ of the operands $\bar \e$.
Rule (Var) outputs the word $\store(\x)$
In Rule (Call),  $\bar{\X} \mapsto \bar{\clos}$, with $\ell(\bar{\X})=\ell(\bar{\clos})$, is the environment mapping each $\X_i \in \Var_1$ to the closure $\clos_i$. It is important to stress that Rule (Call) is the only rule that updates the environment to the closures passed as arguments: hence, oracle calls are fixed for each procedure call.
Rule (Dec) just adds the procedure declaration to the set of procedures in the judgments and Rule (Box) is just a no-op rule.

The notation $\pi_c$ is overloaded to denote the evaluation tree of root $c$ using the rules of Figure <ref>, with $c$ being an element in the definition domain of $\toexp$, $\tost$, or $\toenv$ and the strict subtree relation $\sqsubset$ is updated accordingly.

As we will see shortly, the type discipline will ensure that a  program $\prog= \boite{[\bar{\X} ,\bar{\x}]}{\letin{\bar{\procn}}\term}$ computes the second-order partial functional $\sem{\prog}$ in $(\W \to \W)^{\ell(\bar{\X})} \to \W^{\ell(\bar{\x})} \to \W,$
defined by:

\[
\sem{\prog}(\bar{f},\bar{\w})=w \text{ iff } (\emptyset, \store_\emptyset[\bar{\x} \leftarrow \bar{\w},\bar{\X} \leftarrow \bar{f}],\prog) \toenv  \w.
\]

The store $\store_\emptyset[\bar{\x} \leftarrow \bar{\w},\bar{\X} \leftarrow \bar{f}]$ is called an input store.
If $\sem{\prog}$ is a total function, the program $\prog$ is said to be terminating. Let $\SN$ be the set of terminating programs.

§.§ FLR Restrictions and Aperiodicity

§.§.§ Syntactic restrictions.

For showing soundness and completeness wrt $\BFF$, we need to put some restrictions and hypothesis on the programming language. First, we assume that the set of operators $\Operator$ includes all the operators $\{=, <, \leq, 0, +1, -1, \non, \et, \ou\}$ used in Section <ref> and all the operators defined in Example <ref>. Indeed, this example is used in the proof of completeness and, hence, it is important to include all its operators for completeness to hold. Now we syntactically restrict the study to guarded programs.

A program is guarded if

* oracle calls cannot be nested and appear either in assignments or in break statements $\brk(\size{\X(\bar{\e})}>\size{\X(\bar{\x})})$,

* in a loop, each assignment containing an oracle call $\X(\bar{\e})$ is preceded by a break statement $\brk(\size{\X(\bar{\e})}>\size{\X(\bar{\x})})$.

Guardedness just put simple syntactic restrictions on how oracle calls can be used in a program.
The intuition behind is to ensure the $\flr$ property, i.e., that size of oracle calls cannot increase more than a constant number of times during the program execution. The aim of item (<ref>) is to ensure $\flr$ by the increase of oracle outputs with a break statement before assigning them. The restriction of oracle calls to break statements and assignments (<ref>) avoids uncontrolled increases in other expressions of the program (guard of while, of conditionals, ...). However, this syntactic restriction is not sufficient on its own to ensure that programs compute a functional in $\flr$ (a fortiori in $\spt$). This property will be achieved by complementing the restriction by the typing discipline. In what follows, we will restrict our study to guarded programs.

Program  of Listing <ref> is guarded.
Indeed, the oracle calls line 10 in procedure  and at line 24 in procedure  are immediately preceded by a $\brk$ statement of the good shape (<ref>). Moreover, there are no other oracle calls in the program (<ref>).

§.§.§ Aperiodicity Revisited.

We lift the notion of aperiodicity introduced in Definition <ref> to this second-order programming language. The set of undeclassified variables of $\e$, ${U}(\e)$, is extended by

\[
{U}(\X(\bar{\e}))\triangleq \underset{i=1}{\overset{\ell(\bar\e)}{\cup}}{U}(\e_i),
\]

and the definition of $\equiv_\e$ is updated accordingly.

A program $\prog$ is II-aperiodic if, for each store $\store$, there are no $\pi_{(\sigma',\store',\phi',\cmd)}$ $\pi_{(\sigma'',\store'',\phi'',\cmd)}\sqsubseteq \pi_{(\emptyset,\store,\prog)}$ s.t.

\[
\cmd = \whar{\e}{\cmd'},\quad \pi_{(\sigma',\store',\phi',\cmd)} \sqsubset \pi_{(\sigma'',\store'',\phi'',\cmd)},\ \text{and}\quad  \store' \equiv_\e \store''.
\]

Let $\dap$ be the set of II-aperiodic programs.

II-aperiodicity is very similar to the notion of aperiodicity for first-order programs in Definition <ref>:
it still enforces that there cannot be two consecutive calls to a while loop of a given procedure under equivalent stores.

For a given set of programs $S$, let $\sem{S}\triangleq \{ \sem{\prog} \ | \ \prog \in S\}$ denote the set of functions computed by programs in $S$.  E.g., $\sem{\ASN}$ is the set of functions computed by aperiodic and terminating programs. In aperiodic and terminating programs, termination does not depend on the oracle output.

The program  of Listing <ref> is in $\SN$.
Indeed, procedure  trivially terminates on any input.
Moreover, when called on the appropriate closure (line 30 of Listing <ref>), procedure  assigns to  a value that has decreased by at least $1$ or that is equal to $0$ (line 8 of Listing <ref>).
Notice however that it does not entail that the procedures are terminating.
Indeed, procedure  only terminates on specific closures (including $\abs{\x,\y}.\callcc \verb!K!(\F,\variable{v},\variable{w},\x,\y)$).
Program  is also aperiodic: on any input store, in procedure , the value of variable  used in the guard of the loop  strictly decreases and, in procedure , the value of variable  used in the guard of the loop strictly decreases, as this procedure is called on the closure $\abs{\x,\y}.\callcc \verb!K!(\F,\variable{v},\variable{w},\x,\y)$.
We conclude that  $\in \ASN$.

As the proof of Theorem <ref> is only based on procedure bodies,  II-aperiodicity is also $\Pi_0^1$-hard and in $\Pi^1_1$.

Deciding whether a program $\prog$ is II-aperiodic (i.e., $\prog \in \dap$) is $\Pi^0_1$-hard.

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\typenv(\x)=\sla}
\infer1[%(VAR)
]{\pbl \x: \sla}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\sla_1 \to \cdots \to \sla_{ar(\op)+1} \in \Delta(\op)(\sla_{in},\sla_{out})}
\hypo{\forall i \leq ar(\op),\ \pbl \e_i: \sla_i}
\infer2[%(OP)
]{\pbl  \op(\bar{\e}): \sla_{ar(\op)+1+1} }
\end{prooftree}
\]

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\pbl \e_1: \sla_1}
\hypo{\pbl \e_2: \sla_{out}}
\hypo{\sla_1 \ord \sla\ord \sla_{out}}
\infer3[%(DCL)
]{\pbl  \declass(\e_1,\e_2): \sla}
\end{prooftree}
\qquad
%\hypo{\pbl \e_1: \sla_1}
%\hypo{\pbl \e_2: \sla_{out}}
%\hypo{\sla \ord \sla_1  \meet \sla_{in}}
%\infer3[(TR)]{\pbl  \truncate(\e_1,\e_2): \sla}
\scalebox{1}{\romanobox{\begin{prooftree}
\hypo{\forall i \leq \ell(\bar{\e}),\ \pbl \e_i : \sla_i}
\infer1[(ORC)]{\pbl \X(\bar{\e}) : \infty}
\end{prooftree}}}
\]

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\pbl  \cmd\ : \sla_1}
\hypo{\sla_1 \leq \sla_2}
\infer2[%(SUB)
]{\pbl  \cmd\ : \sla_2}
\end{prooftree}

\[
\begin{prooftree}
\hypo{\phantom{\romanobox{$\sla_2 \neq \infty$}}}
\infer1[%(SKP)
]{\pbl \skp\ : \levela}
\end{prooftree}
\qquad
\scalebox{1}{
\begin{prooftree}
\hypo{\typenv(\x) = \sla_1}
\hypo{\pbl \e: \sla_2}
\hypo{(\sla_{out} = \levela) \vee (\sla_1  \ord \sla_2)}
\hypo{$\romanobox{$\sla_2 \neq \infty$}$}
\infer4[(ASG)
]{\pbl \x \asg \e \ : \sla_1}
\end{prooftree}}
\]

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\pbl  \cmd_1 :\sla}
\hypo{\pbl \cmd_2:\sla}
\infer2[%(SEQ)
]{\pbl \cmd_1 \sep \cmd_2 \ :\sla}
\end{prooftree}}
\qquad
\scalebox{1}{
\begin{prooftree}
\hypo{\pbl \e: \sla}
\hypo{\pbl \cmd_{\true}: \sla}
\hypo{\pbl \cmd_{\false}:\sla}
\infer3[%(CND)
]{\pbl \ifa (\e) \{\cmd_{\true}\} \elsea \{\cmd_{\false}\}\ :\sla}
\end{prooftree}
\]

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\typenv,\typop \vdash^{\sla}_\sla \e: \sla}
\hypo{\typenv,\typop \vdash^\sla_\sla \cmd : \sla}
\hypo{\levelb \ord \sla}
\hypo{$\romanobox{$\sla \neq \infty$}$}
\infer4[(WI)
]{\typenv,\typop \vdash^{\levela}_\levela  \while (\e) \{\cmd\}\ :\sla}
\end{prooftree}
\]

\[
\scalebox{1}{
\begin{prooftree}
\hypo{\typenv,\typop \vdash^\sla_{\sla_{out}} \e: \sla}
\hypo{\typenv,\typop \vdash^\sla_{\sla_{out}} \cmd : \sla}
\hypo{\levelb \ord \sla \ord \sla_{out}}
\hypo{$\romanobox{$\sla \neq \infty$}$}
\infer4[(WH)
]{\pbl  \while (\e) \{\cmd\}\ :\sla}
\end{prooftree}
\qquad
\scalebox{1}{
\begin{prooftree}
\hypo{\pbl \e  : \sla}
%\hypo{\slb \neq \infty}
\hypo{\sla_{in} \ord \sla}
\infer2[%(BRK)
]{\pbl \brk(\e)  : \sla_{in}}
\end{prooftree}
\]

\[
\scalebox{1}{\romanobox{\begin{prooftree}
\hypo{\pbl \X(\bar{\e}) : \infty}
\hypo{\pbl \X(\bar{\x}) :\infty}
\hypo{\forall i \leq \ell(\bar{\x}),\ \pbl \x_i : \sla_i}
\hypo{\sla_{out} \ordst \meet_i \sla_i}
\infer4[(OBK)]{\pbl \brk(\size{\X(\bar{\e})} >\size{\X(\bar{\x})})  : \sla_{in}}
\end{prooftree}

\[
\romanobox{
\scalebox{1}{
\begin{prooftree}
\hypo{\pbla \bar{\X} : \overline{\bar{\TW} \to \TW}}
\hypo{\pbla \bar{\x}: \bar{\TW}}
\hypo{\pbla \bar{\y} : \bar{\TW}}
\hypo{\pbla \x : {\TW}}
\infer4[(DEF)]{\pbla \proc(\bar{\X},\bar{\x})\{[\var \bar{\y}\sep\!]\ \cmd  \ \ret \x\} : (\overline{\bar{\TW} \to \TW}) \to \bar{\TW} \to \TW}
\end{prooftree}
\]

\[
\romanobox{
\scalebox{1}{
\begin{prooftree}
\hypo{\pbla  \proc(\bar{\X},\bar{\x})\{ \cmd  \ \ret \x\} : (\overline{\bar{\TW} \to \TW}) \to \bar{\TW} \to \TW}
\hypo{\pbla  \bar{\clos} : \overline{\bar{\TW} \to \TW}}
\hypo{\pbla \bar{\term} : \bar{\TW}}
\infer3[(CALL)]{\pbla \callcc\proc(\bar{\clos},\bar{\term}) : \TW}
\end{prooftree}
\]

\[
\romanobox{
\begin{prooftree}
\hypo{\typenvs(\va) = \STW}
\infer1[(VAR)]{\pbla \va : \STW}
\end{prooftree}
\qquad
%\hypo{\typenvs \uplus \{\va : \STW\},\typproc,\typop \vdash \term :\STW' }
%\infer1[(L)]{\pbla \abs{\va}.{\term} : \STW \to \STW'}
%\hypo{\pbla \term_1 : \STW \to \STW'}
%\hypo{\pbla \term_2 : \STW}
%\infer2[(A)]{\pbla \term_1 \app {\term_2} : \STW'}
\romanobox{
\begin{prooftree}
\hypo{\typenvs\uplus \{\bar{\x} : \bar{\TW}\} ,\typproc,\typop \vdash \term : \TW}
\infer1[(ABS)]{\pbla  \abs{\bar{\x}}.\term : \bar{\TW}\to \TW}
\end{prooftree}
\]

\[
\romanobox{
\scalebox{1}{
\begin{prooftree}
\hypo{\pbla \prog : {\STW}}
\hypo{\typproc(\procn) = \langle \typenv, (\sla,\sla_{in},\sla_{out}) \rangle}
\hypo{\pbl \body(\procn) : \sla}
\infer3[(DEC)]{\pbla \letin{{\procn}} \prog : \STW}
\end{prooftree}
\]

\[
\romanobox{
\begin{prooftree}
\hypo{\typenvs\uplus\{\va:\STW\},\typproc,\typop \vdash \prog : {\STW'}}
\infer1[(BOX)]{\pbla \boite{[\va]}{\prog} : \STW \to \STW'}
\end{prooftree}
\]

Level-based typing rules for second-order programs

§.§ Type System

Now we adapt the declassification policy presented in Section <ref> to the second-order programming language.

§.§.§ Simple Types and Levels.

Let $\TW$ be the type of words in $\W$. The set $\SST$ contains all simple types over $\TW$ that are defined inductively by the following grammar $\STW  ::= \TW \ | \ \STW \to \STW.$

To account for oracle outputs, the considered set of levels is now $\SLI \triangleq \mathbb{N} \cup \{\infty\}$.
The level $\infty$ behaves as expected: for each $ \sla \in \SLI,\ \sla \ord \infty,\ \sla \mathbf{+} \infty = \infty,\  \sla \join \infty =\infty$, and $\sla \meet \infty =\sla$ hold.
Similarly to simple types, levels can be extended to functional levels by $\STW ::=  \tau \ | \  \STW \to \STW$, with $\tau \in \SLI$.
The order of a type is defined inductively by $\order(\STW_1 \to \STW_2) \triangleq \max(1+\order(\STW_1),\order(\STW_2))$ and $\order(\sla)=\order(\TW) \triangleq 0$.

As usual, an operator $\op$ will have functional levels of the shape $\sla_1 \to \ldots \to \sla_{ar(\op)+1}$ of order $1$ that can thus be viewed as a tuple in $\SLI^{ar(\op)+1}$.

§.§.§ Typing Environments.

We define four kinds of typing environments:

* variable typing environments $\typenv$ are finite maps in $\Var_0 \to \SLI$,

* operator typing environments $\typop$  map each operator $\op \in \Operator$ to a finite map $\Delta(\op) \in \SL^2 \to\mathcal{P}(\SLI^{ar(\op)+1})$,

* simple typing environments $\typenvs$ are finite maps in $\Var \to \SST$,

* procedure typing environments $\typproc$ map each procedure name to a pair $\langle\typenv,\bar{\sla}\rangle$ consisting of a variable typing environment $\typenv$ and a triplet of levels $\bar{\sla} \in \SLI \times \SL \times \SL$.

Variable and operator typing environment are defined as in Section <ref>, with the distinction that $\infty$ can appear in the functional level of an operator. Simple typing environments just assign the type $\TW$ to variables in $\Var_0$ and the type $\TW \to \TW$ to variables in $\Var_1$. A procedure typing environment assigns a typing context to each procedure.
Operator, procedure, and simple typing environments are global, i.e. defined for the whole program. Variable typing environments are local, i.e. relative to the procedure under analysis.

For a procedure typing environment $\typproc$, it will be assumed that for every $\proc \in \dom(\typproc)$, if $\typproc(\proc)=\langle\typenv,\bar{\sla}\rangle$ then $(\param(\proc) \cup \local(\proc)) \cap \Var_0  \subseteq \dom(\typenv)$. I.e., $\typproc$ is defined for the local variables and order-$0$ parameters of the  procedure $\proc$.

§.§.§ Typing Judgments.

The type system uses two kinds of judgments:

* Statement (resp. expression) typing judgments $\pbl \cmd : \sla$ (resp. $\pbl \e : \sla$), with $\sla_{in}, \sla_{out} \in \SL$ and $\sla \in \SLI$.  The  meaning of this judgment is that the statement level (resp. expression level) is $\sla \in \SLI$, under the prerequisite that the innermost  level is $\sla_{in}$, and  the outermost level is $\sla_{out}$. These levels are defined similarly to Section <ref> and are still finite (i.e., $\neq \infty$) as our type discipline will prevent a loop from being guarded by level $\infty$ data.

* Program (resp. term and closure) typing judgments $\pbla \prog : \STW$ ($\pbla \term :\TW$ and $\pbla \clos : \bar{\TW} \to \TW$, resp.). The meaning of this judgment is that  $\prog$ ($\term$ and $\clos$, resp.) is of simple type $\STW$ ($\TW$ and $\bar{\TW} \to \TW$, resp.) under the considered typing environment. Moreover, if $\order(\STW)=i$ then $\prog$ is said to be of order-$i$. On the other hand, a term (resp. closure) is necessarily of order-$0$ (resp. $1$), i.e., of type $\TW$ (resp. $\bar{\TW} \to \TW$).

§.§.§ Typing Rules.

The type system is provided in Figures <ref>.  Well-typed programs are normal form and guarded order-$2$ programs that can be given the  type $(\overline{\TW \to \TW}) \to \bar{\TW} \to \TW$, i.e., second-order programs computing a functional.
The type system is composed of two sub-systems. The typing rules provided at the lower part of Figure <ref> enforce that terms follow a standard simply-typed discipline.
The typing rules presented in the upper part of Figure <ref> ensure that procedure bodies follow a level-based type discipline, adapting smoothly the policy of Section <ref> to the second-order setting.
The transition between the two subsystems is performed in the Rule (DEC) of Figure <ref> that checks that the procedure body follows the level-based type discipline once and for all in a procedure declaration.
In Figure <ref>, the main differences with  the type system of Figure <ref> are highlighted in boxes.
For simplicity, we have not specified the sequence lengths in the typing rules. However, it is clear that programs must check the following trivial syntactic constraints: in Rule (CALL), the type arity of each closure must match the arity $ar(\X)$ of the corresponding procedure parameter; in Rule (ORC) , the length of $\bar \e$ is equal to $ar(\X)$.

§.§.§ Intuition.
We now provide some intuitions on the typing discipline.

The typing rules of Figure <ref> that are not in boxes implement a standard noninterference policy with declassification, as already presented in Figure <ref>.
In a loop of level $\sla$, data of level $\sla$ or higher can only be copied or decreased using neutral operators (or declassifications).
As neutral operators compute subwords or predicates, the corresponding space is polynomially bounded in the size of the program input. The restrictions put on declassified data preserve this property.
Moreover, data of strictly smaller level can increase by a constant in each assignment. Hence under suitable assumptions: aperiodicity and safety  (see next section), the loop terminates in a polynomial number of steps and the lower level data increase at most polynomially.
The same kind of reasoning can be performed on loops of strictly smaller level. Hence the program cannot run for time greater than a composition of a constant (in the size of the program) number of polynomials in the input size and the maximal output of an oracle call. This ensure that the program computes a functional in Oracle PolyTime ($\opt$), as discussed in the introduction.

We now discuss the modification on the level-based discipline. Rule (ORC) takes oracle outputs to level $\infty$.
On this other hand, by the side condition $\tau \neq \infty$, Rules (WH) and (WI) ensure that loops cannot be guarded by data of level $\infty$.
Consequently, by the side condition $\tau_2 \neq \infty$ of Rule (ASG), oracle outputs cannot be directly assigned to in a loop. Hence the only option for an oracle output to be assigned is to be declassified, i.e., truncated and converted to unary (see the reduction rule for $\declass$ in Figure <ref>). We will relax a bit this strong constraint by also allowing the (non unary) truncation of oracle output in the next section.
As a consequence of the restrictions we will put later on admissible operator types and as programs are guarded, only a constant number of unbounded oracle calls can be performed in a typed programs, most of which occur outside while loops (only 1 will be admitted per outermost while loop).
Rule (OBK) enforces that break statements with oracle calls are controlled by expressions of the shape $\size{\X(\bar{\e})} > \size{\X(\bar{\x})}$: the while loop breaks if the oracle call has size greater than the size of the evaluation of $\X(\bar{\x})$. However expressions in $\bar{\x}$ have level $\sla_i$ such that $\sla_{out} \ordst \sla_i$. Hence, they cannot be modified inside the (outermost) while loop. The while loop breaks if the size of the oracle call $\X(\bar{\e})$ exceeds the size of the (constant in the loop) call $\X(\bar{\x})$. Notice that the result of the call does not need to be fully explored for the test to be checked (i.e., if value $\v$ is the result of evaluating $()$ the test can be performed in at most $v+1$ steps). This means that while we remain in the loop, the oracle calls are all of size bounded by the size of the result of $()$, i.e., the computed functional remains in Finite  Length Revision ($$).

To conclude, the functionals computed by each procedure call are in $= ∩$ and the $λ(-)_2$ closure of Theorem~\ref{thm:KS} can just be simulated by our notions of closure and procedure call.

\subsection{Safe Programs and their Properties}\label{ss:sec}

We now adapt the notion of safety to the second-order setting.

\begin{definition}\label{sote}
An operator typing environment $\typop$ is \emph{safe} if $$\Delta(\truncate)(\sla_{in},\sla_{out}) \triangleq \{\infty \to \tau \to \tau'  \ | \  \tau' \ordst \sla_{in} \text{ and }\sla_{out} \ord \tau\}$$ and for each $\op \in \dom(\typop)$, $\op \neq \truncate$, is either neutral, positive, or polynomial, $\sem{\op} \in \FP$, and for each $\sla_{in},\sla_{out} \in \SL$, and for each $\sla_1 \to \ldots \to \sla_{ar(\op)+1} \in \typop(\op)(\sla_{in},\sla_{out})$,
\begin{enumerate}
\item  if $\op$ is a neutral operator then
$\sla_{ar(\op)+1} \ord \meet_{i=1}^{ar(\op)} \sla_i \ord \join_{i=1}^{ar(\op)} \sla_i  \neq \infty$;\label{premier}
\item  if $\op$ is a positive operator then
$\sla_{ar(\op)+1} \ord \meet_{i=1}^{ar(\op)} \sla_i \ord \join_{i=1}^{ar(\op)} \sla_i  \neq \infty,$
and  either $\sla_{ar(\op)+1} \ordst \sla_{in}$ or $\sla_{ar(\op)+1}=\levela$;\label{second}
\item  if $\op$ is a polynomial operator then $\sla_{out}=\levela$.
\label{third}
\end{enumerate}
\end{definition}

We briefly explain the intuition that lies behind safe operator typing environments.
Operator $$ is treated apart to allow non-unary flows from level $∞$ to a finite level $τ'$. However the price to pay for that permissiveness is that the output of a truncate can never be used to guard the corresponding loops (as $τ' _in$).  The other constraints are similar to the ones of Definition~\ref{def:sote}, as there cannot be an operator applied to an oracle output (level $∞$ data), a declassification or a truncation have to occur first.

%%In Example~\ref{ex:npp}, some of the operators used in Program \texttt{I} of Listing~\ref{fig:bruce} were already shown to be neutral or positive.
%%For the other operators, we have:
%%the projections $\gauche$ and $\droite$ are neutral as they compute a subword of their operands,
%%the operators $\size{\cdot}$ and $\pad$ are positive as, $\size{\sem{\size{\w}}} \leq \size{\w}$ and $\size{\sem{\pad}(\u,\v)} \leq \size{\v}$,
%%$\pair$ is polynomial as $\size{\sem{\pair(\u, \v)}} \leq \size{\u}+\size{\v}+1 \leq 2(\max(\size{\u},\size{\v}))+1$.
%Consider the operators $-1$, $\gauche$, and $+$ in the program of Listing~\ref{fig:bruce} and an operator typing environment $\typop$ such that
%\typop(-1)(\levelb,\levelb)&=\{\levelb \to \levelb \to \levelb \} \cup \{\sla \to \sla' \to \levela \ | \ \sla,\sla' \ord \levelb\}\\
%\typop(\gauche)(\levelb,\levelb)&=\{\levelb \to \levelb \to \levelb \} \cup \{\sla \to \sla' \to \levela \ | \ \sla,\sla' \ord \levelb\}\\
%\typop(+)(\levela, \levela)&=\{\sla\to\sla'\to\sla''\ |\ \sla, \sla', \sla'' \ord\levelb\}.
%$\typop$ is safe as $-1$ and $\gauche$ are neutral (see Condition~\ref{premier} of Definition~\ref{sote}) and $+$ is polynomial. However allowing $\levelb \to \levela \to \levelb $ to be in $\typop(-1)(\levelb,\levelb)$ would break safety as it breaks Condition~\ref{premier} (i.e., $ \levelb \not\ord \levelb \meet  \levela$).
%%In the particular case of the outermost level $\sla_{out} = \levela$, any level can be given to $-1$, $\gauche$, and $+$. For example, allowing $\levela \to \levelb \in \Delta(-1)(\levelb,\levela)$ or  $\levela \to \infty \to \levelc \in \Delta(+)(\levelb,\levela)$ does not break safety. In other words, at outermost level $\levela$ (outside loops), levels do not matter.
%%As $+$ is polynomial, for $\levela \ordst \sla_{out}$ and by Condition~\ref{third}, it also holds that $\Delta(+)(\sla_{in},\sla_{out})=\emptyset$. This prevents the use of any polynomial operator like $+$ inside a while loop.

\begin{definition}[Safety]
Given a procedure typing environment $\typproc$ and a safe operator typing environment $\typop$, $\prog $ is a \emph{safe program}  if it is a well-typed program wrt. $\Omega$ and $\Delta$, i.e., $ \emptyset,\typproc,\typop \vdash \prog : (\overline{\TW \to \TW}) \to \bar{\TW} \to \TW$ can be derived. Let $\safe$ be the set of safe programs and $\Delta\safe$ be the set of safe programs wrt. $\Delta$.
\end{definition}

\begin{example}\label{ex:safe}
Let us study how procedure K from Listing~\ref{ex:K} can be part of a safe program.
The $\while$ loop can be typed as follows:\\

\begin{minipage}{0.42\textwidth}
\begin{lstlisting}[firstnumber=22]
$\brk$(|X(i$^{\levela}$)$^{\infty}$|>|X(r$^{\levelc}$)$^{\infty}$|): $\levelb\sep$
i$^{\levela}\asg\truncate$(X(i$^{\levela}$)$^{\infty}$,p$^{\levelb}$)$^{\levela}: \levela\sep$
s$^{\levelb}\asg$(s$^{\levelb}$-1)$^{\levelb}$ : $\levelb$
\end{lstlisting}
\end{minipage}

The level of \verb!s! at line 22 is enforced to be at least $\levelb$ (and cannot be $\infty$), by Rule (WI). Hence in the while loop body the innermost and outermost levels are equal to $\levelb$.
The level of \verb!r! at line 23 is enforced to be $\levelc$, as it needs to be strictly greater than the outermost level, by Rule (OBK).
The level of \verb!p! at line 24 is enforced to be equal to the outermost level $\levelb$, by definition of safety.
The level of the whole expression $\truncate$\verb!(X(i),p)! is $\levela$.
Indeed, by definition of a safe operator typing environment, it has to be smaller than the level of its first operand $\infty$ and strictly smaller than the innermost level $\levelb$.
Hence at line 24, the level of \verb!i! is enforced to be $\levela$ by Rule (ASG) and the statement can be given the level $\levela$.
Finally, the full loop body can be typed using the rules for sequence and subtyping (SEQ) and (SUB).
Notice that the remaining lines of Listing~\ref{ex:K} type as there are no constraints on assignments outside loops.
\end{example}

%\subsection{Properties of Safe and ASN Programs}

First, we can show our main result, stating that the set of functionals computed by safe, terminating, and aperiodic programs is exactly $$. Hence, we have succeeded to capture this class using the $$ scheme of Theorem~\ref{thm:KS}.

\begin{restatable}{theorem}{thmmain}\label{thm:main}
$\sem{\safe  \cap \ASN} = \BFF$.
\end{restatable}

And we can show that safety is tractable. Again, let $$ be the number of symbols in $$.
\begin{restatable}{theorem}{thmtiprog}\label{thm:tiprog}
Given a safe operator typing environment $\typop$, deciding whether $\prog \in \Delta\safe$  can be done in time polynomial in $\size{\prog}$.
\end{restatable}
%By Theorem~\ref{thm:tiproc}, the type inference for procedures can be done in time $\mathcal{O}(\size{\prog}^3)$. Type inference of the simply-typed lambda-calculus is known to be a $\Ptime$-complete problem~\cite{M04}.

\section{Conclusion and Future Work}\label{s:con}
We have provided a new declassification policy for program complexity analysis and shown that it can be applied to provide an expressive characterization of $$ and the first characterization of the class $$ based on $$.
The declassification policy uses a declassification construct that can be used  inside while loop and is, hence, quite general. The characterization is achieved by putting extra and intuitive restrictions: aperiodicity and termination in the second-order case.  We also show that type inference for safety is tractable and that aperiodicity is a $Π^0_1$-complete problem. We have also exhibited a tractable and completeness-preserving criterion for aperiodicity. A future line of research is the search for tractable and more expressive criteria for aperiodicity.

\begin{thebibliography}{HKMP22}

[1]
Stephen Bellantoni and Stephen~A. Cook.
\newblock A new recursion-theoretic characterization of the polytime functions.
\newblock {\em Comput. Complex.}, 2:97--110, 1992.

[2]
Siddharth Bhaskar, Cynthia Kop, and Jakob~Grue Simonsen.
\newblock Subclasses of ptime interpreted by programming languages.
\newblock {\em Theory Comput. Syst.}, 67(3):437--472, 2023.

[3]
Patrick Baillot, Ugo~Dal Lago, Cynthia Kop, and Deivid Vale.
\newblock On basic feasible functionals and the interpretation method.
\newblock In {\em Foundations of Software Science and Computation Structures,
{FOSSACS} 2024}, 2024.
\newblock Accepted.

[4]
Michael Backes and Birgit Pfitzmann.
\newblock Intransitive non-interference for cryptographic purposes.
\newblock In {\em SSP 2003}, pages 140--152, 2003.

[5]
Stephen~A. Cook.
\newblock Computability and complexity of higher type functions.
\newblock In {\em Logic from Computer Science}, pages 51--72. Springer, 1992.

[6]
Stephen~A. Cook and Alasdair Urquhart.
\newblock Functional interpretations of feasibly constructive arithmetic.
\newblock {\em Ann. Pure Appl. Logic}, 63(2):103--200, 1993.

[7]
Daniel de~Carvalho and Jakob~Grue Simonsen.
\newblock An implicit characterization of the polynomial-time decidable sets by
cons-free rewriting.
\newblock In {\em Rewriting and Typed Lambda Calculi ({RTA-TLCA} 2014)}, volume
8560 of {\em Lecture Notes in Computer Science}, pages 179--193. Springer,

[8]
Ugo Dal~Lago, Reinhard Kahle, and Isabel Oitavem.
\newblock A recursion-theoretic characterization of the probabilistic class pp.
\newblock In {\em Mathematical Foundations of Computer Science (MFCS 2021)},
volume 202, pages 35:1--35:12. Schloss Dagstuhl – Leibniz-Zentrum für
Informatik, 2021.

[9]
Norman Danner, Jennifer Paykin, and James~S. Royer.
\newblock A static cost analysis for a higher-order language.
\newblock In {\em Programming languages meets program verification, {PLPV}
2013}, pages 25--34. {ACM}, 2013.

[10]
Norman Danner and James~S. Royer.
\newblock Adventures in time and space.
\newblock In {\em Principles of Programming Languages, {POPL} 2006}, pages
168--179. ACM, 2006.

[11]
J{\"o}rg Endrullis, Herman Geuvers, Jakob~Grue Simonsen, and Hans Zantema.
\newblock Levels of undecidability in rewriting.
\newblock {\em Information and Computation}, 209(2):227--245, 2011.

[12]
Petr H{\'{a}}jek.
\newblock Arithmetical hierarchy and complexity of computation.
\newblock {\em Theor. Comput. Sci.}, 8:227--237, 1979.

[13]
Emmanuel Hainry, Emmanuel Jeandel, Romain P{\'{e}}choux, and Olivier Zeyen.
\newblock Complexityparser: An automatic tool for certifying poly-time
complexity of java programs.
\newblock In {\em Theoretical Aspects of Computing - {ICTAC} 2021}, pages
357--365. Springer, 2021.

[14]
Emmanuel Hainry, Bruce~M. Kapron, Jean-Yves Marion, and Romain P{\'{e}}choux.
\newblock A tier-based typed programming language characterizing feasible
\newblock In {\em Logic in Computer Science, LICS 2020}, pages 535--549, 2020.

[15]
Emmanuel Hainry, Bruce~M. Kapron, Jean-Yves Marion, and Romain P{\'{e}}choux.
\newblock Complete and tractable machine-independent characterizations of
second-order polytime.
\newblock In {\em Foundations of Software Science and Computation Structures,
{FOSSACS} 2022}, pages 368--388, 2022.

[16]
Emmanuel Hainry, Jean-Yves Marion, and Romain P{\'e}choux.
\newblock Type-based complexity analysis for fork processes.
\newblock In {\em Foundations of Software Science and Computation Structures,
FOSSACS 2013}, pages 305--320. Springer, 2013.

[17]
Emmanuel Hainry and Romain P{\'{e}}choux.
\newblock A type-based complexity analysis of object oriented programs.
\newblock {\em Inf. Comput.}, 261:78--115, 2018.

[18]
Emmanuel Hainry and Romain P{\'{e}}choux.
\newblock Theory of higher order interpretations and application to basic
feasible functions.
\newblock {\em Log. Methods Comput. Sci.}, 16(4), 2020.

[19]
Emmanuel Hainry and Romain P{\'{e}}choux.
\newblock A general noninterference policy for polynomial time.
\newblock {\em Principles of programming languages}, 7({POPL}):806--832, 2023.

[20]
Robert~J. Irwin, James~S. Royer, and Bruce~M. Kapron.
\newblock On characterizations of the basic feasible functionals (part {I}).
\newblock {\em J. Funct. Program.}, 11(1):117--153, 2001.

[21]
Neil~D. Jones.
\newblock The expressive power of higher-order types or, life without {CONS}.
\newblock {\em J. Funct. Program.}, 11(1):5--94, 2001.

[22]
Bruce~M. Kapron and Stephen~A. Cook.
\newblock A new characterization of {Mehlhorn}'s polynomial time functionals
(extended abstract).
\newblock In {\em Foundations of Computer Science}, pages 342--347. IEEE, 1991.

[23]
Bruce~M. Kapron and Florian Steinberg.
\newblock Type-two polynomial-time and restricted lookahead.
\newblock In {\em Logic in Computer Science, LICS 2018}, pages 579--588. ACM,

[24]
Daniel Leivant and Jean-Yves Marion.
\newblock Lambda calculus characterizations of poly-time.
\newblock {\em Fundam. Inform.}, 19(1/2):167--184, 1993.

[25]
Peng Li and Steve Zdancewic.
\newblock Downgrading policies and relaxed noninterference.
\newblock In {\em Principles of programming languages, POPL 2005}, pages
158--170. {ACM}, jan 2005.

[26]
Jean-Yves Marion.
\newblock A type system for complexity flow analysis.
\newblock In {\em Logic in Computer Science, LICS 2011}, pages 123--132. IEEE
Computer Society, 2011.

[27]
Andrew~C. Myers and Barbara Liskov.
\newblock Protecting privacy using the decentralized label model.
\newblock {\em ACM Trans. Softw. Eng. Methodol.}, 9(4):410--442, 2000.

[28]
Andrew~C. Myers.
\newblock {JFlow}: practical mostly-static information flow control.
\newblock In {\em Principles of programming languages, POPL 1999}, pages
228--241. {ACM}, jan 1999.

[29]
Andrei Sabelfeld and David Sands.
\newblock Declassification: Dimensions and principles.
\newblock {\em J. Comput. Secur.}, 17(5):517--548, oct 2009.

[30]
Dennis Volpano, Cynthia Irvine, and Geoffrey Smith.
\newblock A sound type system for secure flow analysis.
\newblock {\em J. Comput. Secur.}, 4(2-3):167--187, 1996.

[31]
Dennis Volpano and Geoffrey Smith.
\newblock Verifying secrets and relative secrecy.
\newblock In {\em Principles of programming languages, POPL 2000}, pages
268--276. {ACM}, jan 2000.

[32]
Steve Zdancewic and Andrew~C. Myers.
\newblock Robust declassification.
\newblock In {\em Computer Security Foundations Workshop, CSFW 2001}, pages
15--23. {IEEE}, 2001.

\end{thebibliography}

\end{document}
\newpage

\appendix

\section{Proof of Type-1 Completeness}
\begin{example}\label{ex:mult1}
Consider the program below computing the multiplication.

\begin{lstlisting}[linewidth=.42\textwidth]
mult(x$^\levelc$,y$^\levelc$) {
r$^\levelb\asg$0 :$\levelc\sep$
z$^\levelc\asg$x$^\levelc$ :$\levelc\sep$
r$^\levelb\asg$r+1 :$\levelc\sep$
z$^\levelc\asg$z-1  :$\levelc$
y$^\levelc\asg$y$^\levelc$-1 :$\levelc$
\end{lstlisting}

levels of variables ($\typenv$) have been provided as superscripts in the code.
%This example illustrates the need for more than two levels in order to have a better expressive power (However, as we will see later two levels are sufficient for polynomial time completeness).
The following levels are included in $\typop$:

%For the operator typing environment $\typop$, we use the following levels:
\begin{array}{rcl}
\levelc\to\levelc\to\levelc&\in&\typop(\texttt{and})(\levelc, \levelc)\cap\typop(>)(\levelc,\levelc)\\
\levelb\to\levelb & \in & \typop(+1)(\levelc, \levelc)\\
\levelc\to\levelc & \in & \typop(-1)(\levelc, \levelc).
\end{array}
This typing environment is safe as \texttt{and}, $>$, and $-1$ are neutral operators and $+1$ is a positive operator.

The program is aperiodic since, for the enclosing while loop (lines 3 to 10), $\store(\y)$ is different each time the guard $\y>0$ is encountered (it has been decremented).
Similarly, for the inner loop (lines 5 to 8), only unique values $\store(\z)$ are seen in the strict subtrees of root $(\while(\z>0)\{\ldots\},\store)$.
\end{example}

\thmfpcomplete*

\begin{proof}
Given function $f$ computed by a Turing machine $M_f$ in time $Q(n)$ for inputs of size $n$, we encode this computation by first computing the time bound, second defining a statement that simulates the one-step transition of the Turing machine, and finally iterating this statement $Q(n)$ times.
The computation of polynomials is a matter of multiplications and additions.
We know, from Example~\ref{ex:mult1}, how to do it safely and aperiodically, and obtain the result in a variable \texttt{r} of level $\levelb$.

We can encode the configuration of the Turing machine using 3 variables of level $\levela$ that represent the left part of the tape, the right part of the tape, and the state of the machine.
The operations on those variables are not neutral but positive (with constant 1 for the operators on tapes and constant the number of states for the state variable).
The transition function of $M_f$ is then implemented by a $\instr{if}$ statement that reads and modifies those variables. This statement can be given level $\levela$.
Assume the initial state of the machine is $0$, we obtain a program of the following form:

\begin{lstlisting}[linewidth=0.42\textwidth]
//compute r$^{\levelb}$ equal to $Q(|\store($x$)|)$
/*List of ifs simulating
the transition function */
if(h$^{\levela}$=$\alpha$ and q$^{\levela}$=10) {
/*$\text{E.g., when the symbol is }\alpha$
$\text{and the state is 10,}\ \text{write }\beta\text{,}$
$\text{move right, enter state 11}$*/
return right$^{\levela}$
\end{lstlisting}

The variable typing environment $\typenv$ is provided by the variable annotations in the program code.
The safe operator typing environment $\typop$ is an extension of the one from Example~\ref{ex:mult1} with
\begin{array}{rcl}
\{\levelb\to\levelb\} & \subset & \typop(>0)(\levelb, \levelb)\\
\{\levelb\to\levelb\} & \subset & \typop(-1)(\levelb, \levelb)\\
\forall\sla_1, \sla_2, \{\levela\to\levela\to\levela\} & \subset & \typop(=)(\sla_1, \sla_2) \cap \typop(\texttt{and})(\sla_1, \sla_2)\\
\forall\sla_1,\sla_2, \{\levela\to\levela\} & \subset & \typop(+1)(\sla_1, \sla_2)\cap\typop(\texttt{head})(\sla_1, \sla_2)\\
&&\cap\typop(\texttt{cons})(\sla_1, \sla_2)\cap\typop(\texttt{tail})(\sla_1, \sla_2)\\
\end{array}

This program is safe and aperiodic.
\end{proof}

\section{Proof of Type-1 Soundness}
Given a typing judgment $j$, a \emph{typing derivation} $ρj$  is a tree whose root is the typing judgment $j$ and whose children are obtained by applications of the typing rules of Figure~\ref{fig:t1ts}. The notation $ρ$ will be used whenever mentioning the root of a typing derivation is not explicitly needed. %We use the notation $\rho \rightslice j$ (R) to denote the typing derivation $\rho \rightslice j$ whose children are obtained by application of a typing rule labeled by (R).
Given two typing derivations $ρ$ and $ρ'$, we write $ρ' ⊑ρ$ (respectively $ρ' ⊏ρ$) if $ρ'$ is a (strict) subtree of $ρ$. $ρ'$ is called a \emph{subderivation} of $ρ$. %Let $\D(\rho)$ be  defined by $\D(\rho)=\{\rho' \ | \ \rho' \leq \rho\}$ and let $\mathring{\D} (\rho)$ be defined by $\mathring{\D} (\rho)=\D(\rho)-\{ \rho\}$.

To prove soundness, we introduce intermediate lemmas.
%First, statement levels are monotonic in their substatement level in a given typing derivation.
The following Lemma states that statement levels are monotonic in their substatement level in a given typing derivation.

\begin{lemma}[Monotonicity]\label{lem:monotonicity}
For any two typing subderivations $\rho \rightslice \pbl \cmd : \sla$ and $ \rho' \rightslice \pblp \cmd' : \sla'$ of a safe program, if $\rho' \sqsubseteq \rho$ then $\sla' \ord \sla$.
\end{lemma}

\begin{proof}
Suppose by contradiction that $\rho' \sqsubseteq \rho$ and $\sla \ordst \sla'$ hold. As all typing rules for statements in Figure~\ref{fig:t1ts} %(and Figure~\ref{sfig:tsprog})
are monotonic in the statement level,  $\rho \rightslice \pbl \cmd : \sla$ cannot be derived from $\rho'$.\qedhere
\end{proof}

Let $()$ be the set of variables that are assigned to in $$, for example, $()= {,}$.
The confinement Lemma expresses that statements of level $$ cannot write in variables of strictly higher level.

\begin{lemma}[Confinement]\label{lem:confinement}
For any typing subderivation $\rho \rightslice \ \pbl \cmd:\sla$ of a safe program, it holds that for all $ \x \in \A(\cmd)$, $\Gamma(\x) \ord \sla$.
\end{lemma}

\begin{proof}
By contradiction. Suppose that $\rho \rightslice \pbl \cmd:\sla$ holds. Consider a variable $\x \in \A(\cmd)$ and suppose that $\sla \ordst \Gamma(\x)$. By typing Rule (ASG), there is an expression $\e$  and there are levels $\sla_{in}',\sla_{out}'$ such that $\rho' \rightslice  \vdash_{\sla_{out}'}^{\sla_{in}'} \x \asg \e : \Gamma(\x)$ and $\rho' \sqsubseteq \rho$.
Consequently, by Lemma~\ref{lem:monotonicity}, $ \Gamma(\x) \ord \sla$, which contradicts the assumption.
\qedhere
\end{proof}

%\Rcom{Is the lemma below useful?}
%The following leveling Lemma expresses that inside a loop the statement level is bounded by the innermost level, itself bounded by the outermost level.
%Let $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ be a typing subderivation of a safe program with respect to the typing environments $\typenv,\typop$.  For any typing derivation $ \rho' \rightslice \pblp \cmd': \sla'$, if $\rho' \sqsubset \rho$, then it holds that $\sla' \ord \sla_{in}' \ord \sla_{out}'$.
%The only two typing rules updating the innermost and outermost levels are Rules (WI) and (WH). Rule (WI) cannot be called in a subderivation of a while loop because in a loop the outermost level is always greater then $\levelb$. The side condition in the hypothesis of Rule (WH) ensures that $\sla  \leq \sla_{in} \leq \sla_{out}$. Hence, the result follows directly by Lemma~\ref{lem:monotonicity}.
%Notice that the above Lemma is not true for an outermost loop, as by Rule (WI), the innmerost/outermost level is $\levela$ and it holds that $\levelb \ord \sla$. This is the reason why the requirement $\rho' \sqsubseteq \rho$ is needed.

Let $♢$ be a special symbol denoting a hole. Given a sequence of expressions $^n$ of length $n$, let $_i,C^n$, for $i ≤n$, denote the sequence obtained by replacing $_i$ by $C$ in $$. Contexts are defined by the following grammar:
\[
C, D, \ldots
\rgl \diamond
\ |\ \op(\bar{\e}_{i,C}^{ar(\op)})  \ | \ % \truncate(\bar{\e}_{i,C}^2)\\
\declass(\bar{\e}_{i,C}^2)\ | \ %\X (\bar{\e}_{i,C}^n) \ | \
\bar{\e}_{i,C}^n
\]
%where the length of each sequence $l(\bar{\e}_{i,C})$ is assumed to match the artiy of the corresponding construct.

Given an expression $$ and a context $C$, $C[]$ is the expression obtained as the result of substituting  the expression $$ for the hole $♢$.
In this setting, $$ is a \emph{subexpression} of $C[]$.
Given two expressions $$ and $'$, $'$ is \emph{declassified in }$$ if there are two contexts $C,D$ and an expression $$̣ such that $\e=C[\declass(D[\e'],\d)]$.

In a safe program, only variables of higher level or whose occurrences are all declassified
can be accessed when evaluating an expression.

For any triplet of typing subderivations
\begin{array}{l}
\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla, \\
\rho' \rightslice  \pblp \e' : \sla',\text{ and}\\
\rho'' \rightslice \pblpp \e'' : \sla''
\end{array}
of a safe program, if $\rho'' \sqsubseteq \rho' \sqsubseteq \rho$, then (at least) one of the following conditions holds:

* $\sla' \ord \sla''$,

* $\e''$ is declassified in $\e'$.

By structural induction on the expression $\e'$.

* Case $\e'=\x=\e''$: $\sla' = \sla''$.

* Case $\e'=\op(\ldots,\e^3,\ldots)$: Assume that $\e^3$ is of level $\sla^3$. If $\e''$ is declassified
in $\e^3$ then $\e''$ is declassified
in $\e'$; if $\sla^3 \ord \sla''$ then $\sla' \ord \sla^3 \ord \sla''$, by definition of safe operator typing environment for neutral and positive operators ($\op$ cannot be polynomial in a loop) and by applying typing Rule (OP).

* Case $\e'=\declass(\e^3,\d)$: if $\e''\in \e^3$ then $\e''$ is declassified in $\e'$. If $\e'' \in \d$ of level $^3$ then we apply the induction hypothesis: if $”$ is declassified %/oraculated
in $$̣ then it is declassified
in $\e'$; if $\sla^3 \ord \sla''$ then, by typing Rule (DCL), $\sla^3$ is equal to the outermost level $\sla_{out}'$ and then $\sla' \ord \sla^3 \ord \sla''$.

Consequently, the innermost level of a while loop provides a lower bound on the level of the variables in the guard that are not declassified.

The following Lemma shows that the innermost level of a while loop substatement is always an upper bound on the level of this loop.

For any pair of typing subderivations  $ \rho \rightslice \pbl \while (\e) \{\cmd\}   : \sla$ and $\rho' \rightslice \pblp \cmd' : \sla'$ of a safe program, if $ \rho' \sqsubseteq \rho$, then $\sla'_{in} \ord \sla$.

By a case analysis on rules (WI) and (WH) and using Lemma <ref>.

We now show that within a while loop of level $\sla$, if an expression involving positive operators is assigned to a level $\sla$ variable then the positive subexpressions are all declassified.

For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla'$ of a safe program such that $\rho' \sqsubset \rho$, if $\sla =\sla'$ then for each $\e'' \in \e'$,
if $\e''=\op(\bar{\e})$, for some positive operator $\op$,
then $\e''$ is declassified in $\e'$.

The proof is by induction on the size of the expression $\e'$.
Consider a subexpression $\e'' \in \e'$.
Let $\e''=\op(\bar{\e})$, for some positive operator $\op$, then by definition of safe operator typing environment and by Rule (OP), it holds that if $\op(\bar{\e})$ is of level $\sla''$ then $\sla'' \ordst \sla'_{in}$. Consequently, $\sla'' < \sla$, by Lemma <ref>. As the level of $\e'$ is greater than $\sla$ by Rule (ASG) then $\op(\bar{\e})$ is declassified in $\e'$, by Lemma <ref>.

Now we show that in safe programs any assignment in a loop can cause the memory size to increase by at most a constant.

For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla'$ of a safe program such that $\rho' \sqsubset \rho$, $\exists c \in \mathbb{N}$ such that $\forall \store \in {\tt Stores}$, if $(\store,\e') \toe \w$ then $\size{\w} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c.$

This proof is by induction on expressions.
First note that as the program is safe, by definition of safe operator typing environment (Definition <ref>), no polynomial operator can be called in $\e'$, as the corresponding assignment is inside a while loop by hypothesis ($\rho' \sqsubset \rho$).
Hence its outermost level $\sla_{out}'$ is distinct from $\levela$.

* Case $\e' = \y$. Then by reduction Rule (Var), $\w=\store(\y) \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})$.

* Case $\e' = \op(\bar{\e})$.
By induction hypothesis, if $(\store,\e_i) \toe \w_i$ then
$$\size{\w_i} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_i.$$
By definition of neutral and positive operators, it holds that $\size{\w}=\size{\sem{\op}(\bar{\w})} \leq \max_i(\size{\w_i})+d$, for some $d \geq 0$. Hence $\size{\w} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+ \max_i c_i +d$. Take $c \triangleq \max_i c_i +d$.

* Case $\e' = \declass(\e_1,\e_2)$. Rule (DCL) implies that the level of $\e_2$ is $\sla_{out}$, which in the body of a while loop needs to be finite, from (WI) and (WH). We can apply the induction hypothesis on $\e_2$: assume $(\store,\e_2) \toe \w_2$ then $\size{\w_2} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_2$. If $(\store,\e') \toe \w$, then from the semantics of $\declass$, it holds that:

\size{{\w}} \leq \size{\w_2} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_2.

Now we show that in a loop of level $\sla$, expressions assigned to variables of level greater than $\sla$ and also the loop guard are restricted to some particular bounded domain. For that purpose, we define a notion of span,  corresponding to the set of values that are reachable from a given store.

Given a store $\store$, a typing environment $\typenv$ such that $\dom(\store)=\dom(\typenv)$, and a level $\sla$, the span of $\store$ wrt $\typenv$ and $\sla$ is defined by

\[
\begin{array}{rcl}
\Span& \triangleq &\{ \w \ | \ \exists \x \in \dom(\store),\ \w \dord \store(\x) \wedge \sla \ord \typenv(\x)\} \cup\\
&& \{ 1^n \ | \ n \leq \max_{\x \in \dom(\store) \wedge \sla \ord \typenv(\x)}\size{\store(\x)}\}\cup \{0,1\}.
\end{array}
\]

Notice that $\Span$ is closed under subword, i.e., if $\w \in \Span$ and $\w' \dord \w$ then $\w' \in \Span$.

For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla$ of a safe program such that $\rho' \sqsubset \rho$ holds, $\forall \store \in \texttt{Stores}$, if $(\store,\e') \toe \w$ then $\w \in \Span$.

By induction on expressions.
First note that as the program is safe, by definition of safe operator typing environment (Definition <ref>), no polynomial operator can be called in $\e'$, as the corresponding assignment is inside a while loop by hypothesis ($\rho'  \sqsubset \rho$). Hence its outermost level $\sla_{out}'$ is distinct from $\levela$.

* Case $\e' = \y$. Then by reduction Rule (Var), $\w=\store(\y)$. Moreover, by typing Rule (VAR), $\sla = \typenv(\y)$. Hence $\w \in \Span$.

* Case $\e' = \op(\bar{\e})$. $\op$ cannot be positive, by Lemma <ref>. If $\op$ is a Boolean predicate then $\w \in \Span$ trivially holds (as $0,1 \in \Span$ holds). If $\op$ is not a Boolean predicate then, assume by induction hypothesis, that for each $i \leq \ell(\bar{\e})$, if $(\store,\e_i) \toe \w_i$ then $\w_i \in \Span$. It trivially holds that $\sem{\op}(\bar{\w}) \in \Span$, as $\Span$ is closed by subword.

* Case $\e' = \declass(\e_1,\e_2)$ with $(\store,\e_i) \toe \w_i$. According to the semantics of $\declass$, $\w=1^n$, for some $n \leq \size{\w_2}$. Moreover, by typing Rule (DCL), $\e_2$ is of level $\sla'_{out}$ and it holds that $\sla \ord \sla'_{out}$. Hence by induction hypothesis, $\w_2 \in \Span$. It also implies that $\w = 1^n\in \Span$.

Given a variable typing environment $\typenv$ and a level $\sla$, we define an order relation over stores by $\store \lesssim_{\sla}^\typenv \store'$ iff $\Span \subseteq \Spanp$.

For any typing subderivation $\rho \rightslice \pbl  \while (\e) \{\cmd\}: \sla$ of a safe program, for any $\store,\store'$, and $\cmd'$ such that $\pi_{(\store', \cmd')}$ is a subtree of $\pi_{(\store, \while (\e) \{\cmd\})}$, we have $\store' \lesssim_{\sla}^{\typenv} \store$.

By induction on the evaluation tree.
In the evaluation tree, the store $\store$ is updated by assignments of the form $\x \asg \e'$.
If $\typenv(\x)\ordst\sla$ and $(\store'', \e') \toe \w$, for some $\store''$ then $\Spanp = \Spanpp \subseteq \Span$, by induction hypothesis.
Otherwise $\typenv(\x) = \sla$, by Lemma <ref>.
If $(\store'', \e') \toe \w$, for some $\store''$ then $\w\in\Span$, by Lemma <ref>. Moreover, by induction hypothesis, $\store'' \lesssim_{\sla}^\typenv \store$.  Hence $\store'(\x) \in \Spanpp$ and $\store' \lesssim_{\sla}^\typenv \store''\lesssim_{\sla}^\typenv \store$.

As values in the span are linearly bounded by the size of the input store (and some constant for boolean values), we obtain the following corollary.

For any pair of typing derivations $\rho \rightslice \pbl  \while (\e) \{\cmd\}: \sla$ and $\rho' \rightslice \pblp \e' : \sla'$ of a safe program such that $\rho' \sqsubseteq \rho$ and $\sla \ord \sla'$, for any $\store,\store',\sigma,\phi,$ such that $\pi_{(\sigma, \store', \phi, \e')} \sqsubseteq \pi_{(\sigma, \store, \phi, \while (\e) \{\cmd\})}$, if $(\sigma, \store', \phi, \e') \toexp \w$ then
$$\size{\w} \leq \max(1,\max_{\y \in dom(\store) } \{\size{\store(\y)} \ | \  \sla \ord \typenv(\y)\}).$$

Let $\prog$ be a safe aperiodic terminating program. Consider an outermost while loop:
$\rho \rightslice \typenv,\typop \vdash_{\levela}^{\levela} \while(\e)\{\cmd\}:\sla$ in $\prog$.
For any subexpression $\e'$ of $\e$, from Lemma <ref>, either the level $\sla$ of $\e$ is less or equal to that of $\e'$, or $\e'$ is declassified in $\e$.
In this second case, we can write $\e=C[\declass(\e_1, \e_2)]$ for some context $C$ containing no declassification.
It implies that all expressions in $C$ have level greater or equal to $\sla$.
By Lemma <ref>, for any expression $\e'$ in $C$ and any store $\store'$ in the execution tree $\pi_{(\store, \while(\e)\{\cmd\})}$, if $(\store', \e') \toe \w$, then $\w\in\Span$
By Corollary <ref>, $(\store', \declass(\e_1, \e_2)) \toe^* 1^n\in\Span$.
There exists a constant $c$, bounded by the size of $\e$, such that
the number of distinct values that $\e$ can reach is bounded by $(\#\Span)^c$.
The aperiodicity hypothesis hence implies that the guard is evaluated at most a number of time polynomial in the size of $\store$.
Using Lemma <ref>, the values of level less than $\sla$ can increase at most polynomially in $\max_{\x}(\size{\store(\x)})$ (apply a constant increment a polynomial number of times).
Hence, we can apply the same reasoning on inner loops.
The case of sequential outer loops relies on the fact that between loops, it is possible to apply polynomial operators a constant number of times.
Hence the complexity of the program is bounded by a composition of polynomials, which is a polynomial.

§ TYPE-2 SOUNDNESS AND COMPLETENESS

For the higher-order language of section <ref>, some new lemmas are needed and some previous lemmas need modifications.

The monotonicity lemma (Lemma <ref>) and the confinement lemma (Lemma <ref>) have already been proven.

Let $\rho \rightslice \pbl \while (\e) \{\cmd\} : \sla $ be a typing subderivation of a safe program. For any $ \x \in \A(\cmd)$, $\Gamma(\x) \neq \infty$.

By the side conditions of Rules (WH) and (WI). It holds that $\sla \neq \infty$. Consequently, the result holds by applying Lemma <ref>.

In Lemma <ref>, a third case can arise when oracles appear.
Contexts are defined by the following grammar:

\begin{align*}
C, D, \ldots
\rgl &\diamond
\ |\ \op(\bar{\e}_{i,C}^{ar(\op)})  \ | \truncate(\bar{\e}_{i,C}^2) \ | \\
&  \declass(\bar{\e}_{i,C}^2)\ | \ \X (\bar{\e}_{i,C}^n) \ | \ \bar{\e}_{i,C}^n
\end{align*}

Given two expressions $\e$ and $\e'$, $\e'$ is oraculated in $\e$ if $\e=C[\X(D[\e'])]$.

In a safe program, only variables of higher level or whose occurrences are all declassified or oraculated
can be accessed when evaluating an expression.

For any triplet of typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla $, $ \rho' \rightslice  \pblp \e' : (\sla',\slb')$, and $\rho'' \rightslice \pblpp \e'' : (\sla'',\slb'')$ of a safe program, if $\rho'' \sqsubseteq \rho' \sqsubseteq \rho$, then (at least) one of the following conditions holds:

* $\sla' \ord \sla''$,

* $\e''$ is declassified in $\e'$,

* $\e''$ is oraculated in $\e'$.

Moreover, if $\e'$ is the guard of a while loop then Condition 3 cannot hold.

In the structural induction on the expression $\e'$, the cases already proved  stay true (but occurences of “declassified” are to be understood as “declassified or oraculated”).
$\truncate$ and $\X(.)$ need to be explored:

* Case $\e'=\truncate(\e^3,\d)$: is similar to the case of operators. Indeed, assume that $\sla^3$ is the level of $\e^3$. By safety, the level of $\d$ is enforced to be $_out'(=_out”)$ and it always holds that $' ≤^3 _out”$. Hence we can apply the induction hypothesis as in the previous case.
\item Case $'=()$: if $” ∈$ then $”$ is oraculated in $'$.
\end{itemize}

Now, we show that if $'$ is the guard of a while loop then either Condition 1 or Condition 2 hold. For that purpose, we show that if $”$ is oraculated then $”$ is also declassified. First notice that, by typing rules (WH) and (WI), the level of $'$ is distinct from $∞$. Assume that $”$ is oraculated in $'$. This means that there is $^3 = ()$ of level $∞$ such that  $” ∈^3$ and $^3 ∈'$ both hold. However, by definition of safe operator typing environments and by typing Rule (ORC), an operator and an oracle call cannot be applied to $^3$. A declassification cannot be applied as, by Rule (DCL), the level has to be smaller than the outermost level, which is finite. Hence for $'$ to be typed, the subexpression $()̣$ has to be truncated. However, by safety, the level of an expression $( ()̣, '̣)$ is strictly smaller than the innermost level. Hence for $'$ to type, some declassification has to be applied (at least one). Consequently, $”$ is declassified in $'$.
\end{proof}

\begin{lemma}[Stratification II]\label{lem:stratification2}
For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla'$ of a safe program such that $\rho' \sqsubset \rho$, if $\sla =\sla'$ then for each $\e'' \in \e'$, if one of the following condition holds:
\begin{itemize}
\item $\e'' = \X(\bar{\e})$,
\item $\e'' = \truncate(\d,\d')$,
\item $\e''=\op(\bar{\e})$, for some positive operator $\op$,
\end{itemize}
then $\e''$ is declassified in $\e'$.
\end{lemma}
\begin{proof}
The proof is by induction on the size of the expression $\e'$.
Consider a subexpression $\e'' \in \e'$.

i) If $\e'' = \X(\bar{\e})$, then it has level $\infty$. As such a level cannot  be assigned to in a while loop, by Lemma~\ref{lem:nonboundediterationinloops}, then $\e''$ has to be truncated for the program to type. Just note in the typing rules that $\truncate$ is the only operator allowing a flow from $\infty$ to some finite level. Hence it suffices treat case ii) under the assumption that $\e''$ cannot be oraculated, by side conditions of Rule (ORC) which prevents oracle composition.

ii) If $\e''=\truncate(\d,\d')$, then by safety, it holds that if $\e''$ is of level $\sla''$ then $\sla'' \ordst \sla'_{in}$. Consequently, $\sla'' < \sla$, by Lemma~\ref{lem:inner}. As the level of $\e'$ is greater than $\sla$ by Rule (ASG) then $\e''$ is either declassified or oraculated in $\e'$, by Lemma~\ref{lem:ss2}. The case where $\e''$ is oraculated can be treated using i).

iii) If $\e''=\op(\bar{\e})$, for some positive operator $\op$, then by definition of safe operator typing environment and by Rule (OP), it holds that if $\op(\bar{\e})$ is of level $\sla''$ then $\sla'' \ordst \sla'_{in}$. Consequently, $\sla'' < \sla$, by Lemma~\ref{lem:inner}. As the level of $\e'$ is greater than $\sla$ by Rule (ASG) then $\op(\bar{\e})$ is either declassified or oraculated in $\e'$, by Lemma~\ref{lem:ss2}. The case where $\e''$ is oraculated can be treated using i).
\qedhere
\end{proof}

\begin{lemma}[Controlled increase II]\label{lem:ci2}
For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla'$ of a safe program such that $\rho' \sqsubset \rho$, $\exists c \in \mathbb{N}$ such that $\forall (\sigma,\store,\phi) \in  ({\tt Procedures}) \times {\tt Stores} \times {\tt Env} $, if $(\sigma,\store,\phi,\e') \toexp \w$ then $$\size{\w} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c.$$
\end{lemma}
\begin{proof}
From Lemma~\ref{lem:nonboundediterationinloops}, $\typenv(\x)\neq \infty$ and the level of $\e'$ is finite.
This proof is by induction on expressions whose level is not $\infty$.
As the program is safe, by definition of safe operator typing environment (Definition~\ref{sote}), no polynomial operator can be called in $\e'$, as the corresponding assignment is inside a while loop by hypothesis ($\rho' \sqsubset \rho$). Hence its outermost level $\sla_{out}'$ is distinct from $\levela$.
\begin{itemize}
\item Case $\e' = \y$. Treated in Lemma~\ref{lem:ci}
\item Case $\e' = \op(\bar{\e})$. By rule (OP), $\forall i\leq \ell(\bar{\e})$, $\e_i$ is distinct from $\infty$, so it is as in Lemma~\ref{lem:ci}
%By induction hypothesis, if $(\sigma,\store,\phi,\e_i) \toexp \w_i$ then $$\size{\w_i} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_i.$$ By definition of neutral and positive operators, it holds that $\size{\w}=\size{\sem{\op}(\bar{\w})} \leq \max_i(\size{\w_i})+d$, for some $d \geq 0$. Hence $\size{\w} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+ \max_i c_i +d$. Take $c \triangleq \max_i c_i +d$. %In the case where $\sla = \sla'$, only neutral operators can be applied. Hence $c_i = d = c =0$.
\item Case $\e' = \declass(\e_1,\e_2)$ has been treated in Lemma~\ref{lem:ci}
\item Case $\e' = \truncate(\e_1,\e_2)$ is similar to $\declass$.
Assume $(\sigma,\store,\phi,\e_2) \toexp \w_2$ then $\size{\w_2} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_2$.
If $(\sigma,\store,\phi,\e') \toexp \w$ then by Rule (Truncate), it holds that:
\size{{\w}} \leq \size{\w_2} \leq \max_{\x \in \dom(\store)}(\size{\store(\x)})+c_2.
%If $\sla = \sla'$, then $c_2= 0$ by induction hypothesis.
%\item Case $\e'=\X(\bar{\e})$ is not possible by Lemma~\ref{lem:nonboundediterationinloops} and typing rules (ORC) and (ASG). Indeed, each oracle call has to be encapsulated in a truncate to be typed in a loop.
\end{itemize}
\end{proof}

\begin{lemma}[Bounded span II]\label{lem:bg2}
For any typing subderivations $\rho \rightslice \pbl  \while (\e) \{\cmd\} : \sla$ and $ \rho' \rightslice  \pblp \x' \asg \e' : \sla$ of a safe program such that $\rho' \sqsubset \rho$ holds, $\forall (\sigma,\store,\phi) \in \mathcal{P}({\tt Procedures}) \times {\tt Stores} \times {\tt Env} $, if $(\sigma,\store,\phi,\e') \toexp \w$ then $\w \in \Span$. %Moreover, if $(\sigma,\store,\phi,\e) \toexp \w$ then $\w \in \Span$.
\end{lemma}
\begin{proof}
The proof is the same as that of Lemma~\ref{lem:bg}, but
by induction on expressions of level distinct from $\infty$.
Cases $\e' = \truncate(\e_1,\e_2)$ and $\e' = \X(\bar{\e})$ cannot occur, by Lemma~\ref{lem:stratification2}.
%The case of the loop guard is straightforward as any loop $\while (\e) \{\cmd\}$ of a safe program is equivalent to $$\x \asg \e; \while (\x) \{\cmd; \x \asg \e\}$$ and safety is preserved for such a program for the same typing environments.
\end{proof}
\begin{lemma}[Stability II]\label{lem:stab2}
For any typing subderivation of a safe program $\rho \rightslice \pbl  \while (\e) \{\cmd\}: \sla$, for any $\store,\store',\sigma,\phi,$ and $\cmd'$ such that $\pi_{(\sigma, \store', \phi, \cmd')}$ is a subtree of $\pi_{(\sigma, \store, \phi, \while (\e) \{\cmd\})}$, we have $\store' \lesssim_{\sla}^{\typenv} \store$.
\end{lemma}
\begin{proof}
By induction on the evaluation tree.
In the evaluation tree, the store $\store$ is updated by assignments of the form $\x \asg \e'$.
If $\typenv(\x)\ordst\sla$ and $(\sigma, \store'', \phi, \e') \toexp \w$, for some $\store''$ then $\Spanp = \Spanpp \subseteq \Span$, by induction hypothesis.
Otherwise $\typenv(\x) = \sla$, by Lemma~\ref{lem:confinement}.
If $(\sigma, \store'', \phi, \e') \toexp \w$, for some $\store''$ then $\w\in\Span$, by Lemma~\ref{lem:bg2}. Moreover, by induction hypothesis, $\store'' \lesssim_{\sla}^\typenv \store$.  Hence $\store'(\x) \in \Spanpp$ and $\store' \lesssim_{\sla}^\typenv \store''\lesssim_{\sla}^\typenv \store$. \qedhere
\end{proof}
\begin{corollary}\label{coro:bound2}
For any typing derivations $\rho \rightslice \pbl  \while (\e) \{\cmd\}: \sla,\ \rho' \rightslice \pblp \e' : \sla'$ of a safe program such that $\rho' \sqsubseteq \rho$ and $\sla \ord \sla'$, for any $\store,\store',\sigma,\phi,$ such that $\pi_{(\sigma, \store', \phi, \e')} \sqsubseteq \pi_{(\sigma, \store, \phi, \while (\e) \{\cmd\})}$, if $(\sigma, \store', \phi, \e') \toexp \w$ then $$\size{\w} \leq \max(1,\max_{\y \in dom(\store) } \{\size{\store(\y)} \ | \  \sla \ord \typenv(\y)\}).$$
\end{corollary}
\subsubsection*{Polynomial Step Count.}\label{ss:psc}
In this section, we show that safe and aperiodic terminating programs have a runtime polynomially bounded by the size of the input store and the maximal size of answers returned by the oracle in the course of evaluation.

\begin{definition}
Given a program $\prog$, an input store $\store\triangleq \store_\emptyset[\bar{\x} \leftarrow \bar{\w},\bar{\X} \leftarrow \bar{f}]$, and a procedure $\proc$ of $\prog$,
let $m_{\store}^{\prog,\proc}$ be the maximum of $\size{\store}$ and the maximum size of an oracle answer in any subderivation $\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))}$ of $\pi_{(\emptyset,\store,\prog)}$.
%Formally, $$m_{\store}^{\prog,\proc} =\max(\size{\store}, \max_{\scalebox{0.8}{\begin{tabular}{c}$\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \sqsubseteq \pi_{(\emptyset,\store,\prog)}$ \\ $(\w,f) \in C(\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))})$\end{tabular}}}\{\size{\w};C(\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \}),$$
Formally, \begin{align*}
or_{\store}^{\prog,\proc} &\triangleq \max_{\scalebox{0.8}{$\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \sqsubseteq \pi_{(\emptyset,\store,\prog})$ }}\{\size{\w};\w\in C(\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))})\} \\
&\text{where }C(\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))})\text{ is the set of }\w\text{ such that:}\\
& \scalebox{1}{\begin{prooftree}
\hypo{\cdots}
\infer1[(Orc)]{(\sigma,\store,\phi \Imp \X(\bar{\e})) \toexp \w}
\end{prooftree}}
\in \pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))}\\
m_{\store}^{\prog,\proc} &\triangleq \max(\size{\store}, or_{\store}^{\prog,\proc})
\end{align*}

A procedure $\proc$ of the program $\prog$ has \emph{Polynomial Step Count} if there is a polynomial $Q \in \mathbb{N}[X]$ such that for any input store $\store$ and any $\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \sqsubseteq \pi_{(\emptyset,\store,\prog)}$, $\#\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \leq Q (m_{\store}^{\prog,\proc}).$
\end{definition}

A procedure with Polynomial Step Count terminates in time polynomial in the size of the initial store and the maximal size of an oracle answer.

\begin{theorem}\label{thm:pol}
Each procedure $\proc$ of a program in $\safe \cap \ASN$ has Polynomial Step Count.
\end{theorem}

\begin{proof}
Let $\prog\in \safe\cap\ASN$.
%Let us consider the break-free program $\prog^{\star}$.
Now consider a procedure $\proc$ of $\prog$.
Consider an outermost while loop $\rho \rightslice \pbl  \while (\e) \{\cmd\}:\sla$ of a procedure $\proc$ in $\prog$. For any subexpression $\e' \in \e$, by Lemma~\ref{lem:ss2}, either the level of $\e'$ is greater than the level $\sla$ of $\e$ or $\e'$ is declassified in $\e$. Hence $\e$ can be written as follows $e=C[\bar{\declass(\e_1,\e_2)}]$, for some context $C$ with no declassification (note: $C$ is the straightforward extension of contexts to multiple hole contexts). In particular, this implies that any expression $\e'$ in $C$ has level greater than $\sla$.
By Lemma~\ref{lem:stab2}, for any expression $\e'$ in $C$ and any store $\store'$ (obtained from the input store $\store$) if $(\sigma,\store',\phi,\e') \toexp \w$ then $\w \in \Span$.
By the semantics of $\declass$ and by Corollary~\ref{coro:bound2}, it also holds that each $\declass(\e_1,\e_2)$ is evaluated to a unary value in $\Span$, for each store obtained from the input store $\store$.
Consequently, the number of distinct values that $\e$ can take is then bounded by $(\#\Span)^c$, for some constant $c$ bounded by the size of the program, which is polynomial in $\size{\store}$.
Indeed, if the loop is to be taken more than $(\#\Span)^c$ times, it means that the same configuration for variables of level at least $\sla$ in $C$ and $\declass(\e_1,\e_2)$ is visited twice, contradicting the II-aperiodicity hypothesis. Consequently, this while loop can be unfolded polynomially many times. By Lemma~\ref{lem:ci2}, the values stored in statements of level strictly smaller than $\sla$ can increase at most polynomially (i.e., polynomially many times by a constant) in $\size{m_{\store}^{\prog}}$. The same reasoning can be performed on nested loops of level smaller (non-strictly) than $\sla$. Hence the outermost loop has Polynomial Step Count, where the polynomial is a composition of finitely many polynomials, whose number is bounded by the number of nested loops.
Finally, by an induction on the number of sequential outermost loops in the procedure $\proc$, we conclude that $\proc$ has Polynomial Step Count.
\qedhere
\end{proof}

A direct corollary is that each procedure call of a program in $∩$ can be simulated by an OTM in $$.

\subsubsection*{Finite Length Revision.}\label{ss:flr}
In this section, we show that aperiodic, terminating, and safe programs can only perform a constant number of oracle calls whose answer is  of increasing size with respect to previous calls.

%We first start to show that the outermost level of a statement of a safe and guarded program is an upper bound on the levels of while loop expressions guarding this statement.
%Let $\rho$ be a typing derivation of a safe and guarded program with respect to the typing environments $\typenv,\typop$.
%For any $\rho_1 \rightslice \pbl  \while (\e_1) \{\cmd_1\} : (\sla^1,\sla^1_{in},\sla^1_{out}) (R) \sqsubseteq \rho$ and $ \rho_2 \rightslice \pbl \cmd_2 : (\sla^2,\sla^2_{in},\sla^2_{out}) \sqsubseteq \rho_1$,
%if $R \in \{W,W_0\}$ then $\sla^1 \ord \sla^2_{out} $.
%\footnote{The assumption for the last rule of $\rho_1$ to be in $\{$W,W$_0\}$ ensures that $\sla^1$ is exactly the level of the guard expression $\e_1$. Otherwise typing Rule (SUB) can be applied arbitrarily and the result does not hold.}
%The typing Rule (W$_0$) is the only rule changing the outermost level. It is straightforward to observe that this rule can only be applied to an outermost while loop as the outermost level of the statement is updated from $\levela$ to $\sla$, for some $\sla$ such that $\levelb \ord \sla$.
%There are two cases to consider depending on $R$:
%\item if R=W then
%\hypo{\rho'_1 \rightslice \pbl \cmd_1 : (\sla^1,\sla^1,\sla^1_{out})}
%\hypo{\levelb \ord \sla^1 \ord \sla^1_{out}}
%\infer3[(W)]{\rho_1 \rightslice \pbl  \while (\e_1) \{\cmd_1\}\ :(\sla^1,\sla^1_{in},\sla^1_{out})}
%Clearly, $\sla^1 \ord \sla^1_{out}= \sla^2_{out}$ by the guard condition and as $\rho_2 \leq \rho'_1$ and all the rules under a while preserve the outermost level.
%\item if R=W$_0$ then
%\hypo{\rho'_1 \rightslice \pbl \cmd_1 : (\sla^1,\sla^1,\sla^1 )}
%\hypo{\levelb \ord \sla^1  }
%\infer3[(W$_0$)]{\rho_1 \rightslice \pbl  \while (\e_1) \{\cmd_1\}\ :(\sla^1,\sla^1_{in},\levela)}
%It is straightforward that $\sla^1 = \sla^2_{out}$  as $\rho_2 \leq \rho'_1$ ($\rho_2 \in \mathring{\D}(\rho_1)$) and all the rules under a while preserve the outermost level.\qedhere

Given a sequence $(u_n)$, define the length revision of $(u_n)$ as $lr((u_n)) ≜#{i  |  u_i >max_j < i(u_j)}.$
Given a program $$, an input store $≜_∅[ ←, ←f̅]$, a procedure $$ of $$, and an evaluation tree $π_(σ,',(,)) ⊑π_(∅,,)$, let $(l^π_(σ,',(,))_n)$ be the sequence of output values $$ in (Orc) rules in $π_(σ,',(,))$ except those appearing in a subtree of root indexed by Rules (Brk$_⊤$) or (Brk$_$), and that are obtained by a left-to-right depth-first traversal of the evaluation tree $π_(σ,',(,))$.

Note the left-to-right depth-first traversal in a derivation exactly corresponds to the order of a sequential execution of a statement.
Hence $(l^π_(σ,',(,))_n)$ corresponds to the sequence of calls to oracles in $$ that do not occur in the guard of a break statement. Oracle answers in break statements do not need to be taken into account for the result to hold as it is only necessary to read a fixed size prefix of the oracle answer to decide whether to break.

\begin{definition}
A procedure $\proc$ of the program $\prog$ has \emph{Finite Length Revision} if there is a constant $n\in\mathbb{N}$ such that for each input store $\store$ and any $\pi_{(\sigma,\store',\callcc\proc(\bar{\clos},\bar{\term}))} \sqsubseteq \pi_{(\emptyset,\store,\prog)}$, $lr((l^{\pi_{(\sigma,\store',\callcc \proc(\bar{\clos},\bar{\term}))}}_n)) \leq n$.
\end{definition}

\begin{theorem}\label{thm:flr}
Each procedure of a program in $\safe $ has  Finite Length Revision.
\end{theorem}

\begin{proof}