10.6092/issn.1972-5787/9757
We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF, which feature "lock"-type constructors, and on the new perspectives offered by its novel "shallow" implementation in Coq. The L^P(N:sigma)[.] constructor, and its binding variant L^P(?x:sigma)[.], capture monadically the concept of  inhabitability up-to. They were originally introduced  for  factoring-out, postponing, or delegating to  external tools the verification of time-consuming judgments, which are "morally" proof-irrelevant, thus allowing for integrating different sources of epistemic evidence in a unique Logical Framework.Experimenting with "locks" has shown that they are also a very flexible tool for expressing in Type Theory several diverse cognitive attitudes and mental strategies used in ordinary reasoning. These range from the emerging paradigm of  "fast and loose reasoning", which trades off efficiency for correctness, as in naive Set Theory, or in computer architecture and distributed systems, when branch prediction and optimistic concurrency control are implemented. Lock-types naturally express also Typical Ambiguity provisos, "squash"' types, and many forms of "reasoning-up-to".
application/pdf
1972-5787
9757
1
en
Ivan Scagnetto
Journal of Formalized Reasoning
Computer Aided Formal Reasoning
LF+ in Coq for "fast and loose" reasoning
Text.Serial.Journal
https://jfr.unibo.it/
12
Articles
2020-01-09
2019-08-06
2019-02-19
2020-02-19
11 - 51
JFR
Ivan Scagnetto
2019
10.6092/issn.1972-5787/9757
11
University of Udine
1972-5787
1
Computer Aided Formal Reasoning
en
51
[Uni13] T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
LF+ in Coq for "fast and loose" reasoning
https://jfr.unibo.it/article/download/9757/10375
12
LF+ in Coq for fast-and-loose reasoning
FABIO ALESSI, ALBERTO CIAFFAGLIONE, PIETRO DI GIANANTONIO, FURIO
HONSELL, MARINA LENISA, and IVAN SCAGNETTO
Department of Mathematics, Computer Science and Physics, University of Udine1 , Italy


We develop the metatheory and the implementation, in Coq, of the novel logical framework LF+
and discuss several of its applications. LF+ generalises research work, carried out by the authors
over more than a decade, on Logical Frameworks conservatively extending LF and featuring lock-
type constructors LP(N :σ) J·K. Lock-types capture monadically the concept of inhabitability up-to.
They were originally introduced for factoring-out, postponing, or delegating to external tools the
verification of time-consuming judgments, which are morally proof-irrelevant, thus allowing for
integrating different sources of epistemic evidence in a unique Logical Framework. Besides intro-
ducing LF+ and its “shallow” implementation in Coq, the main novelty of the paper is to show
that lock-types are also a very flexible tool for expressing in Type Theory several diverse cognitive
attitudes and mental strategies used in ordinary reasoning, which essentially amount to reasoning
up-to, as in e.g. Typical Ambiguity provisos or co-inductive Coq proofs. In particular we address
the encoding of the emerging paradigm of fast-and-loose reasoning, which trades off efficiency for
correctness. This paradigm, implicitly used normally in naı̈ve Set Theory, is producing consid-
erable impact also in computer architecture and distributed systems, when branch prediction and
optimistic concurrency control are implemented.




1.   INTRODUCTION
The Logical Framework LF+ is a conservative extension of LF. It builds on [HLMS17],
but in fact it stems from a research line on conservative extensions of the Edin-
burgh Logical Framework [HHP93] started more than a decade ago by the authors,
together with L. Liquori, P. Maksimović, and V. Michielini, see [HLL07, HLLS08,
HLL+ 12, Hon13, HLS14, HLMS15, HLS+ 16, HLLS16, HLMS18]. These systems
have been introduced prudentially and incrementally with two goals in mind:
— integrating, in a unique Logical Framework, different epistemic sources of ev-
 idence deriving from special-purpose tools and oracles, or even non-apodictic
 sources such as, e.g. explicit computations according to the Poincaré Principle
 [BB02], deduction up-to, diagrams, physical analogies;
— factoring-out, postponing, delegating, or running in parallel the verification of
 morally proof-irrelevant and time-consuming judgments and side conditions.
In the course of the research we came to the conclusion that all these issues could be
dealt with conveniently using a notion of lock-type constructor, LP(N :σ) J·K, which
can be naturally construed as a monad, see Section 3.
  Recent experiments (see [ACDG+ 19b]) show that lock-types are a very flexible
tool also for expressing in Type Theory a wide gamut of diverse mental strategies
and cognitive attitudes used in ordinary reasoning, which generalise the above goals,
and which can be generally referred to as reasoning up-to. One can say, indeed,

1 Work supported by the Italian Departmental Research Project “LambdaBridge” (D.R.N. 37
427/2018 of 03/08/2018, University of Udine).
                                              Journal of Formalized Reasoning Vol.12, No.1, Pages 11–51.
12     ·     Fabio Alessi et al.

that the LP(N :σ) J·K type constructor expresses a very general notion of inhabitability
up-to.
   LF+ extends the expressive power of the lock-type systems available of the previ-
ous frameworks, while streamlining and simplifying the rule-system and notation.
The present paper includes an, almost self-contained, introduction to lock-types
using the novel system LF+ . We discuss in detail the monadic nature of locks and
give a rather complete and visionary overview of existing and possible applications
of lock-types.
   The main novelty of this paper is that of using LF+ to address the formalisation
of the emerging paradigm of fast-and-loose reasoning, [DHJG06]. This paradigm
trades off efficiency for correctness and amounts to postponing, or running in par-
allel, tedious or computationally demanding checks, until we are really sure that
the intended goal can be achieved. At logical level this paradigm amounts to the
ordinary practice in everyday Mathematics based on naı̈ve Set Theory or Cate-
gory Theory, when potentially large objects are freely mentioned, see [HLLS16],
or when conjecturing or introducing blanket assumptions to be checked or for-
malised later. The latter is often carried out also in program development, see
e.g. [DHJG06, HLLS16]. At the level of implementations natural examples of this
paradigm occur in Computer Architecture and Concurrency Control, i.e. branch
prediction in CPUs [JKL00] and optimistic concurrency control in distributed sys-
tems [KR81]. In both cases efficiency is improved by forgetting, i.e. running in
parallel, time-demanding tests which otherwise would significantly slow down the
computation, if carried out sequentially. Of course in the event that the outcome of
the test is negative there might be an extra cost for backtracking and restoring the
original context. But the trade-off in speed when this does not occur compensates
significantly this drawback.
   Another important contribution of this paper is a prototype implementation of
LF+ , which supports also mechanised proof search. This is crucial if we want
to explore the above paradigms using a logical framework. The implementation
is achieved through a careful shallow encoding of LF+ in the Coq proof assistant.
“Shallow” in this context means that we delegate as much as possible the mechanics
of LF+ to the metalanguage of the host system. Actually lock-types are rendered as
a Coq Definition. This is quite interesting in itself, both in exposing the principles
underpinning lock-types as well as for the bearing it has on proving that predicates
are well-behaved. Of course, everything relies on an appropriate adequacy result
(see Theorem 5.1).
   In this paper we carry out three detailed case studies. The first is the paradig-
matic call-by-value λ-calculus, the other two are the completely novel case stud-
ies pertaining to the fast-and-loose reasoning paradigm, namely branch prediction
for URM machines (see [Cut80]) and optimistic concurrency control for a sim-
ple programming language, which we call STL (i.e. Simple Transaction Language)
[CDK02].
   Many intriguing issues arise in connection with the latter examples: e.g. can we
short-cut reasoning on different nested locks? What is the correct way of expressing
adequacy when dealing with reasoning up-to? How do we express the adequacy of a
branch prediction protocol ? We outline possible answers to some of these questions.
   In Section 2 we introduce LF+ and we discuss its differences w.r.t. LLFP . In
Journal of Formalized Reasoning Vol.12, No.1
                                      LF+ in Coq for fast-and-loose reasoning       ·     13

Section 3 we explain the monadic nature of locks. In Section 4 we present a gamut of
logical contexts and attitudes which have benefitted or would benefit by an analysis
in terms of locks. In Section 5 we give a shallow definitional implementation in Coq
of LF+ and CLLFP? . The paradigmatic case-study of call-by-value λ-calculus is
implemented in Section 6. Section 7 is a brief discussion of the fast-and-loose
reasoning paradigm and serves as an introduction to the following two sections.
In these we present two massive case-studies, namely: branch prediction for URM
machines [Cut80], and optimistic concurrency control. We briefly discuss future
directions in Section 10. The web appendix of the paper is online at [ACDG+ 19b].
   The authors express their gratitude to F. Rabe and to the anonymous referees
of this paper and of a preliminary version presented at LFMTP 2019 [ACDG+ 19a]
for their helpful suggestions.

2.    THE LF+ LOGICAL FRAMEWORK
The reader familiar with [HLMS17] can read only Subsection 2.3, while the reader
familiar with Type Theory in general can skip both Subsections 2.2 and 2.3.
2.1   The System and its Intuition
In this section, following the standard pattern and conventions of [HHP93], we
introduce the syntax and the rules of LF+ . In Figure 1, we give the syntactic
categories of LF+ , namely signatures, contexts, kinds, families (i.e. types), and
objects (i.e. terms). The language is essentially that of classical LF [HHP93], to
which we add the lock-types constructor (L) for building types of the shape LC JρK,
where C ≡ P(U : V ) is a predicate P on the entity U classified by V , which can
either be a term M and its type σ, or a type σ and its kind K. The predicate P can,
and usually will, access the whole environment Γ. Correspondingly, at the object
level, we introduce the lock constructor (L) and the unlock destructor (U). The
intended meaning of the LP(U :V ) J·K constructor is that of a logical filter expressing
inhabitability up-to the verification of Γ ` P(U :V ).
   Notice that the syntactic category of lock conditions in Figure 1 is merely an
abbreviation, in order to obtain a smoother and lighter notation in the rest of the
paper (in particular, in the type rules of Figure 8). Hence, in the following we
will switch from C to P(U : V ) or to the specific subcases P (M : σ), P(σ : K),
according to our needs.
   The rules for the main one-step βL-reduction, which combines the standard β-
reduction with the novel L-reduction (behaving as a lock-releasing mechanism, eras-
ing the U-L pair in a term of the form UJLC JM KK) appear in Figure 2. The rules for
one-step closure under context for kinds, families, objects, and lock conditions are
collected in Figures 3, 4, 5, 6 respectively. We denote the reflexive and transitive
closure of →βL by →  →βL . Hence, βL-definitional equality is defined in the standard
way, as the reflexive, symmetric, and transitive closure of βL-reduction on kinds,
families, objects, lock conditions, as illustrated in Figure 7.
   Following the standard specification paradigm of Constructive Type Theory, we
define lock-types using formation, introduction, elimination, and equality rules.
Namely, see Figure 8, we introduce a lock-constructor for building objects LC JM K
of type LC JρK, via the introduction rule (O·Lock). Correspondingly, we introduce

                                                Journal of Formalized Reasoning Vol.12, No.1
14       ·       Fabio Alessi et al.

             Σ ∈ Signatures                    Σ ::= ∅ | Σ, a:K | Σ, c:σ
             Γ ∈ Contexts                      Γ ::= ∅ | Γ, x:σ
             K ∈ Kinds                         K ::= Type | Πx:σ.K
      σ, τ, ρ ∈ Families (Types)               σ ::= a | Πx:σ.τ | σ N | LC JρK
       M, N ∈ Objects                        M ::= c | x | λx:σ.M | M N | LC JM K | U JM K
             C ∈ Lock Conditions               C ::= P(N : σ) | P(σ : K)
                                                     where the P denotes an external predicate symbol
                                                     from a fixed set of identifiers.

                                          Fig. 1.    The pseudo-syntax of LF+

             (λx:σ.M ) N →βL M [N/x] (β·O·M ain)                     U JLC JM KK →βL M (L·O·M ain)

                                     Fig. 2.    Main one-step-βL-reduction rules



             σ →βL σ 0                                            K →βL K 0
                                        (K·Π1 ·βL)                                       (K·Π2 ·βL)
     Πx:σ.K →βL Πx:σ 0 .K                                     Πx:σ.K →βL Πx:σ.K 0


                                   Fig. 3.      βL-closure-under-context for kinds


                 σ →βL σ 0                                                       τ →βL τ 0
                                                (F ·Π1 ·βL)                                           (F ·Π2 ·βL)
         Πx:σ.τ →βL         Πx:σ 0 .τ                                      Πx:σ.τ →βL Πx:σ.τ 0


                 σ →βL σ 0                                                     N →βL N 0
                                                (F ·A1 ·βL)                                           (F ·A2 ·βL)
               σ N →βL σ 0 N                                                 σ N →βL σ N 0


                 C →βL C 0                                                       ρ →βL ρ0
                              0
                                                (F ·L1 ·βL)                                           (F ·L2 ·βL)
             LC JρK   →βL   LC JρK                                         LC JρK   →βL LC Jρ0 K


                                  Fig. 4.      βL-closure-under-context for families

an unlock-destructor UJM K via the elimination rule (O·Guarded·U nlock), which is
reminiscent in its shape of a Gentzen-style left-introduction rule.
   In order to provide the intended meaning of LC J·K, we need to introduce in LF+
also the rule (O·T op·U nlock), which allows for the elimination of the lock-type
constructor if the condition C is verified, possibly externally. Figure 8 shows the
full type system of LF+ . All type equality rules of LF+ use as notion of conversion
βL-definitional equality.
   The reader familiar with previous notations for lock-types may notice that we
introduced a simplification in the notation of the unlock operator (U), dropping
the predicate, since the latter is automatically implied by the type of the term
argument M .
   One may wonder why the rule (O·T op·U nlock) is not enough and (F ·Guarded·)
and (O·Guarded·) unlock-rules are called for. In Section 3, we will show that
these two rules are crucial for providing the monadic interpretation of locks, while
(O·T op·U nlock) is merely a non-standard rule for exiting our monads. But the
Journal of Formalized Reasoning Vol.12, No.1
                                                   LF+ in Coq for fast-and-loose reasoning         ·     15


             σ →βL σ 0                                                         M →βL M 0
                                          (O·λ1 ·βL)                                              (O·λ2 ·βL)
     λx:σ.M →βL        λx:σ 0 .M                                       λx:σ.M →βL λx:σ.M 0


           M →βL M 0                                                           N →βL N 0
                                          (O·A1 ·βL)                                              (O·A2 ·βL)
         M N →βL M 0 N                                                    M N →βL M N 0


             C →βL C 0                                                         M →βL M 0
                         0
                                          (O·L1 ·βL)                                              (O·L2 ·βL)
      LC JM K    →βL   LC JM K                                          LC JM K   →βL LC JM 0 K


           M →βL M 0
                                          (O·U ·βL)
       U JM K →βL U JM 0 K



                             Fig. 5.     βL-closure-under-context for objects


           M →βL M 0                                                           σ →βL σ 0
                                          (O·C1 ·βL)                                              (O·C2 ·βL)
    P(M : σ) →βL       P(M 0   : σ)                                   P(M : σ) →βL P(M : σ 0 )


             σ →βL σ 0                                                         K →βL K 0
                                          (O·C3 ·βL)                                              (O·C4 ·βL)
    P(σ : K) →βL P(σ 0 : K)                                           P(σ : K) →βL P(σ : K 0 )



                        Fig. 6.       βL-closure-under-context for lock conditions


    T →βL T 0
                       (βL·Eq·M ain)                     T =βL T               (βL·Eq·Ref l)
     T =βL T 0


     T =βL T 0                                   T =βL T 0      T 0 =βL T 00
                       (βL·Eq·Sym)                                             (βL·Eq·T rans)
     T 0 =βL T                                           T =βL T 00



                                       Fig. 7.    βL-definitional equality

guarded-unlock rules are crucial also pragmatically. It is precisely them that make
it possible to reason hypothetically, i.e. to concatenate reasoning steps under as-
sumptions, thus making locks flexible for modeling the fast-and-loose reasoning
paradigm. Linking deduction steps under assumptions is actually a kind of Kleisli
composition. If we were to always release a locked term before accessing the encap-
sulated judgement this would mean that we would always have to check a proof-
irrelevant side condition, before using that judgement. And this is precisely what
would slow down the main flow of a derivation. Properties occurring in locks are
usually not essential to the main thrust of the proof, because they are usually
proof-irrelevant. The hard stuff goes on within the lock. In practice, one wants to
be free to proceed with the main argument, postponing, as much as possible, the
verification of details. In reaching in a proof development a stage, where we are

                                                               Journal of Formalized Reasoning Vol.12, No.1
16       ·        Fabio Alessi et al.

     Signature rules
             (S·Empty)                                                Γ `Σ σ : Πx:τ.K Γ `Σ N : τ
     ∅ sig                                                                                       (F ·App)
                                                                           Γ `Σ σ N : K[N/x]

     `Σ K      a 6∈ Dom(Σ)                            Γ `Σ ρ : Type    Γ `Σ U : V       C ≡ P(U : V )
                                 (S·Kind)                                                               (F ·Lock)
             Σ, a:K sig                                             Γ `Σ LC JρK : Type

     `Σ σ:Type       c 6∈ Dom(Σ)                               Γ `Σ σ : K      Γ `Σ K 0      K=βL K 0
                                      (S·Type)                                                          (F ·Conv)
               Σ, c:σ sig                                                    Γ `Σ σ :   K0

     Context rules                                                                                   Object rules
     Σ sig                                                                          `Σ Γ c:σ ∈ Σ
           (C·Empty)                                                                             (O·Const)
     `Σ ∅                                                                             Γ `Σ c : σ

     Γ `Σ σ:Type       x 6∈ Dom(Γ)                                                      `Σ Γ x:σ ∈ Γ
                                        (C·Type)                                                     (O·Var)
                `Σ Γ, x:σ                                                                 Γ `Σ x : σ

     Kind rules                                                                   Γ, x:σ `Σ M : τ
                                                                                                    (O·Abs)
                                                                               Γ `Σ λx:σ.M : Πx:σ.τ
       `Σ Γ
               (K·Type)
     Γ `Σ Type                                                        Γ `Σ M : Πx:σ.τ Γ `Σ N : σ
                                                                                                 (O·App)
                                                                           Γ `Σ M N : τ [N/x]
     Γ, x:σ `Σ K
                 (K·P i)
     Γ `Σ Πx:σ.K                                           Γ `Σ M : σ        Γ `Σ τ : Type     σ=βL τ
                                                                                                        (O·Conv)
                                                                            Γ `Σ M : τ
     Family rules
                                                        Γ `Σ M : ρ     Γ `Σ U : V       C ≡ P(U : V )
     `Σ Γ a:K ∈ Σ                                                                                       (O·Lock)
                  (F ·Const)                                        Γ `Σ LC JM K : LC JρK
       Γ `Σ a : K
     Γ, x:σ `Σ τ : Type                    Γ, x : τ `Σ M : ρ Γ `Σ N : LC Jτ K
                        (F ·P i)           P(Γ `Σ U : V ) C ≡ P(U : V ) C=βL C 0
     Γ `Σ Πx:σ.τ : Type                                                                          (O·T op·U nlock)
                                                      Γ `Σ M [U JN K/x] : ρ[U JN K/x]
                                                                        0
                          Γ, x : τ `Σ LC JρK : Type      Γ `Σ N : LC Jτ K      C=βL C 0
                                                  0
                                                                                             (F ·Guarded·U nlock)
                                       Γ `Σ LC Jρ[U JN K/x]K : Type
                                                                        0
                            Γ, x : τ `Σ M : LC JρK       Γ `Σ N : LC Jτ K      C=βL C 0
                                                                0
                                                                                             (O·Guarded·U nlock)
                                    Γ `Σ M [U JN K/x] : LC Jρ[U JN K/x]K



                                        Fig. 8.       The LF+ Type System

not able, or we do not want to waste time, to verify a side-condition, we want to
postpone such a task and use immediately, albeit in a nested way, the given term,
thus proceeding with the main argument of the proof. The (F ·Guarded·U nlock)
and the (O·Guarded·U nlock) rules allows us to realise precisely this. The external
lock-type of the type within which we release the unlocked term will preserve safety,
keeping track that the verification has to be carried out at least once, sooner or
later.
   We conclude this section by recalling that, since external predicates P affect
reductions in LF+ , they must be well-behaved in order to preserve subject reduction.
This property is necessary for achieving decidability, relative to an oracle, which is
Journal of Formalized Reasoning Vol.12, No.1
                                      LF+ in Coq for fast-and-loose reasoning       ·     17

essential to any proof-checker such as LF+ . We introduce, therefore, the following
crucial definition, where α is shorthand for the conclusion of a judgment.
  Definition 2.1 Well-behaved predicates, [HLS+ 16]. A finite set of predi-
cates {Pi }i∈I is well-behaved if each P in the set satisfies the following conditions:
(1) Closure under signature and context weakening and permutation:
    (a) If Σ and Ω are valid signatures such that Σ ⊆ Ω and P(Γ `Σ α), then
        P(Γ `Ω α).
    (b) If Γ and ∆ are valid contexts such that Γ ⊆ ∆ and P(Γ `Σ α), then
        P(∆ `Σ α).
(2) Closure under substitution: If P(Γ, x:V 0 , Γ0 `Σ U : V ) and Γ `Σ U 0 : V 0 ,
    then P(Γ, Γ0 [U 0 /x] `Σ U [U 0 /x] : V [U 0 /x]).
(3) Closure under reduction:
    (a) If P(Γ `Σ U : V ) and U →βL U 0 , then P(Γ `Σ U 0 : V ).
    (b) If P(Γ `Σ U : V ) and V →βL V 0 , then P(Γ `Σ U : V 0 ).

2.2   The metatheory of LF+
For the sake of completeness, we will briefly sketch the metatheory of LF+ . There
are two ways to prove the standard properties (e.g. strong normalisation, confluence
and subject reduction): either directly or exploiting a compositional embedding
function mapping entities and judgments of LF+ into another principled logical
framework, e.g. LF. This approach has been pursued in [HLMS17] for LLFP . In
this section we simply notice that, since in Section 5 we give a shallow and adequate
encoding of LF+ in Coq, we inherit all the main metatheoretic properties from the
Calculus of (Co)Inductive Constructions (the underlying type theory of Coq). This
argument is robust enough to support also all the extensions which we make in LF+
to the original theory of LLFP .
  Theorem 2.2 (Confluence of LF+ ). βL-reduction is confluent, i.e.:
(1) If K →→βL K 0 and K → →βL K 00 , then there exists a K 000 such that K 0 → →βL K 000
           00       000
    and K →    →βL K .
(2) If σ →→βL σ 0 and σ →→βL σ 00 , then there exists a σ 000 such that σ 0 →
                                                                            →βL σ 000 and
      00        000
    σ →  →βL σ .
(3) If M →→βL M 0 and M → →βL M 00 , then there exists an M 000 such that M 0 →
                                                                              →βL M 000
            00       000
    and M →    →βL M .
   We recall here that, as it is often the case for systems without η-like conver-
sions, confluence can alternatively be proved directly on raw terms as in [HHP93,
HLS+ 16]. Namely using Newman’s Lemma ([Bar84], Chapter 3), and showing that
the reduction on raw terms is locally confluent.
  Theorem 2.3 (Strong normalisation of LF+ ). (1) If Γ `Σ K, then K is
    →βL -strongly normalising.
(2) if Γ `Σ σ : K, then σ is →βL -strongly normalising.
(3) if Γ `Σ M : σ, then M is →βL -strongly normalising.



                                                Journal of Formalized Reasoning Vol.12, No.1
18      ·    Fabio Alessi et al.

  Alternatively, strong normalisation can be proved following the same pattern
used in [HLS+ 16], relying on the strong normalisation of LF, as proven in [HHP93].
  Well-behavedness of predicates is not necessary when we prove metatheoretic
results directly on raw terms, as in the theorems above. On the other hand, it is
necessary when we prove metatheoretic results about typings, as in the following
theorems.
  If the predicates are well-behaved, we have also the following:
     Theorem 2.4 (Subject reduction of LF+ ). If predicates are well-behaved, then:
(1) If Γ `Σ K, and K →βL K 0 , then Γ `Σ K 0 .
(2) If Γ `Σ σ : K, and σ →βL σ 0 , then Γ `Σ σ 0 : K.
(3) If Γ `Σ M : σ, and M →βL M 0 , then Γ `Σ M 0 : σ.
  Since we implement predicates in Coq, all the predicates in this paper are well-
behaved. Other useful standard metatheoretic results are the following ones:
  Proposition 2.5 (Weakening and permutation). If predicates are closed un-
der signature/context weakening and permutation, then:
(1) If Σ and Ω are valid signatures, and Σ ⊆ Ω, then Γ `Σ α implies Γ `Ω α.
(2) If Γ and ∆ are valid contexts w.r.t. the signature Σ, and Γ ⊆ ∆, then Γ `Σ α
    implies ∆ `Σ α.
  Proposition 2.6 (Substitution). If predicates are closed under signature/context
weakening and permutation and under substitution, then: if Γ, x:σ, Γ0 `Σ α, and
Γ `Σ N : σ, then Γ, Γ0 [N/x] `Σ α[N/x].
2.3    Comparison with the system LLFP
A more detailed comparison of LF+ with the earlier system LLFP , of [HLMS17], is
in order.
— In the language definition of LF+ we have introduced the new syntactic class C
 of lock conditions. This is essentially a definitional modification which simplifies
 the notations and the rules.
— We have dropped the reference to P(U : V ) in unlock constructors. This is
 safe since the index can be directly recovered from the type of argument to the
 unlock.
— The judgements considered in predicates are extended to families and kinds, e.g.
 P(σ, T ype), thus permitting us to consider inhabitability of types as a predicate.
— The first premise of the rule (O·Guarded·U nlock) is relaxed in that the subject of
 that premise no longer needs to be explicitly locked. Safety is preserved because
 the type has an external lock. We recall that, if subject reduction is to hold, in
 this rule some extra complexity is needed to take care of the parameters occurring
 in the predicate.
— Rule (O·T op·U nlock) is rephrased so as to make it similar in shape to the rule
 (O·Guarded·U nlock).



Journal of Formalized Reasoning Vol.12, No.1
                                        LF+ in Coq for fast-and-loose reasoning        ·     19

3.    THE MONADIC NATURE OF LF+
In this Section we illustrate in full detail how locks can be understood as monads.
This Section can be skipped by readers only interested in the applications.
   The type rules of the L and U constructors allow for an understanding of LC J·K
as a monad. Domain-theoretically this monad behaves as the Identity Monad,
creating a copy of all objects. This look-alike or doppelgänger monad creates a
double, parallel, hypothetical, possibly counterfactual world.
   The introduction rules (F ·Lock) and (O·Lock) of lock-types and lock-terms cor-
respond immediately to the introduction rules of monadic types and monadic terms
in the Metalanguage of [Mog91].
   The elimination rules, on the other hand, require more discussion.
— The (O·T op·U nlock) rule is specific to this monad. In general, there is no
 standard way to exit the encapsulation produced by a monad.
— Eliminations need to be performed also at the level of families by (F·Guarded·Unlock),
 but we do not need explicit unlock-operators at that level.
— Both rules (F·Guarded·Unlock) and (O·Guarded·Unlock) need to take into ac-
 count also definitional equality to preserve subject reduction.
— We do not use the standard letT construct as elimination construct, in favour
 of the U-constructor. We could have introduced it, e.g.
                                               0
       Γ, x : τ `Σ LC JρK : Type   Γ `Σ N : LC Jτ K    C=βL C 0
                                         0                         (F ·Guarded·U nlock)0
                 Γ `Σ let x = N in LC JρK : Type.
 But the use of let would introduce unnecessary terms in our language and make
 the (O·T op·U nlock) rule more awkward to express.
— We can define in LF+ the function letC : (σ → LC Jτ K) → LC JσK → LC Jτ K by
         λx : σ → LC Jτ K. λy : LC JσK. x(UJyK) : (σ → LC Jτ K) → LC JσK → LC Jτ K.
     It evaluates as the traditional letT construct apart from the case when the first
     argument is a constant function. Erasing the dependency is wrong if we use
     the letT construct to model Kleisli composition in the general setting. But
     we are essentially interested in inhabitability of types, rather than encapsulating
     evaluations, and such judgements do not produce effects. In our context the case
     of the constant functions amounts simply to an instance of the strengthening
     structural rule.
  In order to define formally the monad induced by the LP(U :V ) J·K construct, for
a given a predicate P and a judgement Γ `Σ U : V , we need to endow the term
model of LF+ with the structure of a category. In fact this should be done in the
more general setting of categories with families [Dyb96], due to the fact that we use
dependent types. We will not develop all the details of this construction here, but
give only the crucial insights.
  The objects and morphisms of our category will be classes of LF+ terms up to
expansion to βη-lnf. The notion of βη-lnf is given by the following definitions
(see Definition 5.8 and Definition 5.9 in [HLS+ 16]):


                                                   Journal of Formalized Reasoning Vol.12, No.1
20      ·      Fabio Alessi et al.

    Definition 3.1. An occurrence ξ of a constant or a variable in a term of a LF+
                                                                                                          #»
judgement is fully applied and unlocked with respect to its type or kind Π #»                  x 1 : #»
                                                                                                     σ 1. L 1[
                    #»                    #»            #»
. . . Π #»
        x n : #»
              σ n . L n [α] . . .], where L 1 , . . . , L n are vectors of locks, if ξ appears in subob-
                          #»          #» # »               #»           #»        # » #»           #»
jects of the form U n [(. . . ( U 1 [ξ M 1 ]) . . .)M n ], where M 1 , . . . , M n , U 1 , . . . , U n have
the same arities of the corresponding vectors of Π’s and locks.
     Definition 3.2 (Judgements in βη-long normal form).
(1) A term T in a judgement is in βη-lnf if T is in normal form and every constant
    and variable occurrence in T is fully applied and unlocked w.r.t. its classifier
    in the judgement.
(2) A judgement is in βη-lnf if all terms appearing in it are in βη-lnf.
   For the rest of this section, by semantics of an object in the term model we will
mean implicitly its βη-lnf. In order to avoid an excessive burden in the notation, we
will define the monad (LC J·K, η, µ) by giving the corresponding concrete instances
of the natural transformations η and µ as βη-lnf-classes of terms in LF+ . By abuse
of notation, we will use the same symbols both on the syntactic level and on the
semantic level.
                                   ∆                     ∆
   In particular, we have that ηρ = λx:ρ.LC JxK and µρ = λx:LC JLP(U :V ) JρKK. UJxK.
Indeed, if C ≡ P(U : V ) and Γ, x:ρ `Σ U : V is derivable, the term for η can be
easily inferred by applying rules (O·V ar), (O·Lock), and (O·Abs), as follows:
                       Γ, x:ρ `Σ x : ρ Γ, x:ρ `Σ U : V              C ≡ P(U : V )
                                                      C         C
                                       Γ, x:ρ `Σ L JxK : L JρK
                                   Γ `Σ λx:ρ.LC JxK : Πx:ρ.LC JρK
The term for µ, if Γ `Σ U : V is derivable, is obtained by applying weakening and
the rules (O·V ar) and (O·Guarded·U nlock) and finally (O·Abs):
       Γ, x:LC JLC JρKK, z:LC JρK ` z:LC JρK                 Γ, x:LC JLC JρKK `Σ x:LC JLC JρKK
                                  Γ, x:L JL JρKK `Σ UJxK : LC JρK
                                          C   C

                                      Γ ` λx:LC JLC JρKK. UJxK.
   Locks yield strong monads, whose tensorial strength is given, in our context, by
a function:
                tσ,τ : Πx:σ.Πy:LC Jτ K.LC JρK −→ Πx:LC JσK.Πy:LC Jτ K.LC JρK
namely:
        tσ,τ , λf : (Πx:σ.Πy:LC Jτ K.LC JρK).λx : (LC JσK).λy:(LC Jτ K).f (UJxK)y.
  We are left to check that the monad equalities hold. This we will do by showing
that the unity and associativity axioms of the Kleisli triple (T, η, −∗ ), corresponding
to the monad LC J·K, hold on the corresponding classes of the term model. Recall
that (see, e.g., [Mog91] for details), given a monad (T, η, µ), we can consider the
corresponding Kleisli triple (T, η, −∗ ), i.e. the category of computations induced by
the endofunctor T : C −→ C. In our case the endofunctor is parameterised by a
predicate P and a type judgment Γ `Σ U : V . The natural transformation −∗ is


Journal of Formalized Reasoning Vol.12, No.1
                                       LF+ in Coq for fast-and-loose reasoning       ·     21

defined on f : σ −→ LC Jτ K by:
                                  f ∗ : LC JσK −→ LC Jτ K
where:
                              f ∗ , λx : LC JσK.f (UJxK).
     The unity and associativity axioms for the Kleisli category are the following:
(1) f ; ητ∗ = f for f : σ −→ LC Jτ K
(2) ησ ; f ∗ = f for f : σ −→ LC Jτ K
(3) (f ; g ∗ ); h∗ = f ; (g; h∗ )∗ for f : σ −→ LC Jτ K, g : τ −→ LC JρK, and h : ρ −→
    LC JξK
These axioms hold in the term model of LF+ . Indeed, for point 1), we have that
f ; ητ∗ = λx:σ.LC JUJf (x)KK which is the βη-lnf form of f (whose type is σ −→ LC Jτ K).
    Similarly, for point 2), we have that ησ ; f ∗ = λx:σ.f (UJLC JxKK), which, according
to (L·O·M ain), reduces to λx:σ.f (x), which in turn corresponds to λx:σ.LC JUJf (x)KK
in our term model, i.e. the βη-lnf of f .
    The verification of point 3) is simpler, since both sides of the equation are equal
to λx:σ.h(UJg(UJf (x)K)K), which corresponds in our term model to the βη-lnf form
λx:σ.LC JUJh(UJg(UJf (x)K)K)KK.
    For the sake of simplicity, in all the above cases we considered σ, τ , and ρ as
constant types, otherwise we would have to further unravel their structures to
comply with the notion of βη-lnf.
    It is worth noting that all the previous Kleisli axioms would be for free if the
term model were quotiented by the notion of congruence induced by βL-reduction,
standard η-reduction, and the following notion of (L·O·η)-reduction:
                             LC JUJM KK → M          (L·O·η)
  The reason why we do not add η-rules it that those rules would make the language
theory of LF+ more difficult, because CR does not hold on raw terms, while η-
expansion is always safe. Moreover, adequacy statements need only to mention
βη-long normal forms [HHP93, AHMP92].
  Finally, to provide the intended meaning of LP(U :V ) J·K, we need to introduce in
LF+ also the rule (O·T op·U nlock), which allows for the elimination of the lock-type
constructor if the predicate P is verified, possibly externally, on an appropriate
and derivable judgement. Thus, it amounts to the possibility of “exiting” from the
monad, if certain special conditions are fulfilled. We will come back to this issue in
Section 7.
  Concluding the monadic account of locks, we remark the moral of this section:
reasoning under assumptions, via the Guarded·Unlock rules, essentially corresponds
to Kleisli composition.

4.    A REPERTOIRE OF LOCKS
This section is a cursory review of existing and potential applications of locks and
can be skipped without losing the main flow of the paper.


                                                 Journal of Formalized Reasoning Vol.12, No.1
22      ·    Fabio Alessi et al.

   In the following we list various reasoning logical systems and proof strategies
where locks have been, or could be, used fruitfully to provide a faithful and trans-
parent encoding in a Logical Framework. Implicitly this will show also that such
reasoning attitudes can be viewed as monads. Namely the concatenation of deduc-
tion steps in these patterns essentially amounts to carrying out Kleisli composition.
   A first kind of examples where locks come in handy arises when we want to factor
out, possibly proof-irrelevant, side-conditions. The only critical issue is to ensure
that the predicates involved in locks are well-behaved. Here is a non-exhaustive
list:
— modal logics. The syntactic side condition is that a proof term is either closed
 w.r.t. variables whose type is an object-logic judgment, or the free variables of
 object-logic judgement type occur in subterms of a particular shape, [HLL+ 12,
 HLS+ 16];
— substructural logics: e.g. affine elementary linear logic, non-commutative lin-
 ear logic. The side condition is that object-logic judgment typed variables are
 constrained appropriately in proof terms, [HLL+ 12, Hon13, HLS14, HLMS15,
 HLS+ 16, HLMS18];
— Hoare’s logic. Quantifier-free formulæ, and non-interference predicates are de-
 fined using syntactic constraints on formulæ, [HLL+ 12, Hon13, HLS14, HLMS15,
 HLS+ 16, HLMS17, HLMS18];
— Fitch-Prawitz Set Theory. The side condition is that proof terms are normal-
 isable [HLMS15, HLLS16, HLMS17, HLMS18]. We elaborate more on this in
 Section 7.
  Proof attitudes and concepts which can be naturally represented in LF+ using
lock-types, and hence be construed as monads, are for example:
— systems which separate deduction and computation. For instance in Deduction
 Modulo, the implication-up-to rule:
                                    C      A⊃B   A≡C
                                             B
     can be expressed as:
             ΠA, B, C : o.T rue(A ⊃ B) → T rue(C) → LP(A≡C:o) JT rue(B)K;
— systems which support reasoning and programming up-to equivalence relations,
 or up-to computations according to Poincaré’s principle, see [BB02], where terms
 are taken to be definitionally equal even if only computationally equal;
— the logical ambient in [DHJG06], where the very paradigm of fast-and-loose
 reasoning was coined in order to reason under the assumption that objects are
 total ;
— the squash, bracket, or (-1)-truncation type constructor, (see [Uni13], page 152)
 can be expressed using locks by taking ||σ|| , LInh(σ:T ype) JσK, where Inh is the
 inhabitability predicate. Using guarded-unlock rules, the introduction rule, and
 both the recursive and inductive elimination rules for squash types (see [Uni13],


Journal of Formalized Reasoning Vol.12, No.1
                                         LF+ in Coq for fast-and-loose reasoning       ·     23

     ex.3.17) can be derived in LF+ :
                                      Γ`M :σ
                                                                   Intro
                        Γ ` LInh(σ:T ype) JM K : LInh(σ:T ype) JσK

     Γ, x : σ ` M : τ     all occurrences of x in τ appear in a LInh(σ:T ype) J·K context
                                                                                                  Rec−elim
                                Γ, x : LInh(σ:T ype) JσK ` M : τ

     Γ, x : LInh(σ:T ype) JσK ` ρ : T ype
     Γ, y : σ ` N : ρ(LI(σ:T ype) JyK)    all occurrences of y in N appear within a LInh(σ:T ype) J·K
                                                                                                             Ind
                                  Γ, x : LI(σ:T ype) JσK ` N [UJσK/y] : ρx                                         .
 In this context the condition that “τ (x) is a mere proposition” in [Uni13] implies
 that all occurrences of x in τ appear in a LInh(σ:T ype) J·K context;
— generalised propositions such as x 6= 0 ⊃ x−1 6= 0 were explained by Martin-Löf
 in [MLS84] using the following rule for A ⊃ B:
                                               A True
                                 A Prop        B Prop
                                      A ⊃ B Prop
     Using locks in LF+ we can express this by:
                         A Prop            LT rue(A:Prop) JB PropK
                                        A ⊃ B Prop                 .
— Finally typical ambiguity as tacitly assumed in [Uni13], i.e. Φ(U ∈ U), can be
 expressed using locks in LF+ by:
                                   LStratif iable(Φ:T ype) JΦK

5.    A DEFINITIONAL IMPLEMENTATION OF LF+ IN COQ
An implementation of the logical framework LLFP , from scratch, in a functional
language has been attempted successfully, as far as proof checking, by Vincent
Michielini at ENS Lyon [Mic16]. Florian Rabe has given an implementation of
LLFP in the meta-metalanguage MMT [MR19]. However, extending any of the two
to a full-fledged proof development environment for LF+ would be a major task. To
achieve this we capitalise on the existing proof-assistant Coq, [Coq18].
5.1    The Coq encoding
We do not use Coq as a logical metalanguage to give a deep encoding of LF+ in Coq,
since we are not interested in reasoning on LF+ ’s metatheory. On the contrary, we
provide in this section an encoding as shallow as possible, so as to delegate to Coq’s
metalanguage not only all of LF+ ’s metalanguage, but also to reduce inhabitation-
search in LF+ to proof-search in Coq.
   We exploit the fact that Coq is a conservative extension of the dependent construc-
tive type theory of LF [HHP93], which underpins the type system of LF+ , [HLS+ 16].
Then we simulate/implement in Coq the mechanism of lock-types. Thus we can use
Coq both as the host system and as the oracle for external propositions. This yields
                                                   Journal of Formalized Reasoning Vol.12, No.1
24         ·   Fabio Alessi et al.

a definitional encoding of LF+ in Coq. It restricts us, of course, to dealing only with
total Coq-definable predicates, but this is enough for illustrating our approach and
moreover has the advantage of enforcing automatically the well-behavedness of the
external predicates, provided their Coq-encoding is adequate.
  Therefore, LF+ signatures and contexts are not modeled via structured datatypes,
such as e.g. lists, but are represented by Coq’s contexts and made available as as-
sumptions. The kind Type is represented directly via Coq’s sorts Set and Prop.
The choices are consistent with the Coq tradition: datatypes are modeled in Set,
because these feature strong recursion principles, while Props are used when intro-
ducing specifications. Hence LF+ ’s families are rendered as Coq sets or propositions
and objects as their inhabitants. Remarkably, we need to implement only the lock
constructor for families, which we do twice, once for predicates on terms, and once
for predicates on families:
Definition lockF := fun sigma: Set => fun N: sigma => fun P: sigma->Prop =>
                    fun rho: Prop => forall x: P N, rho.

     and
Definition lockK := fun kappa: Type => fun sigma: kappa => fun P: kappa->Prop =>
                    fun rho: Prop => forall x: P sigma, rho.

  In the first case families, represented by rho, are typed by Prop and objects by
families, except for the family sigma in the definition of P, which is typed by Set.
In the second case families, represented by rho, are again typed by Prop and objects
by families, while kinds in the definition of P are typed by Coq’s Type.
  External predicates of LF+ are therefore encoded as Prop-valued functions in
Coq. In doing this we can take full advantage of Coq’s logical strength, e.g. Leibniz
equality, natural numbers, inductive datatypes, and recursive functions. This is
what makes it possible to use Coq also as an oracle.
  In a nutshell, the gist of the lockF definition is to represent the locking of families
by a predicate on terms in LF+ by the Π-type:
                       pLP(N :σ) JρKq          ;       Πx : pPq(pN q).pρq.
while the gist of the lockK definition is to represent the locking of families by a
predicate on families in LF+ by the Π-type:
                        pLP(σ:κ) JρKq          ;       Πx : pPq(pσq).pρq.
For example:
                        pLClosed(N :σ) JρKq        ;   Πx:Closed(pN q) .pρq,

                         pLInh(σ:T ype) JσKq       ;     Πx:Inh(pσq) .pσq,
where Closed and Inh are Prop-valued functions in Coq which check closedness and
inhabitation conditions.
  Finally locked objects will be represented in Coq either using LockF or LockK,
according as to whether the predicate is on terms or on families, as follows (we only
give the case for a predicate on terms):
                      pLP(N :σ) JM Kq          ;       λx : pPq(pN q)pM q.

Journal of Formalized Reasoning Vol.12, No.1
                                     LF+ in Coq for fast-and-loose reasoning       ·     25

For example, the necessitation box-introduction rule in Hilbert-style S4 (see [HLS+ 16])
is given by:
             N EC : ΠA : o.Πx : T rue A.LClosed(x:T rue   A)
                                                               JT rue(A)K
whence, an occurrence of N EC A x can be rendered by:
          Γ ` λy : Closed(x).pN EC A xq : Πy : Closed(x).pT rue(A)q
where Closed is a Prop-valued function in Coq which checks the closedness condi-
tion, i.e. there are no variables of type T rue( · ).
   Our encoding might appear weak, but actually it permits us to develop formal
proofs up-to P. As a consequence, somewhat surprisingly, our Definition is suf-
ficient to derive as Coq Lemmas all the LF+ ’s typing rules that involve lock-types.
We only give the cases involving families, the other cases for kinds are dealt with
similarly. In the following, to avoid wasting space (in Coq code), we abbreviate the
names of variables denoting types as follows: s stands for sigma (σ), r stands for
rho (ρ), and t stands for tau (τ ).
— Lock-introduction (see rule (O·Lock) in Fig. 8) is rendered by Π-introduction:
  Lemma lock: forall s: Set, forall N: s, forall P: s -> Prop,
              forall r: Prop, forall M:r, lockF s N P r.
  intros; unfold lockF; intro; assumption.
  Qed.
— Unlocking at top level (see rule (O·T op·U nlock) in Fig. 8) is rendered by means
 of Π-elimination:
  Lemma top_unlock: forall s: Set, forall N: s, forall P: s -> Prop,
                    forall r: Prop, forall M:lockF s N P r, forall x: P N, r.
  intros; exact (M x).
  Qed.
— Finally, guarded-unlocking (see rule (O·Guarded·U nlock) in Fig. 8) is rendered
 by an interplay of dependencies, namely that of the unlocked inner term (N x)
 on the externally bound variable of the outer lock x, and that of the outer locked
 typed (r (N x)) on the unlocked inner term (N x):
  Lemma guarded_unlock: forall    s: Set, forall S: s, forall P: s -> Prop,
                     forall t:    Prop, forall r: t -> Prop,
                     forall M:    forall y:t, lockF s S P (r y),
                     forall N:    lockF s S P t,
                     forall x:    P S, r (N x).
  intros; unfold lockF; unfold    lockF in M; intros; apply M; auto.
  Qed.

  The encoding of this last rule is slightly problematic, because it is necessary to
  deal with the unlock constructor. Namely, we need a witness x : pPq(pSq, psq)
  such that:
                             pUJN Kq       ;       pN q x.
  This is a technical and subtle point, because the witness x is bound in the en-
  coding of the locked type. We have therefore rephrased the guarded-unlock rule

                                               Journal of Formalized Reasoning Vol.12, No.1
26      ·     Fabio Alessi et al.

     so that the definition in Coq of the lockF constructor, in the conclusion of the
     rule, appears already unfolded (i.e. δ-reduced). Thus the proof witness which
     needs to be supplied to N is directly available.
     However, this trick is transparent to the user, because we have provided him/her
     with the following user-defined tactic2 , which allows one to apply the (O·Guarded
     ·U nlock) rule to a lockF _ _ _ _ goal by supplying as witness only the propo-
     sition t (represented below by the formal parameter z):
     Ltac Guarded_unlock z :=
       match goal with
       [ |- lockF _ _ _ ?A ] =>
       unfold lockF at 1;
       apply guarded_unlock with (r := (fun w: z => A));
       [> intro; apply lock | idtac ]
       end.

     In the following sections on applications we will illustrate further the use of this
     rule.
   In conclusion, we have given a shallow encoding of LF+ in Coq via a subtle,
but ultimately natural, Definition, see [ACDG+ 19b], which expands the proof-
technique of [HLMS17]. As pointed out earlier this does not support the full
strength of LF+ , in that predicates are restricted to Coq-definable terms of some
type which eventually maps into Prop.

5.2     Adequacy of the encoding of locks in Coq
As to the adequacy of our encoding of locks in Coq, we can state the following
result:
                                                     +
  Theorem 5.1. For every Γ, M , and A, if Γ `LF M : A, then pΓq `Coq pM q : pAq.
                                                                            +
On the other hand, if pΓq `Coq N : pAq, then there exists M such that Γ `LF M : A,
provided that N does not contain variables of type P (·) (corresponding to predicates
P in LF+ ) in operator positions.
   The variable occurrence constraint in the theorem above is crucial. Otherwise,
for every σ, the translated type pLInh(σ:T ype) JσKq ≡ Πx : pσq.pσq would be always
inhabited in Coq, since it would amount to A −→ A.
   However, we cannot avoid that, from Πx : pAq.Πy : pPq(pU q).pBq, i.e. the Coq
encoding of A −→ LP(U :V ) JBK, we can derive Πy : pPq (pU q).Πx : pAq.pBq, i.e. the
Coq encoding of LP(U :V ) JA −→ BK. While in LF+ we cannot get from a derivation
of type A −→ LP(U :V ) JBK a derivation of type LP(U :V ) JA −→ BK.
   In order to be able to achieve this, we would have to extend LF+ with the axiom
that (A −→ LP(U :V ) JBK) −→ LP(U :V ) JA −→ BK is inhabited. Notice that this
kind of scoping enlargement of locks can happen only when the abstracted variables
pushed within the lock do not appear in pPq(pU q).

2L
  tac is the tactic language available in Coq, allowing one to define proof search procedures
[Coq18].




Journal of Formalized Reasoning Vol.12, No.1
                                                 LF+ in Coq for fast-and-loose reasoning              ·     27

5.3    Implementation of CLLFP? in Coq
In this subsection, to illustrate the generality of our approach to implementing
locks in Coq, we discuss a system introduced in [HLMS15, HLMS18]. The reader
can skip this subsection, if not interested in that system, without losing the flow of
the paper.
   In [HLMS15, HLMS18] we introduced, using the canonical format, the system
CLLFP? . It generalises the lock mechanism of LLFP allowing for the external tool to
synthesise a witness. The LP(?x:σ) J·K becomes a binder which binds the variable x of
type σ in the locked term/type. In this section we outline a possible implementation
in Coq of CLLFP? along the lines of what we did for LF+ .
   For the sake of brevity, we will discuss only the main rules involving locks in
CLLFP? . But, since the system introduced in CLLFP? was given in canonical form,
for the sake of clarity, we will rephrase them in standard form. The lock-introduction
rule at the level of terms is straightforward:
                                      Γ, x : σ ` M : τ
                                    P(?x:σ)
                                                                      O·? · Lock
                             Γ`L              JM K : LP(?x:σ) Jτ K
The lock-operator, graphically highlighted by the question mark (?) before the
bound variable x, is a binder. Its bound variable will be replaced by the witness
produced in establishing the predicate, according to the following lock-elimination
rule:

       Γ ` LP(?x:σ) JM K : LP(?x:σ) Jτ K                    P(Γ ` N : σ)
                                                                                O·? · T op · U nlock
                      Γ ` M [N/x] : τ [N/x]
  Please notice the difference with the (O·T op·U nlock)-rule. In CLLFP? the unlock
provides in fact a witness which needs to be replaced in the term.
  Otherwise, if we are not interested in verifying immediately the predicate and
computing the witness, we can postpone the task by the following guarded-unlock
rule:
 Γ, y:τ ` M : LP(?x:σ) Jτ K             Γ ` N : LP(?x:σ) J0 Kτ            σ =βL σ 0
                         0                                                                O·? · Guarded · U nlock
Γ ` LP(?x:σ) J0 KU P(x:σ ) JM [U P(x:σ) J0 KN /y]K : LP(?x:σ) J0 Kτ [U P(x:σ) J0 KN /y]
 It is worth noticing that, differently from the rule (O·Guarded·U nlock) of LF+ ,
appearing in Figure 8, in this case the subject of the type judgment in the conclusion
must be lock-expanded, in order to bind the variable x in U P(x:σ) JN K. Indeed this
allows for postponing the verification of predicate P and hence also the computation
of the witness.
   The previous encoding can be accommodated in Coq as follows:
                  pLP(?x:σ) JρKq           ;          Πx : pσqΠy : pPq(x, pσq).pρq
The binding nature of LP(?x:σ) J·K is rendered in the encoding by the outer Π, which
acts on the variable x of type pσq.
   Clearly also the generalised notion of lock, LP(?x:σ) J·K, discussed in this subsec-
tion, can have a monadic-ful interpretation, which we shall not discuss here.



                                                             Journal of Formalized Reasoning Vol.12, No.1
28      ·     Fabio Alessi et al.

6.    CALL-BY-VALUE λ-CALCULUS
In this section we use the implementation of LF+ introduced in Section 5 on a
standard benchmark-encoding for Logical Frameworks, namely untyped λ-calculus
with a call-by-value equational theory, i.e. the λv -calculus, see [Plo75]. In the
literature there are many ways of encoding this system starting from [AHMP92].
We use the signature given in [HLMS17], because it illustrates the flexibility of
LF+ in capitalising on Higher Order Abstract Syntax (HOAS) when considering
bound variables, while retaining the ordinary way of referring to free variables. We
carry out a simple, but meaningful derivation, which provides a paradigm of how
to reason with locked assumptions. The full code appears in the online appendix,
see [ACDG+ 19b].
   The well-known abstract syntax of λ-calculus is given by: M ::= x | M M | λx.M .
We model free variables in this object language as constants in LF+ . Bound vari-
ables are modeled by variables of the metalanguage, thus exploiting HOAS in del-
egating α-conversion and capture-avoiding substitution to the metalanguage. For
instance, the λ-term x (in which the variable is free) is encoded by the term `Σ (free
n):term for a suitable (encoding of a) natural number n (see Definition 6.1 below).
On the other hand, the λ-term λx.x (in which the variable is obviously bound) is
encoded by `Σ (lam λx:term.x).
   We introduce therefore the following signature:
     Definition 6.1 (LF+ signature Σλ for untyped λ-calculus).
     nat: Type                 term: Type
     0: nat                    S: nat → nat
     free: nat → term          app: term → term → term   lam: (term → term) → term
We use natural numbers as standard abbreviations for repeated applications of S
to 0. Standard call-by-value conversion is given by the following rules:
     Definition 6.2 (Call-by-value equational theory).
                                                    Γ `CBV N = M
                      (refl)                                     (symm)
Γ `CBV M = M                                        Γ `CBV M = N

Γ `CBV M = N Γ `CBV N = P                           Γ `CBV M = N Γ `CBV M 0 = N 0
                          (trans)                                                 (app)
       Γ `CBV M = P                                       Γ `CBV M M 0 = N N 0

v is a free variable or an abstraction (β )         Γ `CBV M = N, x 6∈ F V (Γ)
                                         v                                     (ξv )
     Γ `CBV (λx.M )v = M [v/x]                         Γ `CBV λx.M = λx.N
where the contexts Γ represent lists of equality assumptions.
     Accordingly, we extend the signature of Definition 6.1 as follows:
     Definition 6.3 (LF+ signature Σv for λv -calculus).
eq:         term → term → Type
refl:       ΠM:term. eq M M
symm:       ΠM,N:term. eq M N → eq N M
trans:      ΠM,N,P:term. eq M N → eq N P → eq M P
eq_app:     ΠM,N,P,Q:term. eq M N → eq P Q → eq (app M P) (app N Q)
betav:      ΠM:term → term. ΠN:term. LVal(N:term) Jeq (app (lam M) N) (M N)K
csiv:       ΠM,N:term → term. (Πx:term. LVal(x:term) Jeq (M x) (N x)K) → eq (lam M) (lam N)
Journal of Formalized Reasoning Vol.12, No.1
                                               LF+ in Coq for fast-and-loose reasoning               ·     29



where the predicate Val(M : term) holds if and only if M is either an abstraction or
a variable (i.e. a term of the shape (free n)) up-to reduction. Notice that the
encoding of the (ξv )-rule explicitly enforces the fact that the bound variable ranges
over values.
Notice how, in Definition 6.3, LF+ ’s lock-types permit us to model the (βv ) and (ξv )
rules: the former holds “up-to” the verification of Val(N : term), while the latter
depends, in turn, on a locked premise.
6.1   Adequacy
The adequacy of the signature for the λv -calculus can be stated as follows, see
[HLS+ 16] for more details. Given an enumeration {xi }i∈N\{0} of the variables in
the untyped λv -calculus, we put:
                                     
                                       x i, if xi ∈ X
                          X (xi ) =
                                       (free i), if xi 6∈ X
                             X (M N ) = (app X (M ) X (N ))
                            X (λx.M ) = (lam λx:term.X ∪{x} (M )),
where X is the set of bindable variables (i.e. not free variables), and hence in the
latter clause, x 6∈ X . The expression x_i denotes a Coq variable.
  Theorem 6.4 (Adequacy of syntax). Let {xi }i∈N\{0} be an enumeration of
the variables in the λv -calculus. Then, the encoding function X is a bijection be-
tween the λv -calculus terms with bindable variables in X and the terms M derivable
in judgements Γ `Σλ M : term in βη-lnf, where Γ = {x : term | x ∈ X }. More-
over, the encoding is compositional, i.e. for a term M , with bindable variables
in X = {x1 , . . . , xk }, and N1 , . . . , Nk , with bindable variables in Y, the following
holds:
      X (M [N1 , . . . , Nk /x1 , . . . , xk ]) = X (M )[Y (N1 ), . . . , Y (Nk )/x1 , . . . , xk ].
   Theorem 6.5 (Adequacy of equational theory). Given an enumeration
{xi }i∈N\{0} of the variables in the λv -calculus, there is a bijection between deriva-
tions of the judgment `CBV M = N on terms with no bindable variables in the
CBV λv -calculus and proof terms h, such that `ΣCBV h : (eq ∅ (M ) ∅ (N )) is in
βη-lnf.
6.2   Formalisation in Coq
We now proceed to represent the above signature in the Coq editor for LF+ presented
in Section 5.
   First, we declare the syntactic category of terms (typed by Set) and its construc-
tors, by exploiting the built-in representation of natural numbers, which is available
in Set:
Parameter    term:    Set.
Parameter    free:    nat -> term.
Parameter    app :    term -> term -> term.
Parameter    lam :    (term -> term) -> term.

                                                            Journal of Formalized Reasoning Vol.12, No.1
30     ·     Fabio Alessi et al.

Then, we model the Val predicate in Coq, since Coq can play in this case also the
oracle role:
Definition Val := fun N:term => (exists n, N = (free n)) \/
                                (exists M, N = (lam M)).

One can easily, albeit not formally, check that the above Coq-encoding of “being a
value” is an adequate formalisation of the intended concept, thereby giving evidence
also that the predicate originally used in the lock is well-behaved in the sense of
Definition 2.1. All Coq definable predicates are obviously well-behaved.
   Finally, we encode the call-by-value equational theory, by means of a predicate
eq typed by Prop:
Parameter eq: term -> term -> Prop.
Parameter refl:   forall M:term, eq M M.
Parameter symm:   forall M N:term, eq M N -> eq N M.
Parameter trans: forall M N P:term, eq M N -> eq N P -> eq M P.
Parameter eq_app: forall M N P Q:term, eq M N -> eq P Q ->
                  eq (app M P) (app N Q).
Parameter betav: forall M:term->term, forall N:term,
                  lockF term N Val (eq (app (lam M) N) (M N)).
Parameter csiv:   forall M N:term->term,
                  (forall x:term, lockF term x Val (eq (M x) (N x))) ->
                  eq (lam M) (lam N).

Notice that, in defining term and eq, we do not use Coq’s inductive types. This
would go beyond the expressivity of LF+ and would not support full Higher Order
Abstract Syntax (HOAS). Inductive types would be compatible, in dealing with
variables, with weak HOAS, [DFH95] but exotic terms would arise, see [DH94].
   The use of lock-types in expressing the (ξv )-rule, although natural, might appear
to be unmanageable in applications, since the variable in the premise is not imme-
diately free or bound, but only bindable. But, as it will become apparent in the
following example, the (O·Guarded·U nlock) rule in LF+ accommodates precisely
this issue. Namely, the necessary verification is pushed at the outermost level,
where it is discharged by the application of the (ξv )-rule.
   To illustrate the Coq editor of LF+ in action, we conclude the section with the
formal proof of the simple equation λx. z ((λy.y) x) = λx. z x. As pointed out
earlier, this is a paradigm example of how to reason with locks. The crucial step is
the application of the (O·Guarded·U nlock) rule; the first premise is given by the
application of the (O·Lock) rule to the conclusion of the eq_app rule, while the
second premise is the conclusion of the betav rule3 :
                                                                          (betav)
             ∇         x:t `Σv LV al(x:t) Jeq(app(lam(λy:t. y), x), x)K
                                                                              (O·G·U)
        z, x:t `Σv LV al(x:t) Jeq(app(z, app(lam(λy:t. y), x)), app(z, x))K
       z:t `Σv ∀x:t. LV al(x:t) Jeq(app(z, app(lam(λy:t. y), x)), app(z, x))K
                                                                              (csiv)
          z:t `Σv eq(λx:t. app(z, app(lam(λy:t. y), x)), λx:t. app(z, x))

3 Inthe following proof tree we use the abbreviation t for term and (O·G·U ) for
(O·Guarded·U nlock). We apply it via the Guarded_unlock tactic introduced in Section 5.

Journal of Formalized Reasoning Vol.12, No.1
                                       LF+ in Coq for fast-and-loose reasoning       ·     31

“∇” represents the following derivation, where u , eq(app(lam(λy:t. y), x), x) is
the witness that we supply to the Guarded_unlock tactic (see Section 5):
                         (refl)                                          (Hyp)
          z:t ` eq(z, z)          x:t, w:u ` eq(app(lam(λy:t. y), x), x)
                                                                         (eq app)
            z, x:t, w:u ` eq(app(z, app(lam(λy:t. y), x)), app(z, x))
                                                                             (O·Lock)
      z, x:t, w:u ` LV al(x:t) Jeq(app(z, app(lam(λy:t. y), x)), app(z, x))K
 We remark the role of the (O·Guarded·U nlock) rule, which allows us to apply the
rules of the Σv signature (in this case, the eq_app rule) under Val, i.e. it permits
to handle even premises which are locked.
  We finally observe that using the Coq editor of LF+ we may accomplish the above
goal without having to exhibit the full proof term beforehand, as we had to do using
the ad-hoc type checker written by Michielini [Mic16] or the embedding of LLFP
in MMT [MR19], because we can now build it interactively and incrementally, via
Coq’s tactics.

7.    FAST-AND-LOOSE REASONING PARADIGMS
The present section is an introduction to the reasoning paradigms underpinning
the massive case studies presented in the two following sections, concerning the
management of branch prediction and of optimistic concurrency control.
   In Section 4 we outlined already many logical situations which could benefit if
analysed using locks. Here, we focus on a family of emerging paradigms which
we have termed fast-and-loose reasoning paradigms borrowing the phrase from
[DHJG06].
   It is often the case, when carrying out informal, or rather pre-formal, reasoning
in program development [DHJG06] or in ordinary mathematics [HLLS16], that we
trade off efficiency against correctness and postpone tedious or computationally
demanding checks, until we are really sure that the intended goal can be achieved.
Only then it is worth “dotting the i’s and crossing the t’s”. At machine level similar
policies are implemented to achieve efficiency in concurrency control or branch pre-
diction. In these cases the checks are not postponed, but rather run in parallel, and
strict protocols are implemented to recover from possibly counterfactual situations.
   In this section we briefly speculate on the novel idea of using Computer Assisted
Formal Reasoning (CAFR) tools for fast-and-loose informal reasoning. The gist of
the idea is to encapsulate, using locks, the arguments which are informal for the
time being. It is thus apparent how monads come into play.
   We list below a number of situations which, in our view, come under the fast-
and-loose reasoning paradigm. In the following two sections the same ideas will be
used to model the instances of this paradigm in Computer Architecture.
7.1   A historical example: the Regula Falsi for solving linear equations
The paramount example of fast-and-loose reasoning attitudes are trial and error
procedures. The Regula Falsi is perhaps the oldest one. It is a technique for solving
linear equations, widespread over continents and along centuries, see [CWB+ 12]. It
first appeared in the ancient Egyptian Rhind Papyrus dating from 1650 BC; then as
the ying bu zu shu (rule of too much and not enough) in Chapter 7 of the Jiuzhang
Suanshu (Computational Prescriptions in Nine Chapters) dating from 200 BC; the
                                                 Journal of Formalized Reasoning Vol.12, No.1
32     ·     Fabio Alessi et al.

Arab mathematician Abū Kāmil used it extensively in the 9th century in the Kitāb
al Khāta’ayn (the book of the two errors); the Indian mathematician Bhāshkara
        ˙
in his book  Lı̄lāvati dating from the 12th century called it false supposition, and
finally Fibonacci in the 13th century in his Liber Abaci called it Regula Falsi.
   The Regula is the following: when presented with a linear equation guess a value
for the indeterminate and compute the value of the linear terms in the equation,
using your guess. Next compute the fraction of the result corresponding to the
constant term in the equation. The root of the equation will be the same fraction
of your guess. In the general case the guess is iterated as in a dichotomic search,
hence the name “too much and not enough”. Using locks the simple case can be
expressed as an alternate top-unlock-rule, namely:

                    L{M (a)=N }(a:Q) JM (a) = N K       kM (a) = N
                                       M (ka) = N
provided M is a rational linear homogenous polynomial, and N is a constant term.
  Notice that the lock in this case plays the role of a counterfactual conditional.
7.2   Fitch-Prawitz Set Theory FP
Fitch-Prawitz Set Theory, [Fit52, Pra65, HLLS16], is a non standard set-theory
which comes closest among consistent set-theories to approximating the contra-
dictory naı̈ve unrestricted comprehension axiom, namely the axiom asserting the
existence of the set {x | φ(x)} for any property φ. The theory is a natural deduc-
tion First Order Logic w.r.t. a signature with only one term constructor λx.φ(x) and
only one binary predicate, i.e. membership ∈. These are introduced and eliminated
by the rules:
                     φ(t)                       t ∈ λx.φ(x)
                             λ − Intro                      λ − Elim
                 t ∈ λx.φ(x)                        φ(t)
   Since FP does not rely on any hierarchy of sets, Russell’s paradox is immediately
derivable if no further restrictions are enforced. Fitch introduced various conditions,
but it was Prawitz who isolated the crucial property, namely that the derivation be
normal. In [HLMS15] we have extended this condition to normalisability. In our
view this system is a paradigm example of a system supporting the fast-and-loose
reasoning paradigm. We can pretend to reason in Cantor’s paradise and freely use
the un-restricted set-theoretic comprehension principle. These arguments however
yield only pseudo-proofs. At some stage we need to check that these pseudo-proofs
are indeed normalisable. One could check this proviso only at the very end on the
whole proof. Lock types [HLMS17, HLMS18] permit to highlight incrementally the
crucial points in the proofs where such checks need to be carried out, e.g. each time
introduction rules are applied, possibly removing the locks at one’s convenience,
   Clearly the Type Ambiguity proviso in Type Theory, discussed in Section 4, or
the small categories blanket assumption, normally made by the working category
theorist, are other examples of the fast-and-loose reasoning paradigm when dealing
with large objects in the context of hierarchies.
   For the sake of completeness we mention that similar issues arise also in dealing
with highly self-descriptive concepts such as truth, see [Kri75].
Journal of Formalized Reasoning Vol.12, No.1
                                      LF+ in Coq for fast-and-loose reasoning       ·     33

7.3   Co-inductive proofs in Coq
Coq itself offers an immediate example of the fast-and-loose reasoning paradigm in
the way by which it handles co-inductive proofs and the Cofix-tactic, [Coq18]. In-
deed in proof development one can freely apply the coinductive hypothesis, namely
assume the goal, without checking that it is guarded by some constructor. The
editor checks this condition either at the end or whenever the user invokes the
Guarded command. The Coq editor keeps track implicitly of the guardedness con-
dition, whereas locks propagate such proviso explicitly.

7.4   “Fast-and-Loose Reasoning is Morally Correct”[DHJG06]
In the seminal paper [DHJG06] the authors introduced the concept of “Fast-and-
Loose Reasoning” to denote those program transformations and program equality
derivations, in possibly non-terminating functional programming languages, which
are strictly speaking sound only if the data are total and finite. The authors prove
that this kind of informal program development is morally correct in the sense that
if two programs are proved to be equal in the world of sets they are equivalent (w.r.t.
a certain notion based on PER’s) also in the world of domains. Hence correctly
terminating programs, proved equal assuming that the inputs are total, are not
transformed in looping ones.
   The reasoning attitude of [DHJG06] can be naturally expressed using locks. For
example reverse ◦ reverse = id is sound if the type of reverse is taken to be
Πx ∈ List[N at].L{x6=⊥}(x:List[N at]) JList[N at]K. Locks automate the burden of prop-
agating preconditions across the proof tree.
7.5   A visionary example
Quantum Computing is really a kind of analogical computing. Somewhat futuristi-
cally we can imagine to use Quantum Computers for deriving propositions, either
using massively parallel case analyses or even in counterfactual computing, i.e. in
computing without executing or in truth-without-proof. Locks could be used to
make apparent where such non-apodictic sources of evidence are invoked.
7.6   The issue of Adequacy
Fast-and-loose reasoning paradigms, especially in computer architecture, see Sec-
tion 8, usually come with some error-recovery protocol or backtracking strategy. In
LF+ predicates in Locks are implicitly checked in parallel. How do we express and
capture adequately such paradigms/protocols? In Section 8.3 we give a possible
solution in Coq, but more experimenting is necessary. This issue is related to the
problem of exiting from a monad, when the predicate is false, possibly backtracking
to a previous “safe” state, or even an entirely new state. In general the natural exit
from a monad (T, η, µ) can be expressed by ∃x.N = η(x) →
L∃x.N =η(x)(N :A) JletT y = N in M = M [η −1 (N )/y]K → (letT y = N in M ) = M [η −1 (N )/y]
 but we could also speculatively imagine that, in case ¬∃x.N = η(x), then some
kind of judgement
  L∃x.N =η(x)(N :A) J(letT x = N in M ) = M [η −1 (N )/y]K → (letT x = N in M ) = M 0
holds for a suitable M 0 .

                                                Journal of Formalized Reasoning Vol.12, No.1
34       ·        Fabio Alessi et al.

8.     BRANCH PREDICTION
In computer architecture, a branch predictor is a digital circuit which tries to guess
which branch will exit a conditional control, e.g. an if-then-else, before the result
of the test is actually known [JKL00]. The purpose of a branch predictor circuit
is to speed-up the flow in the instruction pipeline. Namely, the time needed for
the branch instruction, to pass the execution stage, is not wasted idly, but the
computation proceeds by guessing whether the conditional branch is more likely to
be taken or not taken. The branch which is guessed to be the most likely is then
fetched and speculatively executed; if later it is detected that the guess was wrong,
the speculatively executed or partially executed instructions are discarded and the
pipeline starts over with the correct branch, incurring a delay.
   In this section we model the behavior of conditional branching in LF+ by con-
sidering the conditional jump construct of the Unlimited Register Machine (URM),
a simple universal model of computation popularised by N. Cutland [Cut80]. Our
modeling of branch prediction is rather coarse-grained w.r.t. real scenarios in CPUs,
but this helps to focus on the main issues involved. As a first step, we give the
semantics of URM using lock-types; then, in the second part of the section, we deal
with the issue of handling misprediction. Finally we address the adequacy of the
whole approach.
   An URM has an infinite number of registers R0 , R1 , . . . containing natural num-
bers r0 , r1 , . . . which may be mutated by instructions. Sequences of instructions
form programs:
              s ::= hι7→rι iι∈[0..∞]                                  Store
              I ::= Z(i) | S(i) | T (i, j) | J(i, j, k)   i, j, k∈N   Instruction
              P ::= (ι7→Iι )ι∈[1..m]                      m∈N         Program
The four kinds of instructions Zero, Successor, Transfer, Jump have the following
intended meanings (r → R stands for loading the natural r into the register R):
     Z(i)         ,   0 → Ri
     S(i)         ,   ri + 1 → Ri
     T (i, j)     ,   ri → Rj
     J(i, j, k)   ,   if ri =rj then execute as next instruction Ik else the following one
When given a program P , a program counter n, and a store s, an URM executes the
program starting from the n-th instruction in P and carries out the instructions
sequentially (unless a “positive” J instruction is encountered), mutating at each
step the contents of the store as prescribed by the instructions. The evaluation of
a program may be described, therefore, as follows:
               
               
                 s                        if f etch(P, n)=Halt
                E(P, n+1, zero(s, i)) if f etch(P, n)=Z(i)
               
               
  E(P, n, s) =    ...                      ...
                  E(P, k, s)               if f etch(P, n)=J(i, j, k) and s(i)=s(j)
               
               
               
               
                  E(P, n+1, s)             if f etch(P, n)=J(i, j, k) and s(i)6=s(j)
               

We use the zero function for updating the store according to the Z instruction
(similar updating functions succ for S and move for T are omitted) and the f etch
function for recovering the instruction pointed to by the program counter. The
Journal of Formalized Reasoning Vol.12, No.1
                                               LF+ in Coq for fast-and-loose reasoning        ·       35

Halt instruction is added to make the function f etch total. A computation stops
if and only if f etch fetches Halt. On the other hand, due to the looping back via
the J instruction, there are non-terminating computations. In our case study we
consider only terminating computations (the interested reader may refer to [Cia11]
for a coinductive approach to diverging computations).
   The functions introduced in order to formalise evaluation are defined as follows:
                   f etch(P, n)    ,    if n>length(P ) then Halt else In
                   zero(s, i)      ,    λι∈N. if ι=i then 0 else s(ι)
                   succ(s, i)      ,    λι∈N. if ι=i then s(ι)+1 else s(ι)
                   move(s, i, j)   ,    λι∈N. if ι=j then s(i) else s(ι)
   To introduce an LF+ signature for the URM machine, we need first to encode infi-
nite stores and non-structured programs. Both datatypes are handled by mimicking
lists.
  Definition 8.1 (LF+ signature for Stores and Programs).
  nat: Type       0: nat    S: nat → nat
  store: Type     zeros: store    cs: nat → store → store
  ins: Type       Ht: ins    Zr: nat → ins    ...    Jp: nat → nat → nat → ins
  pgm: Type       void: pgm    cp: ins → pgm → pgm
Natural numbers nat are extensively used in the URM-signature: actually, we make
them play also the role of store locations, e.g. in Zr (encoding Z), and program
counters, in Jp (encoding J). Stores are modeled as “LF+ -lists”. We introduce
therefore the nil-like zeros object constant and the cons-like cs constructor, whose
intended meanings are given by the constants in Definition 8.2. We encode programs
as lists of instructions in ins, where Ht represents the Halt instruction.
   To structure the evaluation of URM programs, we introduce the two small-step
relations ; ⊆ pgm × nat × store × nat × store and ⇒ ⊆ pgm × nat × store × store,
as follows:
                f etch(P, n)=Z(i)                           f etch(P, n)=S(i)
                                           (eZ)                                      (eS)
          hn, si ; hn+1, zero(s, i)i
                    P
                                                       hn, si ;P hn+1, succ(s, i)i

        f etch(P, n)=T (i, j)                      hn, si ;P hm, ti    hm, ti ;P hq, ui
                                        (eT)                                                (trans)
   hn, si ; hn+1, move(s, i, j)i
           P
                                                             hn, si ; hq, ui
                                                                      P



    f etch(P, n)=J(i, j, k)    s(i)=s(j)               f etch(P, n)=J(i, j, k)   s(i)6=s(j)
                                           (Jt)                                               (Jf)
               hn, si ; hk, si
                        P
                                                              hn, si ; hn+1, si
                                                                          P



      f etch(P, n)=Halt                    hn, si ;P hm, ti      f etch(P, m)=Halt
                   P
                              (empty)                                                  (stop)
          hn, si ⇒ s                                       hn, si ⇒P t

 Now we come to the crucial issue. LF+ ’s lock-types allow us to model faithfully also
the execution of a “branch prediction” version of this semantics, by postponing the
store access and test required by J, which is a slow instruction. Lock-types permit
to carry out the store access and equality check concurrently and asynchronously
w.r.t. the main computation, in the spirit of the fast-and-loose philosophy. We omit

                                                         Journal of Formalized Reasoning Vol.12, No.1
36         ·       Fabio Alessi et al.

for simplicity in the following definition the encoding of the S and T instructions.
In the following definition some of the constants are self-explicatory, constants step
and eval are the encodings of ; and ⇒ respectively, the remaining constants reify
the behaviour of the auxiliary functions and judgements.
     Definition 8.2 (LF+ signature ΣB for URM evaluation).
      T        :    Type
      fetch    :    pgm → nat → ins → Type
      zero     :    store → nat → store → Type
      step     :    prg → nat → store → nat → store → Type
      eval     :    prg → nat → store → store → Type
      h, , i   :    store → nat → nat → T
      fvn      :    Πn:nat. fetch void n Ht
      fc0      :    ΠI:ins. ΠQ:prg. fetch (cp I Q) 0 I
      fcn      :    ΠI,L:ins. ΠQ:prg. Πn:nat. fetch Q n L → fetch (cp I Q) (S n) L
      zvn      :    Πn:nat. zero zeros n zeros
      zc0      :    Πv:nat. Πs:store. zero (cs v s) 0 (cs 0 s)
      zcn      :    Πv,n:nat. Πs,t:store. zero s n t → zero (cs v s) (S n) (cs v t)
      sZ       :    ΠP:pgm. Πn,i:nat. Πs,t:store.
                    fetch P n (Zr i) → zero s i t → step P n s (S n) t
      sJt      :    ΠP:pgm. Πn,i,j,k:nat. Πs:store.
                    fetch P n (Jp i j k) → LEq(hs,i,ji:T) Jstep P n s k sK
      sJf      :    ΠP:pgm. Πn,i,j,k:nat. Πs:store.
                    fetch P n (Jp i j k) → LNeq(hs,i,ji:T) Jstep P n s (S n) sK
      sTr      :    ΠP:pgm. Πn,m,q:nat. Πs,t,u:store.
                    step P n s m t → step P m t q u → step P n s q u
      e0       :    ΠP:pgm. Πn:nat. Πs:store. fetch P n Ht → eval P n s s
      e1       :    ΠP:pgm. Πn,m:nat. Πs,t:store.
                    step P n s m t → fetch P m Ht → eval P n s t
where Eq(hs, i, ji, T) holds if and only if s(i)=s(j), and Neq(hs, i, ji, T) iff s(i)6=s(j).
     The above signature is adequate in the sense of Claim 8.6.
8.1        Formalisation in Coq
In this subsection we illustrate how to encode the signature ΣB in the implemen-
tation of LF+ in Coq, given in Section 5. Accordingly, we express the external
predicates Eq and N eq in Coq thus using it as the oracle. In so doing we take
advantage also of Coq’s built-in notion of Leibniz equality, natural numbers, and
lists, to define stores, locations, program counters, instructions, and programs (all
typed by Set), namely:
Definition store: Set := list nat.
Definition loc: Set := nat. Definition pc: Set := nat.
Parameter ins: Set. Parameter Ht: ins.
Parameter Zr: loc -> ins. ... Parameter Jp: loc -> loc -> pc -> ins.
Definition pgm: Set := list ins.
We define also the type of the input to the oracle, i.e. a store and a pair of locations,
as an inductive type T of triples, to gain efficient projection functions. Memory
access is realised through the built-in total function nth, which returns the 0 value
when the end of a list-store is reached.
Journal of Formalized Reasoning Vol.12, No.1
                                                        LF+ in Coq for fast-and-loose reasoning        ·       37

   The oracle predicates can then be formalised in Coq using these datatypes, as
follows:
Inductive T: Set := triple: store -> loc -> loc -> T.
Definition pr1 (x:T): store := match x with triple s i j => s end. ...
Definition s_nth (s:store) (n:loc): nat := nth n s 0.
Definition Eq := fun x:T => s_nth (pr1 x) (pr2 x) = s_nth (pr1 x) (pr3 x).
Definition Neq := fun x:T => s_nth (pr1 x) (pr2 x) <> s_nth (pr1 x) (pr3 x).
The evaluation semantics is finally encoded as a predicate, via suitable auxiliary
functions that update the store. We omit for lack of space such functions and most
of the Coq translation of Definition 8.2, this is available at [ACDG+ 19b].
Parameter step: pgm -> pc -> store                        -> pc -> store -> Prop.
Parameter sJt: forall P n i j k s,                        fetch P n = (Jp i j k) ->
               lockF T (triple s i                        j) Eq (step P n s k s).
Parameter sJf: forall P n i j k s,                        fetch P n = (Jp i j k) ->
               lockF T (triple s i                        j) Neq (step P n s (S n) s). ...
Parameter eval: pgm -> pc -> store                        -> store -> Prop. ...

  In principle we could have used directly the signature ΣB of Definition 8.2 in
defining the external predicates, but this would have required to spell out in an ex-
tended signature all the recursion and inversion principles necessary to manipulate
the data-types. But this would have been a time-consuming task. Exploiting Coq’s
expressive power is another feature of our implementation.
8.2       Examples
In order to appreciate the encoding at work, let us consider the simple program
P , [Z(0), J(0, 1, 0)] and the stores s , [1, 1] and t , [0, 1].
  Example 8.3 (First proof of h1, si ;P h1, ti).                            4

                 P (1)=J(0, 1, 0)
                                                (sJt)
      L   Eq(hs,0,1i:T )
                           Jh1, si ;P h0, siK             Eq(hs, 0, 1i)               P (0)=Z(0)
                                                                          (O·Top)                      (sZ)
                               h1, si ;P h0, si                                     h0, si ;P h1, ti
                                                                                                       (sTr)
                                                           h1, si ;P h1, ti
In this proof tree there is a limited amount of parallelism between the equality check
of the contents of store locations and the main computation, because we wait until
the verification of Eq(hs, 0, 1i) is accomplished, before channeling the reductions
via the transitivity (sT r) rule. The parallelism may be increased by exploiting the
(O·Guarded·U nlock) rule, which handles arguments within a lock-type, and allows
us to apply the (sT r) rule even in the presence of a locked J reduction.

4 Asalready remarked in Section 5, in the present and the next derivations we display LF+ ’s types
without the proof terms because these are synthesised by the editor.




                                                                  Journal of Formalized Reasoning Vol.12, No.1
38       ·      Fabio Alessi et al.

     Example 8.4 (Second proof of h1, si ;P h1, ti).                              5

          P (1)=J(0, 1, 0)                       P (0)=Z(0)
LEq(hs,0,1i:T ) Jh1, si ;P h0, siK           h0, si ;P h1, ti
                                                                        (sTr via O·G·U)
             LEq(hs,0,1i:T ) Jh1, si ;P h1, tiK                                              Eq(hs, 0, 1i)
                                                                                                               (O·Top)
                                                    h1, si ; h1, ti
                                                               P


The Eq(hs, 0, 1i) check can now be delayed (actually, it now appears closer to
the conclusion) and carried out independently w.r.t. the main reduction. The
(O·Guarded·U nlock) rule allows for more proof trees for the same judgment. This
is precisely what accommodates the branch prediction philosophy.
   An even higher degree of parallelism could be achieved in LF+ if a mechanism
to “compose” pieces of reductions within different lock-types were available. This
would give us the opportunity to apply the transitivity rule “under” pairs of Jump
instructions. If, for instance, we want to manage a maximum of 2 branch constructs,
we can define introduction and elimination rules of the following shape:
              LP1 (hx~1 i:T ) Jhn, si ;P hm, tiK             LP2 (hx~2 i:T ) Jhm, ti ;P hq, uiK
                                                                                                       (P+ )
                             LP1 (hx~1 ,T i);P2 (hx~2 i:T ) Jhn, si ;P hq, uiK

                    LP1 (hx~1 ,T i);P2 (hx~2 i:T ) Jhn, si ;P hm, tiK            P1 (x~1 )
                                                                                             (P−1 )
                                  LP2 (hx~2 i:T ) Jhn, si ;P hm, tiK

                    LP1 (hx~1 ,T i);P2 (hx~2 i:T ) Jhn, si ;P hm, tiK            P2 (x~2 )
                                                                                             (P−2 )
                                  L   P1 (hx~1 i:T )
                                                       Jhn, si ; hm, tiK
                                                                    P


where Pι stands for Eq or N eq, and x~ι ≡ hxι , iι , jι i, for all ι∈{1, 2}. We could then
delay even more the access to pairs of memory locations to check for (in)equality
of their contents, as follows.
     Example 8.5 (Proof of h1, si ;P h2, ti).
                  ..
                   .                                     P (1)=J(0, 1, 0)
LEq(hs,0,1i:T ) Jh1, si ;P h1, tiK           L   N eq(ht,0,1i:T )
                                                                    Jh1, ti ;P h2, tiK
                                                                                         (P+ )
              LEq(hs,0,1i,T );N eq(ht,0,1i:T ) Jh1, si ;P h2, tiK                                    Eq(hs, 0, 1i)
                                                                                                                     (P−1 )
                                           LN eq(ht,0,1i:T ) Jh1, si ;P h2, tiK                                               N eq(ht, 0, 1i)
                                                                                      h1, si ; h2, ti
                                                                                                 P


It turns out that such a “composition” of predicates can be dealt with via lock
nesting: that is, we manage elimination rules in the form P− by means of the
(O·T op·U nlock) rule (i.e. Coq’s top_unlock lemma) and introduction rules such
as P+ via the (O·Guarded·U nlock) rule (i.e. Coq’s guarded_unlock lemma and
Guarded_unlock tactic, see Section 5). Moreover, the order of predicates does not
matter, as the commutativity property holds.
   We have thus shown how LF+ can naturally accommodate computations running
in parallel asynchronously, as it happens when performing branch prediction.

5 We   omit here the details of the full application of (O·G·U ).

Journal of Formalized Reasoning Vol.12, No.1
                                     LF+ in Coq for fast-and-loose reasoning        ·     39

8.3    Adequacy: prediction and misprediction
It is apparent that the LF+ ’s signature ΣB introduced so far models all possible
outcomes of a branch predictor circuit, within a “soup” of provable judgments,
many of which are in fact counterfactual. Namely, given a URM program P , a
store s and a program counter n, by working with our machinery we are able
to mimic every terminating computation that a branch predictor would perform
in transforming s into a final store t. We could formalise all this by a suitable
adequacy result.
   If we want to formalise more perspicuously a branch predictor circuit, we need to
make more precise assumptions on its behaviour. Recall, however, that our formal
model of branch prediction is coarse-grained, being in fact without pipelining, dif-
ferently from real-world branch predictor circuits. In the following claim we state
the adequacy of the signature ΣB w.r.t. a branch predictor which predicts at most
one Jump instruction and carries out at most two instructions ahead of the fully
checked, definitive execution flow.
   We introduce the notation {A} −→∗P {B} to denote the computation carried
out by such a branch predictor circuit from the state A to the state B under the
program P .
   The claim can be proved by induction on the structure of the derivation (sound-
ness) and by induction on the length of the computation (completeness).
  Claim 8.6 (Adequacy of ΣB signature). For every program P ∈ pgm, pro-
gram counters m, n ∈ nat, stores s, t ∈ store, and P ∈ {Eq, N eq}:
            Soundness: If Γ `ΣB step P n s m t then {n, s} −→∗P {m, t}

      Completeness: 1) If {n, s} −→∗P {m, t} without active mispredictions then
                       Γ `ΣB step P n s m t
                    2) If {n, s} −→∗P {m, t} with one active misprediction then
                       ∃u, i, j. Γ `ΣB LP(hu,i,ji:T ) Jstep P n s m tK,
   The way branch predictor computations are represented in our setting is not fully
satisfactory. In fact, we do not model either prediction or misprediction, but allow
for taking always the “correct” branch. In the practice of computer architecture,
the selection of which strategy to take, may be either dynamic (via information
collected at runtime) or static, i.e. decided in advance. When a misprediction
occurs, the execution of the incorrect branch is discarded and the computation is
resumed from the correct branch.
   In this section, we discuss two different URM semantics, which implement two
kinds of static prediction that we name NEVER protocol and BACKWARDS pro-
tocol. When a Jump instruction is encountered, in the former case we guess the
result of the test to be false and arrange the computation to proceed from the
following instruction; in the latter scenario, the target of the Jump is checked at
runtime and it is taken only if it is less than the current program counter.
   Suppose that Pn =f etch(P, n)=J(i, j, k), then the intended prediction of the
Jump instruction for the NEVER and the BACKWARDS protocol are, respec-



                                                Journal of Formalized Reasoning Vol.12, No.1
40     ·     Fabio Alessi et al.

tively:
J(i, j, k) ,N execute as the next instruction the one immediately following, i.e. Pn+1
J(i, j, k) ,W if k<n then execute as next instruction Pk else Pn+1
   The LF+ signature for the NEVER protocol is almost the same as that of Def-
inition 8.2, but for the sJt rule, which disappears, and for sJf, which is updated
to:
      sJnever : ΠP:pgm. Πn,i,j,k:nat. Πs:store.
                fetch P n (Jp i j k) → LNeq(hs,i,j,P,n,ki:U) Jstep P n s (S n) sK
On the other hand, in the LF+ signature for the BACKWARDS protocol one re-
places both rules sJt and sJf of Definition 8.2, respectively by:
sJback  : ΠP:pgm. Πn,i,j,k:nat. Πs:store.
          fetch P n (Jp i j k) → k < n → LEq(hs,i,j,P,n,ki:U) Jstep P n s k sK
sJahead : ΠP:pgm. Πn,i,j,k:nat. Πs:store.
          fetch P n (Jp i j k) → k >= n → LNeq(hs,i,j,P,n,ki:U) Jstep P n s (S n) sK
In both protocols the predicate given as input to the oracle contains now three
extra parameters (thus its type becomes U ), namely the program P , the address
n of the Jump instruction involved, and its potential target k, i.e. the information
to be used to backtrack the computation in the case of misprediction. Therefore, a
novel mechanism to handle such an event is required. In the NEVER scenario we
have to add just one rule, which completes the ΣN signature, namely:

           backtrack_neq : ΠP:pgm. Πn,i,j,q,k,m:nat. Πs,t,u:store.
                           LNeq(hu,i,j,P,q,ki:U) Jstep P n s m tK → u(i)=u(j) →
                           step P n s k u
The BACKWARDS case demands for a second rule, which gives the ΣW signature:

            backtrack_eq : ΠP:pgm. Πn,i,j,q,k,m:nat. Πs,t,u:store.
                           LEq(hu,i,j,P,q,ki:U) Jstep P n s m tK → u(i)6=u(j) →
                           step P n s (S q) u

  These new rules provide the mechanism which allows us to discard a mispre-
diction, performed with the store being u, and resume the computation from the
correct branch, that is, from u itself and the k-th instruction, provided we are able
to prove that u(i)=u(j), in the first case, and from the q+1-th instruction, pro-
vided that u(i)6=u(j) holds, in the second one. Notice that the tests, u(i)=u(j)
and u(i)6=u(j), in the backtracking rules are computationally demanding and of
the same nature as the predicate in the lock. In our encoding philosophy we must
conceive them as being carried out at the level of the Oracle. We will discuss further
this issue at the end of the section.




Journal of Formalized Reasoning Vol.12, No.1
                                         LF+ in Coq for fast-and-loose reasoning           ·     41

  Claim 8.7 (Adequacy of ΣN for the “never” protocol). For every pro-
gram P ∈ pgm, program counters m, n ∈ nat, stores s, t ∈ store:
   Soundness:    If Γ `ΣN step P n s m t then {n, s} −→∗P N {m, t}
   Completeness: 1) If {n, s} −→∗P N {m, t} without active mispredictions then
                    Γ `ΣN step P n s m t
                 2) If {n, s} −→∗P N {m, t} with one active misprediction then
                    ∃u, i, j, q, k. Γ `ΣN LN eq(hu,i,j,P,q,ki:U ) Jstep P n s m tK
A similar Claim may be made for ΣW w.r.t. the BACKWARDS protocol.
   Wrapping up, the modifications of the Coq code, to formalise the NEVER proto-
col, concern the type of (the input to) the oracle, the N eq predicate, the semantics
of the Jump instruction, and the extra rule to backtrack from a misprediction:
Inductive U: Set := sestet: store -> loc -> loc -> pgm -> pc -> pc -> U.
Definition Neq := fun x:U => store_nth (pr1 x) (pr2 x) <>
                             store_nth (pr1 x) (pr3 x) /\
                             fetch (pr4 x) (pr5 x) =
                             Jp (pr2 x) (pr3 x) (pr6 x).
Parameter sJnever: forall P n i j k s, fetch P n = (Jp i j k) ->
                   lockF U (sestet s i j P n k) Neq (step P n s (S n) s).
Parameter backtrack_neq: forall u i j q k P n s m t,
                   lockF U (sestet u i j P q k) Neq (step P n s m t) ->
                   s_nth u i = s_nth u j -> step P n s k u.

   The proof trees performed with the ΣB signature in the previous section are
clearly affected by these additions. In the case of the NEVER protocol, in Example
8.3 the subgoal h1, si ;P h0, si cannot be proved via (O·Top), because the Eq
predicate is not defined in this protocol: hence, one has to apply backtrack_-
neq and discard the LN eq(hs,0,1,P,1,0i:T ) Jh1, si ;P h2, siK misprediction. And this is
precisely what would happen if the protocol were implemented. For the same reason
the proof carried out in Example 8.4 is no longer available, while that in Example
8.5 may be accomplished alternatively. On the other hand, proofs involving only
the N eq predicate remain unchanged.
   Corresponding remarks apply to the BACKWARDS protocol, see [ACDG+ 19b].
   A few remarks are in order regarding the rules backtrack_eq and backtrack_-
neq. As we pointed out earlier these rules have a hybrid nature, mixing, in fact,
both Coq and LF+ judgements. They could be viewed as further additions to LF+ ,
formalising exits out of the lock monad, alternative to the (O·T op·U nlock) rule,
e.g.
Γ ` M : LNeq(hu,i,j,P,q,ki:U) Jstep P n s m tK u(i)=u(j)              Γ ` step P n s m t : T ype
                            Neq(hu,i,j,P,q,ki:U)
                      Γ`E                          [M ] : step P n s (S q) u
for a suitable new object level constructor E ·(·:·) [·] This reading however would
break the nature of LF+ as a “framework” because such rules are object-language
specific. We are currently exploring how they could be subsumed conveniently
under a general scheme for handling mechanisms for exiting monads. See also
Section 7.6.


                                                       Journal of Formalized Reasoning Vol.12, No.1
42       ·       Fabio Alessi et al.

9.    OPTIMISTIC CONCURRENCY CONTROL
In transactional systems, concurrency control (CC) ensures that concurrent oper-
ations generate correct results, still taking advantage of parallelism in speeding up
the management of possibly remote operations. The optimistic approach (OCC),
in particular, assumes that transactions do not interfere frequently; hence, trans-
actions are allowed to access resources without implementing lock mechanisms.
   When a transaction A is completed and “commits” the shared resources trying
to make permanent the modifications it has carried out, the concurrency control
manager checks that no other transaction B, which has committed after A was
“activated”, has already modified the data that A has used, i.e. read or written.
If the check reveals interference , A “rolls back” i.e. it is restarted, otherwise it is
allowed to commit its modifications, which are therefore made permanent.
   In this section, we approach formally OCC in LF+ by formalising the semantics
of the Simple Transaction Language (STL) [CDK02], a language which is usually
adopted by textbooks addressing concurrency control of transactional systems.
   Throughout the section we assume that transactions modify resources only locally
before committing. A generic transaction i may perform the following actions:
     start(i)       ,   activation (first action of the transaction)
     read(i, j)     ,   reading on resource j
     write(i, j)    ,   writing to resource j
     check(i)       ,   checking against interference (last action): commit vs roll back
We represent both transactions and resources by means of natural numbers; hence,
schedules are finite sequences of actions, carried out by the former on the latter:
                     T , N                                         Transaction
                     R , N                                         Resource
                     A ::= start(i) | check(i) |         i∈T       Action
                           read(i, j) | write(i, j)      j∈R
                     S ::= (ι7→Aι )ι∈[1..m]              m∈N       Schedule
To design a possible semantics for OCC, we use the following data structures:
      ctr    ,   stack(A)              activation control (only start and check actions)
      seq    ,   T * queue(A)          actions by transactions, in sequencial order
      usr    ,   T * list(R)           used resources (by transactions)
      wrt    ,   R * list(T )          writing transactions (to resources),
   We use these datatypes6 to implement concurrency and diagnose interference as
follows. When transactions start (via start), we push on top of the stack ctr such
an information. Then, we keep recording the resources used by transactions (via
read and write) in usr, and the transactions writing to them (via write) in wrt;
correspondingly, we collect all the actions carried out by transactions, in sequential
order, in seq. Note that if a write(i, j) action takes place, we intend that the same
resource j has been also read by the transaction i.

6 The   type of wrt goes in the opposite direction, just for convenience in implementing checks.


Journal of Formalized Reasoning Vol.12, No.1
                                             LF+ in Coq for fast-and-loose reasoning                    ·     43

   The crucial (potentially conflicting) action is check(i), when two mutually exclu-
sive alternatives arise: either there is no transaction k which has committed after
the activation of i (i.e. we do not find any check(k) on top of start(i) in ctr), or at
least one of such transactions does exist.
   In the first case no interference occurs, and therefore we may both register the
successful conclusion of i (by pushing check(i) on the top of ctr) and consider
permanent its actions, just by leaving unchanged the usr and wrt datatypes.
   In the second alternative scenario (when one or more occurrences of check(k)
are on top of start(i) in ctr) a deeper validation process has to be undertaken,
by computing the intersection of the resources used by i with those written by the
potentially interfering transactions k. In case the intersection set is empty we are in
the previous non-interference scenario. If at least one resource used by i and written
by k does exist, we remove the (activation of the) transaction i (i.e. start(i)) from
ctr and erase i from usr and wrt; and we evaluate sequentially i from its beginning
by appending its actions, collected in seq, on top of the current schedule.
   Some remarks are in order. First, it is apparent that the readings and writings
of successfully committing transactions must not be deleted, because their actions
are needed to be checked against potential future interferences. Second, coherently
w.r.t. the toy-languages usually introduced by textbooks that address concurrency
control, e.g. [CDK02], we give an abstract semantics, i.e. we do not consider a store
structure to record the values “read from” and “written to” resources. We could
easily do so, but this would pointlessly obscure matters.
   To formalise the OCC that we have conceived, we introduce a small-step seman-
tics, whose intended meaning is to process list-like schedules S ∈ sch, till they are
emptied, by transforming the initial state h[ ], ↑, ↑, ↑i ∈ M≡ctr × seq × usr × wrt
into the final one. Hence, we define the relations 7→ ⊆ sch × M × sch × M and
=⇒ ⊆ sch × M × M, namely7 :
                                                        {S, N } 7→ {[ ], N 0 }
                                       (empty)                                      (stop)
                     {[ ], N } =⇒ N                        {S, N } =⇒ N 0

                       {S, N } 7→ {S 0 , N 0 }   {S 0 , N 0 } 7→ {S 00 , N 00 }
                                                                                  (trans)
                                    {S, N } 7→ {S 00 , N 00 }

                                                                                            (start)
               {s(i)::S, M } 7→ {S, hpush(s(i), c), enqueue(s(i), si ), u, wi}

                                                                                             (read)
              {r(i, j)::S, M } 7→ {S, hc, enqueue(r(i, j), si ), cons(j, ui ), wi}

                                                                                                  (write)
        {w(i, j)::S, M } 7→ {S, hc, enqueue(w(i, j), si ), cons(j, ui ), cons(i, wj )i}

                                                                                                      (opt)
       LOpt(hi,M i:C) J{c(i)::S, M } 7→ {S, hpush(c(i), c), enqueue(c(i), si ), u, wi}K

                                                                                                              (itf)
LItf(hi,M i:C) J{c(i)::S, M } 7→ {S 0 , hremove(s(i), c), empty(si ), empty(ui ), delete(i, wi}K

7 To save space, we shorten the notation for actions to their contracted versions (e.g. start(i)

becomes s(i)) and we use subscripts for the components of the state (e.g. s(i) ∈ seq is written si ).
                                                           Journal of Formalized Reasoning Vol.12, No.1
44      ·        Fabio Alessi et al.

where we make use of the following notations: M = hc, s, u, wi; S 0 = append(
enqueue(check(i), si ), S) in the last rule; C = T ×M in the last two rules. The
(non-)interference conditions, that we encode via lock-types (one is the negation of
the other, as in Section 8) are defined by:
            Itf(hi, M i, C) , ∃k∈T. ∃h∈R. check(k)c start(i) ∧ h∈ui ∧ k∈wh
            Opt(hi, M i, C) , ∀k∈T. ¬check(k)c start(i) ∨
                                    check(k)c start(i) ⇒ (∀h∈ui . k6∈wh )
where the notation “c ” represents that the lefthand side precedes, i.e. “is on the
top of”, the righthand side in the stack c.
  The non-self evident functions adopted in the semantics are defined as follows8 :
      remove(a, c) , if top(c)=a then pop(c) else push(top(c), remove(a, pop(c)))
      delete(i, w) , erase(i, wj ) ∀write(i, j)∈si
      erase(i, wj ) , if wj =[ ] then [ ] else if wj =h::l then
                      if h=i then erase(i, l) else h::erase(i, l)
In our semantics, the intended meaning of {S, M } 7→ {[ ], N } is that the schedule
S in the state M completes its processes, by transforming M into N .
9.1     Formalisation in Coq
All these structures could be promptly defined in LF+ and then encoded in Coq
as we did in Section 8. For the sake of brevity, we skip such a phase, and work
directly in Coq, since the role and behaviour of lock-types is not affected by this
choice. Thus we take advantage of Coq’s native inductive features and use the
built-in notion of Leibniz equality, natural numbers for defining transactions and
resources, and lists to define schedules. It is convenient to model also actions as an
inductive type, because in the semantics we need decidability of equality on actions,
which has to proved by (double) induction on the actions themselves. Hence we
put:
Definition trs: Set := nat.
Definition res: Set := nat.
Inductive act: Set := start: trs -> act | read: trs -> res -> act
                    | write: trs -> res -> act | check: trs -> act.
Definition sch: Set := list act.
Lemma eq_dec_act: forall a b: act, {a = b} + {a <> b}. ...
To gain efficient projection functions, as in Section 8 we encode via inductive types
both the type T of the input to the oracle, i.e. a transaction and a state, and the
state type itself, which is formed by a cartesian product of four components:
Definition ctr: Set := list act.
Definition seq: Set := list (list act).
Definition usr: Set := list (list res).
Definition wrt: Set := list (list trs).
Inductive state: Set := quad: ctr -> seq -> usr -> wrt -> state.
Definition pr1 (x:state): ctr := match x with quad c s u w => c end. ...
Inductive T: Set := pair: trs -> state -> T.
Definition left (y:T): trs := match y with pair i M => i end. ...

8 Notice    that, in rule (itf), delete(i, w) has to be computed before emptying si through empty(si ).
Journal of Formalized Reasoning Vol.12, No.1
                                      LF+ in Coq for fast-and-loose reasoning       ·     45

We have rendered also the state components as lists. Some remarks are in order:
— the activation control ctr, being a stack datatype, is naturally modeled by a
 list;
— sequential actions seq, used resources usr, writing transactions wrt, being all
 partial functions, are lists of lists, where the n-th list represents the application
 of the corresponding function to n, the empty list representing undefined values;
— the queue seq is also represented, albeit inefficiently, by a list.
The oracle predicates are considerably more involved w.r.t. the ones in previous
sections. We need to formalise the “c ” predicate (on_top_of) and a polymorphic
function which selects the n-th component of a list of lists, namely:
Fixpoint on_top_of (k i:trs)(L:list act){struct L}: Prop := ...
Fixpoint select (i:nat)(A:Set)(LL:list(list A)) {struct i}: list A := ...
Definition Itf := fun z:T => exists k:trs, exists h:res,
                  on_top_of k (left z) (pr1 (right z)) /\
                  In h (select (left z) trs (pr3 (right z))) /\
                  In k (select h trs (pr4 (right z))).
Definition Opt := fun z:T => forall k:trs,
                  (not (on_top_of k (left z) (pr1 (right z)))) \/
                  (on_top_of k (left z) (pr1 (right z)) ->
                  forall h:res, In h (select (left z) trs (pr3 (right z))) ->
                  not (In k (select h trs (pr4 (right z))))).
Full details appear in the web-appendix [ACDG+ 19b].
  The small-step semantics is finally encoded as a predicate, via suitable auxiliary
functions that update the state (the full code is available at [ACDG+ 19b]):
Parameter step: sch -> state -> sch -> state -> Prop. ...
Parameter eval: sch -> state -> state -> Prop. ...

9.2   Example: lost update
The formalisation we have introduced allows us to master typical correctness prob-
lems, a.k.a. anomalies, that may occur in transactional systems, such as e.g. lost
update, inconsistent read, ghost update. To manage, for example, the first kind of
anomaly, let us consider the following schedule, where two transactions a and b
operate concurrently on a resource x that initially contains the n value:
           Transaction a                           Transaction b
        start(a), read(a, x)
                                    start(b), read(b, x), write(b, x), check(b)
       write(a, x), check(a)
We assume, for instance, that both transactions calculate the successor of x and
then write its new value. It is apparent that check(b) succeeds whereas check(a)
does not, i.e. the transaction a must be rolled back, otherwise the final value stored
in x would be incorrectly n+1, being thus lost the effect of the b transaction.
   We outline some of the formal steps in the execution of the above schedule. First
we define:
S = [start(a), read(a, x), start(b), read(b, x), write(b, x), check(b), write(a, x), check(a)]
T = [start(a), read(a, x), write(a, x), check(a)]
                                                Journal of Formalized Reasoning Vol.12, No.1
46      ·       Fabio Alessi et al.

An interference is diagnosed by our formal system when a prompts to commit,
because check(b) is on top of start(a) in the stack (first line below), and b has
written to the resource x (fifth line), in turn read by a (first list of the fourth line):
      {S, h[ ], ↑, ↑, ↑i} 7→ {[check(a)], h[check(b), start(b), start(a)],
                                           [[start(a), read(a, x), write(a, x)],
                                            [start(b), read(b, x), write(b, x), check(b)]],
                                           [[x, x], [x, x]],
                                           [[a, b]]i}
Therefore, the transaction a is rolled back, with the following immediate effect:
                     7→ {T, h[check(b), start(b)],
                             [[ ],
                              [start(b), read(b, x), write(b, x), check(b)]],
                             [[ ], [x, x]],
                             [[b]]i}
Afterwards, a can be processed successfully, hence the schedule is eventually emp-
tied:
            {S, h[ ], ↑, ↑, ↑i} 7→ {[ ], h[check(a), start(a), check(b), start(b)],
                                          [[start(a), read(a, x), write(a, x), check(a)],
                                           [start(b), read(b, x), write(b, x), check(b)]],
                                          [[x, x], [x, x]],
                                          [[a, b]]i}
   The goal is accomplished via Coq’s top-down editor similarly to what was done
in the previous case study on branch prediction in Section 8. Apart from requiring
to deal with more involved datatypes and semantics, the application presented in
this section does not demand for the development of new specifications or proof
techniques w.r.t. Section 8, see [ACDG+ 19b].
9.3    Adequacy
The optimistic concurrency control system, which we have modeled in this section,
has quite a different purpose from the branch prediction application. The latter
tries to speedup the computation within CPUs, whereas OCC handles transactions
which may be remote w.r.t. each other and w.r.t. the resources they use.
   Again, as for branch prediction, we claim that our formalisation models all pos-
sible outcomes of an OCC system, simply because it is always possible to take the
“correct” management action, and use the top-unlock rule to get rid of the lock.
Hence it is adequate in the sense of Claim 8.6.
  Claim 9.1 (Adequacy of Coq signature for OCC). Let be {A} −→∗ {B}
the representation of a concurrent transaction carried out by an OCC system. Given
schedules S, T ∈ sch, states s, t ∈ state, and P ∈ {Opt, Itf }:
                Soundness:    If Γ ` step S s T t then {S, s} −→∗ {T, t}
                Completeness: If {S, s} −→∗ {T, t} then Γ ` step S s T t
  Modeling optimistic concurrency control requires only the use of the top-unlock
rule. But the logical setting that we have defined in Coq in this section is quite gen-
Journal of Formalized Reasoning Vol.12, No.1
                                      LF+ in Coq for fast-and-loose reasoning       ·     47

eral and could allow us to model also other concurrency control strategies, different
from the optimistic one. We do not elaborate on these.

10.   CONCLUSION
This paper is a significant enhancement and expanded version of [ACDG+ 19a]. We
present LF+ , a generalisation of the Lax Logical Framework LLFP , introduced in
[HLMS17]. The novel features of this framework w.r.t. previous ones are a more
expressive lock-type system, as well as a streamlined and simplified rule-system
and notation. We show, furthermore, how to use Coq as a proof development
environment, supporting mechanised proof search, for a version of LF+ in which
the predicates used in locks are Coq-definable. This is achieved by giving a shallow,
actually definitional, implementation of LF+ in Coq. A specific adequacy result, see
Theorem 5.1, puts the encoding on firm ground.
   In this paper we discuss in detail the monadic nature of locks and give a repertoire
of logical situations and attitudes which we believe can benefit from an analysis in
terms of lock-types. These range from the historically significant example of the
regula falsi to squash types. An emerging family of such proof attitudes we term
fast-and-loose reasoning paradigms, following [DHJG06]. These arise in situations
where boring and cumbersome checks are postponed until they are worthwhile,
but go well beyond these examples, leading to seemingly unrelated programming
techniques such as branch prediction circuits and concurrency control systems. The
main pragmatic contributions of this paper are the two case studies which illustrate
how locks in LF+ can model adequately such techniques. More work needs to be
done in order to streamline adequacy results for the various protocols used in such
contexts.
   One may legitimately ask why should a user go through the overhead of learning
LF+ rather than utilise directly the Coq encoding. First, there are pragmatic moti-
vations. When a proof is expressed using LF+ we can use in principle also external
tools, and LF+ shows how to encapsulate them. Encoding predicates in Coq might
be a cumbersome task or might even not be possible. There are also cognitive
motivations. As all logical frameworks, also LF+ is normative. The very process of
formalising a reasoning pattern, highlighting where up-to reasoning steps can arise
using LF+ , renders the argument conceptually easier to grasp and hence to formalise
in a Logical Framework. Factoring out patterns introduces a uniform perspective
which can be more easily transferred than an ad hoc approach. Moreover an ad hoc
encoding in Coq is more prone to being inadequate.
   The very idea of reasoning formally on fast-and-loose reasoning patterns has not
been considered before, to our knowledge, in the context of Type Theory, while
it arose naturally in the LF+ perspective. We believe that reasoning up-to is an
almost ubiquitous (albeit under diverse formats) irreducible cognitive pattern. To
increase the transparency of a formalisation, it deserves therefore to be dealt with
by a primitive notion such as that of lock-type.
   However more work needs to be done to understand fully the connections between
lock-types, proving and programming up-to-equivalence, monads, and fast-and-loose
reasoning. We feel, however, that in this paper we have provided clear indications
of the conceptual relationship relating these notions.

                                                Journal of Formalized Reasoning Vol.12, No.1
48     ·     Fabio Alessi et al.

   Our definitional implementation suggests how to rapidly prototype editors for
other calculi such as CLLFP? , see [HLMS17], or extensions of LF+ which support
an algebraic structure of locks.
   There are many questions still to be asked about lock-types. The most natural
one is: what are the logical limitations, if any, in having considered only typing
judgements as predicates in locks? Since our predicates can access the whole envi-
ronment, everything, in principle, can be represented via a predicate on a judgement.
Of course opaque encodings might arise in doing this, so there could be a point in
introducing predicates on other kinds of judgements, such as equality judgements,
or in making the logical structure of predicates more visible and thus accessible
to the user. Many possibilities are open, even considering judgements in different
contexts, provided predicates are well-behaved.
   Besides the many suggestions briefly sketched in the paper, an important case
study related to the fast-and-loose philosophy which we intend to develop is that
of Fitch-Prawitz consistent Set Theory, [HLLS16]. This is a natural proof theoretic
counterpart of the naı̈ve Set Theory used in developing ordinary mathematics (see
also [Gir98]).
   It would be interesting to address the issue of extending full-fledged locks to Coq
itself. To this end connections with the paper [CSW14] should be explored, for its
approach in combining different proof systems.
   Finally, we intend to explore how to prototype an alternate editor for LF+ using
the MMT UniFormal Framework of F. Rabe, [RK13]. Indeed, there exists already
an implementation of LLFP in MMT (see, e.g., [MR19]); hence, it should be intrigu-
ing to develop and compare a new encoding, taking into account the new alternative
lock-rules of LF+ presented in Section 2.

References
[ACDG+ 19a] F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell, and
            M. Lenisa. A definitional implementation of the lax logical framework
            LLFP in coq, for supporting fast and loose reasoning. In D. Miller
            and I. Scagnetto, editors, Proceedings of the Fourteenth Workshop
            on Logical Frameworks and Meta-Languages: Theory and Practice,
            LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019, volume
            307 of EPTCS, pages 8–23, 2019. doi:10.4204/EPTCS.307.3.
[ACDG+ 19b] F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell,
            M. Lenisa, and I. Scagnetto. The Web appendix of this pa-
            per.    https://users.dimi.uniud.it/~alberto.ciaffaglione/
            LLFP/JFR-19.tar.gz, 2019.
[AHMP92]    A. Avron, F. Honsell, I. Mason, and R. Pollack. Using Typed Lambda
            Calculus to Implement Formal Systems on a Machine. Journal of
            Automated Reasoning, 9(3):309–354, 1992.
[Bar84]     H. Barendregt. Lambda Calculus: its Syntax and Semantics. North
            Holland, 1984.
[BB02]      H. Barendregt and E. Barendsen.          Autarkic computations in
            formal proofs.      J. Autom. Reasoning, 28(3):321–336, 2002.
            doi:10.1023/A:1015761529444.
Journal of Formalized Reasoning Vol.12, No.1
                                  LF+ in Coq for fast-and-loose reasoning       ·     49

[CDK02]     G. Coulouris, J. Dollimore, and T. Kindberg. Distributed systems -
            concepts and designs (3. ed.). International computer science series.
            Addison-Wesley-Longman, 2002.
[Cia11]     A. Ciaffaglione. A coinductive semantics of the unlimited register ma-
            chine. In F. Yu and C. Wang, editors, Proceedings 13th International
            Workshop on Verification of Infinite-State Systems, INFINITY 2011,
            Taipei, Taiwan, 10th October 2011., volume 73 of EPTCS, pages 49–
            63, 2011. doi:10.4204/EPTCS.73.7.
[Coq18]     The Coq Development Team. The Coq Reference Manual - Release
            8.8.2. https://coq.inria.fr, 2018.
[CSW14]     C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and
            programs in a dependently typed language. In S. Jagannathan and
            P. Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Sym-
            posium on Principles of Programming Languages, POPL ’14, San
            Diego, CA, USA, January 20-21, 2014, pages 33–46. ACM, 2014.
            doi:10.1145/2535838.2535883.
[Cut80]     N. Cutland. Computability - An introduction to recursive function
            theory. Cambridge University Press, 1980.
[CWB+ 12]   J. Chabert, C. Weeks, E. Barbin, J. Borowczyk, J. Chabert,
            M. Guillemot, A. Michel-Pajus, A. Djebbar, and J. Martzloff. A
            History of Algorithms: From the Pebble to the Microchip. Springer
            Berlin Heidelberg, 2012. URL https://books.google.it/books?
            id=XcDqCAAAQBAJ.
[DFH95]     J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract
            syntax in coq. In M. Dezani-Ciancaglini and G. Plotkin, editors,
            Typed Lambda Calculi and Applications, pages 124–138, Berlin, Hei-
            delberg, 1995. Springer Berlin Heidelberg.
[DH94]      J. Despeyroux and A. Hirschowitz. Higher-order abstract syntax
            with induction in coq. In F. Pfenning, editor, Logic Programming
            and Automated Reasoning, pages 159–173, Berlin, Heidelberg, 1994.
            Springer Berlin Heidelberg.
[DHJG06]    N. A. Danielsson, J. Hughes, P. Jansson, and J. Gibbons. Fast and
            loose reasoning is morally correct. In J. G. Morrisett and S. L. Pey-
            ton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT
            Symposium on Principles of Programming Languages, POPL 2006,
            Charleston, South Carolina, USA, January 11-13, 2006, pages 206–
            217. ACM, 2006. doi:10.1145/1111037.1111056.
[Dyb96]     P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors,
            Types for Proofs and Programs, pages 120–134, Berlin, Heidelberg,
            1996. Springer Berlin Heidelberg.
[Fit52]     F. B. Fitch. Symbolic logic. New York, 1952.
[Gir98]     J.-Y. Girard. Light linear logic. Information and Computation,
            143(2):175 – 204, 1998. doi:https://doi.org/10.1006/inco.1998.2700.



                                            Journal of Formalized Reasoning Vol.12, No.1
50     ·     Fabio Alessi et al.

[HHP93]          R. Harper, F. Honsell, and G. D. Plotkin. A framework for defining
                 logics. J. ACM, 40(1):143–184, 1993. doi:10.1145/138027.138060.
                 Preliminary version in Proc. of LICS’87.
[HLL07]          F. Honsell, M. Lenisa, and L. Liquori. A framework for defining logi-
                 cal frameworks. Volume in Honor of G. Plotkin, Electr. Notes Theor.
                 Comput. Sci., 172:399–436, 2007. doi:10.1016/j.entcs.2007.02.014.
[HLL+ 12]        F. Honsell, M. Lenisa, L. Liquori, P. Maksimović, and I. Scagnetto.
                 Lfp: A logical framework with external predicates. In Proceedings
                 of the Seventh International Workshop on Logical Frameworks and
                 Meta-languages, Theory and Practice, LFMTP ’12, pages 13–22, New
                 York, NY, USA, 2012. ACM. doi:10.1145/2364406.2364409.
[HLLS08]         F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto. A conditional
                 logical framework. In LPAR’08, volume 5330 of LNCS, pages 143–
                 157. Springer-Verlag, 2008.
[HLLS16]         F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto. Implementing
                 cantor’s paradise. In A. Igarashi, editor, Programming Languages and
                 Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam,
                 November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes
                 in Computer Science, pages 229–250, 2016. doi:10.1007/978-3-319-
                 47958-3 13.
[HLMS15]         F. Honsell, L. Liquori, P. Maksimović, and I. Scagnetto. Gluing to-
                 gether proof environments: Canonical extensions of LF type theories
                 featuring locks. In I. Cervesato and K. Chaudhuri, editors, Pro-
                 ceedings Tenth International Workshop on Logical Frameworks and
                 Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Ger-
                 many, 1 August 2015., volume 185 of EPTCS, pages 3–17, 2015.
                 doi:10.4204/EPTCS.185.1.
[HLMS17]         F. Honsell, L. Liquori, P. Maksimović, and I. Scagnetto. LLFP : a
                 logical framework for modeling external evidence, side conditions,
                 and proof irrelevance using monads. Logical Methods in Computer
                 Science, 13(3), 2017. doi:10.23638/LMCS-13(3:2)2017.
[HLMS18]         F. Honsell, L. Liquori, P. Maksimović, and I. Scagnetto. Plugging-
                 in proof development environments using Locks in LF. Math-
                 ematical Structures in Computer Science, 28(9):1578–1605, 2018.
                 doi:10.1017/S0960129518000105.
[HLS14]          F. Honsell, L. Liquori, and I. Scagnetto. LaxF: Side Conditions and
                 External Evidence as Monads. In Proc. of MFCS 2014 (39th In-
                 ternational Symposium on Mathematical Foundations of Computer
                 Science), Part I, volume 8634 of Lecture Notes in Computer Science,
                 pages 327–339, Budapest, Hungary, August 2014. Springer.
[HLS+ 16]        F. Honsell, M. Lenisa, I. Scagnetto, L. Liquori, and P. Maksimović.
                 An open logical framework. J. Log. Comput., 26(1):293–335, 2016.
                 doi:10.1093/logcom/ext028.
[Hon13]          F. Honsell. 25 years of formal proof cultures: Some problems, some
                 philosophy, bright future. In Proceedings of the Eighth ACM SIG-

Journal of Formalized Reasoning Vol.12, No.1
                               LF+ in Coq for fast-and-loose reasoning       ·     51

          PLAN International Workshop on Logical Frameworks and Meta-
          languages: Theory and Practice, LFMTP’13, pages 37–42, New York,
          NY, USA, 2013. ACM. doi:10.1145/2503887.2503896.
[JKL00]   D. A. Jiménez, S. W. Keckler, and C. Lin. The impact of delay on
          the design of branch predictors. In A. Wolfe and M. S. Schlansker,
          editors, Proceedings of the 33rd Annual IEEE/ACM International
          Symposium on Microarchitecture, MICRO 33, Monterey, California,
          USA, December 10-13, 2000, pages 67–76. ACM/IEEE Computer
          Society, 2000. doi:10.1109/MICRO.2000.898059.
[KR81]    H. T. Kung and J. T. Robinson. On optimistic methods for con-
          currency control. ACM Trans. Database Syst., 6(2):213–226, 1981.
          doi:10.1145/319566.319567.
[Kri75]   S. Kripke. Outline of a theory of truth. The journal of philosophy,
          72(19):690–716, 1975.
[Mic16]   V. Michielini.      LLFP type checker.        https://github.com/
          francescodellamorte/llfp-type-checker, 2016.
[MLS84]   P. Martin-Löf and G. Sambin. Intuitionistic type theory, volume 9.
          Bibliopolis Naples, 1984.
[Mog91]   E. Moggi. Notions of computation and monads. Information and
          Computation, 93(1):55 – 92, 1991. doi:https://doi.org/10.1016/0890-
          5401(91)90052-4. Selections from 1989 IEEE Symposium on Logic in
          Computer Science.
[MR19]    D. Müller and F. Rabe. Rapid Prototyping Formal Systems in MMT:
          5 Case Studies. In LFMTP 2019 Logical Frameworks and Meta-
          Languages: Theory and Practice 2019, Vancouver, Canada, June
          2019. URL https://hal.archives-ouvertes.fr/hal-02150167.
[Plo75]   G. Plotkin.      Call-by-name, call-by-value and the λ-calculus.
          Theoretical Computer Science,          1(2):125 – 159,        1975.
          doi:https://doi.org/10.1016/0304-3975(75)90017-1.
[Pra65]   D. Prawitz.      Natural Deduction. A Proof Theoretical Study.
          Almqvist Wiksell, Stockholm, 1965.
[RK13]    F. Rabe and M. Kohlhase. A scalable module system. Inf. Comput.,
          230:1–54, 2013. doi:10.1016/j.ic.2013.06.001.
[Uni13]   T. Univalent Foundations Program. Homotopy Type Theory: Univa-
          lent Foundations of Mathematics. https://homotopytypetheory.
          org/book, Institute for Advanced Study, 2013.




                                         Journal of Formalized Reasoning Vol.12, No.1
