Higher-Order MSL Horn Constraints

2025-05-06 0 0 704.88KB 56 页 10玖币

侵权投诉

arXiv:2210.14649v1 [cs.PL] 26 Oct 2022

JEROME JOCHEMS, University of Bristol, UK

EDDIE JONES, University of Bristol, UK

STEVEN RAMSAY, University of Bristol, UK

The monadic shallow linear (MSL) class is a decidable fragment of ﬁrst-order Horn clauses that was discovered and rediscovered

around the turn of the century, with applications in static analysis and veriﬁcation. We propose a new class of higher-order Horn

constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn

constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which

make them well suited to higher-order program veriﬁcation. In fact, we show that the higher-order MSL satisﬁability problem and

the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to

higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to veriﬁed socket

programming.

Additional Key Words and Phrases: higher-order program veriﬁcation, constraint-based program analysis

1 INTRODUCTION

Constraints of various kinds form the basis of many program analyses and type inference algorithms. Specifying an

analysis as a combination of generating and resolving constraints is very appealing: as Aiken [1999] remarks in his

overview paper, constraints help to separate speciﬁcation from implementation, they can yield natural speciﬁcations and

their often rich theory (typically independent from the problem at hand) can enable sophisticated optimisations that

may not be apparent if stating the analysis algorithm directly.

To realise these advantages, we want classes of constraints that can naturally express important features of the

problem domain, that draw upon a well-understood theory and yet have a decidable satisﬁability problem.

In this work we propose a new class of constraints that are designed to capture the complex, higher-order behaviours

of programs with ﬁrst-class procedures. We develop a part of the theory of these constraints and situate them in

relation to other higher-order program analyses. Finally, we obtain an eﬃcient decision procedure and we describe an

application of the constraints to automatic veriﬁcation of socket programming in a functional programming language.

1.1 MSL Horn constraints

Our constraints can be framed as an extension of the well-known Monadic Shallow Linear (MSL) Horn constraints

to higher-order logic. Like many natural ideas, MSL constraints were discovered independently in two diﬀerent com-

munities. At CADE’99, Weidenbach [1999] proposed MSL Horn constraints as a natural setting in which to “combine

the beneﬁts of the ﬁnite state analysis and the inductive method”, he showed that satisﬁability was decidable and de-

scribed how this class of constraints could be used in an automatic analysis of security protocols. Independently, at

SAS’02, Nielson, Nielson, and Seidl [2002] proposed the H1 class of Horn constraints, and it was later observed by

[Goubault-Larrecq 2005] to be an equivalent reformulation of MSL. The H1 class was originally used for the control

ﬂow analysis of the Spi language, but has also been applied to e.g. the veriﬁcation of cryptosystems written in C.

Authors’ addresses: Jerome Jochems, Department of Computer Science, University of Bristol, Bristol, UK, jerome.jochems@bristol.ac.uk; Eddie Jones,

Department of Computer Science, University of Bristol, Bristol, UK, ej16147@bristol.ac.uk; Steven Ramsay, Department of Computer Science, University

of Bristol, Bristol, UK, steven.ramsay@bristol.ac.uk.

2 Jerome Jochems, Eddie Jones, and Steven Ramsay

MSL is the fragment of ﬁrst-order Horn clauses obtained by restricting predicates to be monadic and restricting

the subject of positive literals to be shallow and linear – that is, the single argument of a predicate in the head of a

clause must be either a variable 𝑥or a function symbol applied to distinct variables 𝑓(𝑥1, . . . , 𝑥𝑛). In practice, because

we can view the function symbol 𝑓as constructing a tuple (𝑥1, . . . , 𝑥𝑛), it is convenient to also allow non-monadic

predicates, so long as they are only applied to variables when used positively: 𝑃(𝑥1, . . . , 𝑥𝑛). With this concession, all

of the following are MSL Horn clauses (we omit the preﬁx of universal quantiﬁers in each case):

Zero(𝑥) ⇒ Leq(𝑥, 𝑧)Leq(s(𝑥),s(𝑦)) ⇒ Leq(𝑥, 𝑦)Leq(𝑥, 𝑦) ∧ Leq(𝑦, 𝑧) ⇒ Leq(𝑥, 𝑧)

Black(leaf)Black(branch(𝑥, 𝑑, 𝑧)) Black(𝑥) ∧ Black(𝑧) ⇒ Red(branch(𝑥, 𝑑, 𝑧))

M(sent(𝑦, b,pr(encr(tr(𝑦, 𝑥, tb(𝑧)),bt),encr(nb(𝑧), 𝑥)))) ∧ Sb(pr(𝑦, 𝑧)) ⇒ Bk(key(𝑥, 𝑦))

Note: there are no syntactical restrictions on the body of clauses. As can be seen in the last example, which is taken

from Weidenbach’s security protocol analysis, atoms in the body may contain terms with arbitrary nesting.

Sets of MSL clauses were shown by Weidenbach to have decidable satisﬁability. The procedure is an instance of

ordered resolution, with a carefully crafted ordering that guarantees terminating saturation. Essentially the same pro-

cedure was rediscovered independently by Goubault-Larrecq, as he sought to construct a more standard procedure

than Nielsen, Nielsen and Seidl’s original, which was a bespoke kind of constraint normalisation.

In each case, the authors identify a key, solved form for constraints. Clauses in this solved form have shape: 𝑄1(𝑦1)∧

· · · ∧𝑄𝑘(𝑦𝑘) ⇒ 𝑃(𝑓(𝑥1, . . . , 𝑥𝑚)) with {𝑦1, . . . , 𝑦𝑘} ⊆ {𝑥1, . . . , 𝑥𝑚}. A set of clauses of this form can straightforwardly

be viewed as an alternating tree automaton and so such clauses are called automaton clauses. Given as input a set of MSL

Horn constraints C, each of the above decision procedures can be viewed as constructing a set of automaton clauses

Aequisatisﬁable with C, and since Ais essentially a tree automaton, its satisﬁability can be eﬀectively determined.

1.2 Contributions of this paper

In this work, we propose three diﬀerent higher-order extensions of MSL constraints: (i) the class HOMSL(1) obtained by

allowing predicates of higher types but maintaining the limitation of ﬁrst-order function symbols, (ii) the class MSL(𝜔)

obtained by allowing for function symbols of higher-types but maintaining the limitation of ﬁrst-order (monadic)

predicates and (iii) the class HOMSL(𝜔) obtained by allowing for both predicates and function symbols of higher type.

I. Reduction to existential-free MSL(𝜔). Our ﬁrst contribution is to show that the satisﬁability problem for all of the

above classes reduces to the satisﬁability problem for a fragment of MSL(𝜔)– i.e. ﬁrst-order predicates only – in which

formulas contain no existential quantiﬁcation. We show that existential quantiﬁers are, in a sense, already deﬁnable

using higher-order predicates and that higher-order predicates in general can be represented as higher-order functions,

whose truth is internalised as a new ﬁrst-order predicate.

II. Decidability of MSL(𝜔). Our second contribution is to give a resolution-based algorithm for deciding the satisﬁa-

bility problem of MSL(𝜔). A key diﬃculty in generalising the resolution-based decision procedure for the ﬁrst-order

fragment is what to do about negative literals whose subject is headed by a variable 𝑃(𝑥 𝑠1· · · 𝑠𝑛). Literals of this form

simply cannot occur in the ﬁrst-order case, and allowing (higher-order) resolution on such literals creates clauses that

violate one of the cornerstones of the decidability result at ﬁrst-order, namely that clause heads are shallow.

We introduce a novel kind of higher-order resolution which avoids this phenomenon, but it necessitates a signiﬁ-

cantly diﬀerent notion of automaton formula (solved form), which nevertheless specialises to the existing deﬁnition

Higher-Order MSL Horn Constraints 3

at ﬁrst-order. A simple type system for automaton clauses ensures that the level of nesting and the binding structure

of variables is in tight correspondence with the type theoretic order of the function symbols involved. Consequently,

as in the ﬁrst-order case, there can be only ﬁnitely many automaton clauses associated with a given problem instance,

and this forms the backbone of the decidability proof.

III. Interreducibility of MSL(𝜔), HORS model checking, and intersection (reﬁnement) typeability. Although they look

superﬁcially complex, it is easy to see that our higher-order automaton clauses, viewed as constraints, are in 1-1

correspondence with a simple kind of intersection types used in higher-order model checking. Since it is known that

this class of intersection types deﬁne regular tree languages [Broadbent and Kobayashi 2013], the name automaton

clauses is still justiﬁed. Our third contribution is to use this correspondence to moreover give two problem reductions:

(i) from MSL(𝜔) satisﬁability to HORS model checking and (ii) from intersection typeability to MSL(𝜔) satisﬁability.

The reduction from HORS model checking to intersection typeability is already well known [Kobayashi 2013], and thus

completes the cycle. We obtain from these reductions that MSL(𝜔) satisﬁability is (𝑛−1)-EXPTIME hard for 𝑛≥2

(here 𝑛refers to the type theoretic order of the function symbols). This is the class of problems that can be solved in

time bounded by a tower of exponentials of height-𝑛.

IV. Application to veriﬁed socket programming. As proof of concept, we have implemented our prototype decision

procedure in Haskell and applied it to the higher-order veriﬁcation problem of socket usage in Haskell programs. In-

terestingly, our extraction of clauses from a Haskell program does not analyse the source code directly. Instead, the

domain-speciﬁc language is represented as a typeclass that can be instantiated with a speciﬁc “analysis” instance that

extracts a representation of the program to be passed to our decision procedure in addition to the usual IO implemen-

tation. The principle advantage of this approach is that the source code need not be present, making way for library

functions to appear freely. Furthermore, it is easier to implement and maintain as orthogonal concerns in the source

code need not be explicitly handled that have no natural encoding with clauses. As far as we are aware, this technique

is novel and could be fruitfully applied to other domains.

1.3 Wider significance

In ﬁrst-order automated program veriﬁcation there is a consensus around ﬁrst-order logic as foundation, to the beneﬁt

of the ﬁeld. On the one hand, ideas from ﬁrst-order logic, such as interpolants, the Horn fragment, abduction, reso-

lution and so on have found an important place in automated veriﬁcation. On the other, ﬁrst-order logic provides a

common vocabulary with which to understand the automated veriﬁcation landscape conceptually, and locate diﬀerent

technologies.

However, in higher-order automated program veriﬁcation there are only a disparate collection of formalisms: reﬁne-

ment types [Rondon et al. 2008;Terauchi 2010;Unno and Kobayashi 2009;Vazou et al. 2015,2013;Zhu and Jagannathan

2013], higher-order grammars/automata [Hague et al. 2008;Kobayashi 2013;Kobayashi and Ong 2009;Ramsay et al.

2014;Salvati and Walukiewicz 2016], ﬁxpoint logic [Bruse et al. 2021;Kobayashi 2021;Viswanathan and Viswanathan

2004], and many others. Moreover, the procedures involved are often bespoke and diﬃcult to relate to techniques that

are standard in ﬁrst-order veriﬁcation.

This paper is part of a larger eﬀort to establish an analogous foundation for higher-order automated program veri-

ﬁcation based on higher-order logic [Cathcart Burn et al. 2017,2021;Jochems 2020;Ong and Wagner 2019]. We have

shown that a standard technique from ﬁrst-order automated reasoning, namely saturation under resolution, is eﬀective

4 Jerome Jochems, Eddie Jones, and Steven Ramsay

at higher-order, and even forms a decision procedure for the higher-order extension of MSL. Furthermore, in combina-

tion with our correspondence between intersection types and higher-order automaton clauses, this sets up a pattern

for understanding type-based approaches to veriﬁcation more generally.

Our interreducibility results allow us to situate higher-order model checking (also known as HORS model checking)

conceptually, within the HOL landscape. This is beneﬁcial because HORS model checking, although inﬂuential, is a set

of techniques for solving a somewhat exotic problem. The safety version of the problem asks to decide if the value tree

determined by a certain kind of higher-order grammar is accepted by a Büchi tree automaton with a trivial acceptance

condition [Kobayashi 2013]. Thanks to the results of this paper, this form of higher-order model checking can be

located more simply as “a group of decision procedures for the MSL fragment”. We hope this will make this topic more

accessible to the wider veriﬁcation community, since monadic, shallow, and linear restrictions are well understood

even by non-experts on higher-order program veriﬁcation.

Our results also make an interesting connection with work on constructive logic and logic programming. Our higher-

order automaton formulas are a special form of higher-order hereditary Harrop clauses (HOHH), lying in the intersec-

tion of HOHH goal and deﬁnite formulas. The fact that we have shown them to play an essential role in characterising

satisﬁability for this class of higher-order Horn clauses sheds a novel light on the relationship between these two

classes of formulas, which have been instrumental in the work of Miller and his collaborators [Miller and Nadathur

2012;Miller et al. 1991]. Furthermore, our intersection type and higher-order automaton clause correspondence sug-

gests an alternative to the “Horn Clauses as Types” interpretation pioneered by Fu, Komendantskaya, and coauthors

[Farka 2020;Fu and Komendantskaya 2015,2017;Fu et al. 2016]. Instead of identifying Horn clauses and types, reso-

lution and proof term construction, our work casts types as monadic predicates, represented as HOHH clauses with a

single free variable, and saturation-under-resolution as type inference.

1.4 Outline

The paper is structured as follows. In Section 2we introduce higher-order MSL Horn constraints and their proof sys-

tem, and we give an example of their use in verifying lazy IO computations. In Section 3we reduce the provability

problem for HOMSL(𝜔) to the same problem for existential-free MSL(𝜔). In Section 4we introduce higher-order au-

tomaton clauses and use them in deciding satisﬁability (via goal-formula entailment). In Section 5, we show that the

MSL(𝜔) satisﬁability and HORS model checking are interreducible. In Section 6we describe our implementation and

its application. Finally, in Section 7we conclude with a description of related and future work. All proofs are available

in the appendix of this paper.

2 HIGHER-ORDER MSL HORN FORMULAS

The logics we consider will make a type-level distinction between predicates and the subjects that they classify. In the

ﬁrst-order case, the subjects will be terms built from a certain signature of function symbols and constants.

Deﬁnition 2.1 (Syntax of types). We consider a subset of simply typed applicative terms. Starting from the atomic

type of individuals 𝜄and the atomic type of propositions 𝑜, the types are given by:

(Constructor Types) 𝛾F𝜄|𝜅→𝛾

(Constructor Arg Types) 𝜅F𝛾

(Predicate Types) 𝜌F𝑜|𝜎→𝜌

(Predicate Arg Types) 𝜎F𝜅|𝜌

We use 𝜏as a metavariable for types in general (i.e. that may belong to any of the above classes). Thus, the constructor

types are just the simple types built over a single base type 𝜄, and the predicate types are those simple types with an 𝑜

Higher-Order MSL Horn Constraints 5

(Var) 𝑥:𝜏∈Δ

Δ⊢𝑥:𝜏(Cst) 𝑐:𝛾∈Σ

Δ⊢𝑐:𝛾(Pred) 𝑃:𝜌∈Π

Δ⊢𝑃:𝜌

(True) Δ⊢true :𝑜

Δ⊢𝑠:𝜏1→𝜏2Δ⊢𝑡:𝜏1

(App) Δ⊢𝑠 𝑡 :𝜏2

Δ⊢𝐺:𝑜Δ⊢𝐻:𝑜

(And) Δ⊢𝐺∧𝐻:𝑜

Δ, 𝑥 :𝜎⊢𝐺:𝑜

(Ex) 𝑥∉dom(Δ)

Δ⊢ ∃𝑥:𝜎. 𝐺 :𝑜

Δ,𝑦:𝜎⊢𝐺:𝑜Δ, 𝑦:𝜎⊢𝐴:𝑜

(Cl) Δ⊢ ∀𝑦:𝜎 . 𝐺 ⇒𝐴

Fig. 1. Typing of terms, goals and clauses

in tail position (i.e. that are ultimately constructing a proposition) and whose arguments are either other predicates or

constructors. The introduction of the metavariable 𝜅seems unmotivated, but we will later place restrictions on 𝜅that

diﬀer from those on 𝛾more generally. We deﬁne the order of a type as follows:

ord(𝜄)=ord(𝑜)=0ord(𝜏1→𝜏2)=max(ord(𝜏1) + 1,ord(𝜏2))

After introducing terms below, we will say that the order of a typed term is the order of its type.

Deﬁnition 2.2 (Terms, Clauses and Formulas). In all that follows, we assume a ﬁnite signature Σof typed function

symbols and a ﬁnite signature Πof typed predicate symbols. We use 𝑎, 𝑏, 𝑐 and other lowercase letters from the be-

ginning of the Roman alphabet to stand for function symbols and 𝑃, 𝑄, 𝑅 and so on to stand for predicates. Function

symbols have types of shape 𝛾and predicate symbols have type of shape 𝜌.

Terms. We assume a countably inﬁnite set of variables. We use lowercase letters 𝑥, 𝑦, 𝑧 and so on to stand for variables.

Atype context, typically Δ, is a ﬁnite, partial function from variables to types. Then terms, typically 𝑠, 𝑡, 𝑢, are given by

the following grammar:

(Term) 𝑠, 𝑡, 𝑢 F𝑥|𝑐|𝑃|𝑠 𝑡

We will only consider those terms that are well typed according to the system speciﬁed in Figure 1, where (Ex) instan-

tiates one variable at a time for convenience.

Since we work in higher-order logic, the syntactic category of terms includes both objects that we think of as

predicates (which have type 𝜌) and those that we think of as strictly the subjects of predicates (which have type 𝛾). To

make the discussion easier, we will typically refer to terms of the former type as predicates and terms of the latter type

𝛾as trees, or tree constructors.

The depth of a symbol 𝑥,𝑐or 𝑃is 0 and the depth of an application 𝑠 𝑡 is the maximum of the depth of 𝑠and the

depth of 𝑡with 1 added.

Formulas. The atomic formulas, typically 𝐴and 𝐵, are just those terms of type 𝑜. We deﬁne the goal formulas and

deﬁnite formulas by mutual induction using the following grammar:

(Goal Formula) 𝐺, 𝐻 F𝐴|𝐺∧𝐻| ∃𝑥:𝜎. 𝐺 |true

(Definite Formula) 𝐶, 𝐷 F∀𝑦:𝜎 . 𝐺 ⇒𝑃 𝑦 | ∀𝑦:𝜎 . 𝐺 ⇒𝑃(𝑐 𝑦) | 𝐶∧𝐷|true

Wherever possible we will omit the explicit type annotation on binders and we write FV(𝑋)to denote the typed free

variables of some term, clause or formula 𝑋. We identify formulas up to renaming of bound variables.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

arXiv:2210.14649v1[cs.PL]26Oct2022Higher-OrderMSLHornConstraintsJEROMEJOCHEMS,UniversityofBristol,UKEDDIEJONES,UniversityofBristol,UKSTEVENRAMSAY,UniversityofBristol,UKThemonadicshallowlinear(MSL)classisadecidablefragmentofﬁrst-orderHornclausesthatwasdiscoveredandrediscoveredaroundtheturnofthecentur...

展开>> 收起<<

Higher-Order MSL Horn Constraints.pdf

共56页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Higher-Order MSL Horn Constraints

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: