Implicit Complexity and Formal Proofs
H. Férée & S. Hym & M. Mayero & J.-Y. Moyen & D. Nowak
Jean-Yves.Moyen@lipn.univ-paris13.fr
School of Computing, University of Kent, United Kingdom
CRIStAL, CNRS & University of Lille, France
LIPN, University of Paris 13, France

October 10-11 2018

FHMMN

QI+CoqElica’18

1 / 27

What is this talk about?

Formal proof in Coq of the P-criterion: “PPO + QI ≡ Ptime”.
Tool, integrated with Coq, to help show that a program satisfies
the P-criterion.
Some tricks and learning that could be useful for further similar
projects.

FHMMN

QI+CoqElica’18

2 / 27

Motivation: Cryptography

The need for formal proofs

Cryptography needs to prove security of its protocols.
“Paper” proofs are often discovered wrong a few year later.
Formal proofs are needed.

FHMMN

QI+CoqElica’18

4 / 27

The need for formal proofs

Cryptography needs to prove security of its protocols.
“Paper” proofs are often discovered wrong a few year later.
Formal proofs are needed.
Security:
Adversary gives me 2 plain texts. I randomly chose one andencrypt it. Adversary guesses which one.
Protocol is secure if Adversary guesses correctly with probability 0.5

FHMMN

QI+CoqElica’18

4 / 27

The need for formal proofs

Cryptography needs to prove security of its protocols.
“Paper” proofs are often discovered wrong a few year later.
Formal proofs are needed.
Security:
Adversary gives me 2 plain texts. I randomly chose one andencrypt it. Adversary guesses which one.
Protocol is secure if Adversary guesses correctly with probability 0.5
Against all Adversaries? No! Ptime Adversaries are enough.
Formal proof of security needs to quantify “For all adversaries
running in polynomial time”.

FHMMN

QI+CoqElica’18

4 / 27

The need for ICC“For all adversaries running in polynomial time”
Formalise polynomial Turing Machines?

FHMMN

QI+CoqElica’18

5 / 27

The need for ICC“For all adversaries running in polynomial time”
Formalise polynomial Turing Machines?
Not that uniform definition (number of tapes, heads, . . . )Need to handle clocks and bounds.
I Extremely hard to actually program an adversary (or thealgorithm).
I ICC provides nice, machine-free, somewhat expressive
characterisations of Ptime.
I
I

FHMMN

QI+CoqElica’18

5 / 27

A long term Work

Formalisation of Bellantoni&Cook system [Heraud&Nowak, 2011].

FHMMN

QI+CoqElica’18

6 / 27

A long term Work

Formalisation of Bellantoni&Cook system [Heraud&Nowak, 2011].
I

Still very hard to program. . . (Binary addition takes 3 pages in
H. Rose’s classical book on Primitive recursion).

FHMMN

QI+CoqElica’18

6 / 27

A long term Work

Formalisation of Bellantoni&Cook system [Heraud&Nowak, 2011].
I

Still very hard to program. . . (Binary addition takes 3 pages in
H. Rose’s classical book on Primitive recursion).

Shonan meeting organised by D. Nowak (2013).
I

Quasi-Interpretations offer a good mix between expressivity andsimplicity.

FHMMN

QI+CoqElica’18

6 / 27

A long term Work

Formalisation of Bellantoni&Cook system [Heraud&Nowak, 2011].
I

Still very hard to program. . . (Binary addition takes 3 pages in
H. Rose’s classical book on Primitive recursion).

Shonan meeting organised by D. Nowak (2013).
I

Quasi-Interpretations offer a good mix between expressivity andsimplicity.

Presentation of a preliminary version of this work [Dice 2016].
I
I

Only soundness was proved.
No really interesting example, poor tool (little automation).

FHMMN

QI+CoqElica’18

6 / 27

A long term Work

Formalisation of Bellantoni&Cook system [Heraud&Nowak, 2011].
I

Still very hard to program. . . (Binary addition takes 3 pages in
H. Rose’s classical book on Primitive recursion).

Shonan meeting organised by D. Nowak (2013).
I

Quasi-Interpretations offer a good mix between expressivity andsimplicity.

Presentation of a preliminary version of this work [Dice 2016].
I
I

Only soundness was proved.
No really interesting example, poor tool (little automation).

Conference paper in the formal proofs community [CPP 2018].

FHMMN

QI+CoqElica’18

6 / 27

The toolMotivating example

Modular exponentiation: expmod(x, y, m) = xy [m]Central in many modern cryptographic algorithms.
Polynomiality is not trivial and needs careful use of the modulo.
30 function symbols, 110 rules.

FHMMN

QI+CoqElica’18

8 / 27

Modular exponentiation: the good parts

Interface module, writing TRS is (arguably) easy.
Rules are mostly obtained by extraction from (proven) Coq code.
Very little adhoc code.
Code is proven semantically correct.
Termination by PPO is entirely automatic.
Finding QIs is incremental, guided, and supported by the proof
assistant (use of full Arithmetic to prove inequalities between
polynomials). Most rules are solved by a couple of tactics leaving
only the burden of finding the QI to the user.

FHMMN

QI+CoqElica’18

9 / 27

Modular exponentiation: the bad parts

Need to add some “clock” arguments, with no computational use,just to ensure bounds.
These arguments are only needed when the function is re-used.
Without them, a QI can be found but is too big for re-use.
Thus, compositionality is not really achieved.

FHMMN

QI+CoqElica’18

10 / 27

Demo time!

The proof

From Paper to Formal: ICC
Usually, in ICC:Soundness proofs are hard (need to carefully craft a bound on the
programs). Thus somewhat detailed.
Completeness proofs are easy (need to show that a previous
system is contained in the new one). Thus often extremely short.

FHMMN

QI+CoqElica’18

13 / 27

From Paper to Formal: ICC
Usually, in ICC:Soundness proofs are hard (need to carefully craft a bound on the
programs). Thus somewhat detailed.
Completeness proofs are easy (need to show that a previous
system is contained in the new one). Thus often extremely short.
Here, on paper, completeness is usually: “It is easy to see that eachfunction in B is ordered by M P O0 . Then Lemma 4.1 of [2] provides aquasi-interpretation” (LPAR’01).
Obviously far from Formal proof.
Actually not really correct.
Still easier than proof of soundness.

FHMMN

QI+CoqElica’18

13 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).

FHMMN

QI+CoqElica’18

14 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).
Independent proof (TCS’11): around 6 (soundness) + 2(completeness) pages of proof (reduction from parallel registermachines).

FHMMN

QI+CoqElica’18

14 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).
Independent proof (TCS’11): around 6 (soundness) + 2(completeness) pages of proof (reduction from parallel registermachines).
With improved semantics (MSCS’12): around 4 pages of proof(soundness), many details skipped (not the main goal).

FHMMN

QI+CoqElica’18

14 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).
Independent proof (TCS’11): around 6 (soundness) + 2(completeness) pages of proof (reduction from parallel registermachines).
With improved semantics (MSCS’12): around 4 pages of proof(soundness), many details skipped (not the main goal).
“Master 2 level” detailed proof: around 35 (soundness) + 3(completeness) pages of proof (several “obvious” results still haveno proof).

FHMMN

QI+CoqElica’18

14 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).
Independent proof (TCS’11): around 6 (soundness) + 2(completeness) pages of proof (reduction from parallel registermachines).
With improved semantics (MSCS’12): around 4 pages of proof(soundness), many details skipped (not the main goal).
“Master 2 level” detailed proof: around 35 (soundness) + 3(completeness) pages of proof (several “obvious” results still haveno proof).
Coq proof: around 16000 (non-empty) lines of code (completeness:around 3000 lines). . .

FHMMN

QI+CoqElica’18

14 / 27

From Paper to Formal: the long way
Original proof (LPAR’01): around 3 pages of proof (reduction toLMPO).
Independent proof (TCS’11): around 6 (soundness) + 2(completeness) pages of proof (reduction from parallel registermachines).
With improved semantics (MSCS’12): around 4 pages of proof(soundness), many details skipped (not the main goal).
“Master 2 level” detailed proof: around 35 (soundness) + 3(completeness) pages of proof (several “obvious” results still haveno proof). (less than 6000 lines of LATEX)
Coq proof: around 16000 (non-empty) lines of code (completeness:around 3000 lines). . .

FHMMN

QI+CoqElica’18

14 / 27

The formal result

Soundness:

Completeness:

FHMMN

QI+CoqElica’18

15 / 27

The formal result

Soundness:bound on the size of the full derivation tree of the evaluation of aterm, including all caches at all levels.
I QIs are not bounded a priori but the bound depends on the QI(hence polynomial bound with polynomial QI).
I

Completeness:

FHMMN

QI+CoqElica’18

15 / 27

The formal result

Soundness:bound on the size of the full derivation tree of the evaluation of aterm, including all caches at all levels.
I QIs are not bounded a priori but the bound depends on the QI(hence polynomial bound with polynomial QI).
I

Completeness:
Reduction from the previous proof of BC.
Every BC program can be translated into a TRS that satisfies theP-criterion.
I Still missing a proof of (semantic) correctness of the translation.
I
I

FHMMN

QI+CoqElica’18

15 / 27

Some difficulties in the
proof

CBV
ti ↓
c(t1 , . . . , tn ) ↓
ti ↓

vi

(Constructor)

c(v1 , . . . , vn )∃j, tj ∈/ T (C)vi
f(v1 , . . . , vn ) ↓f(t1 , . . . , tn ) ↓v(Split)v

f(p1 , . . . , pn ) → r ∈ E
rσ ↓σ ∈ S p i σ = viv======================================== (Update)f(v1 , . . . , vn ) ↓v
FHMMN

QI+CoqElica’18

17 / 27

CBV with cache (memoisation)
hCi−1 , ti i ⇓ hCi , vi i
hC0 , c(t1 , . . . , tn )i ⇓ hCn , c(v1 , . . . , vn )i(Constructor)∃j, tj ∈/ T (C)hCi−1 , ti i ⇓ hCi , vi i hCn , f(v1 , . . . , vn )i ⇓ hC, vi
hC0 , f(t1 , . . . , tn )i ⇓ hC, vi(f(v1 , . . . , vn ), v) ∈ C
hC, f(v1 , . . . , vn )i ⇓ hC, vi(Split)(Read)@u/ (f(v1 , . . . , vn ), u) ∈ C f(p1 , . . . , pn ) → r ∈ E
σ ∈ S pi σ = vi hC, rσi ⇓ hD, vi=================D===[===================E= (Update)hC, f(v1 , . . . , vn )i ⇓ D {(f(v1 , . . . , vn ), v)} , v
FHMMN

QI+CoqElica’18

17 / 27

How to represent a derivation proof tree?
Inductive type, but “side” conditions are hard to enforce directly andare checked a posteriori with a well formed property.

FHMMN

QI+CoqElica’18

18 / 27

How to represent a derivation proof tree?
Inductive type, but “side” conditions are hard to enforce directly andare checked a posteriori with a well formed property.
ti ↓ vic(t1 , . . . , tn ) ↓ c(v1 , . . . , vn )FHMMN

QI+Coq(Constructor)

Elica’18

18 / 27

How to represent a derivation proof tree?
Inductive type, but “side” conditions are hard to enforce directly andare checked a posteriori with a well formed property.
ti ↓ vic(t1 , . . . , tn ) ↓ c(v1 , . . . , vn )(Constructor)

Is represented by the constructor| cbv constr : list cbv → term → value → cbv

FHMMN

QI+CoqElica’18

18 / 27

How to represent a derivation proof tree?
Inductive type, but “side” conditions are hard to enforce directly andare checked a posteriori with a well formed property.
ti ↓ vic(t1 , . . . , tn ) ↓ c(v1 , . . . , vn )(Constructor)

Is represented by the constructor| cbv constr : list cbv → term → value → cbv
corresponding to the “rule”. . . πi . . .
cbv constr [. . . πi . . .] t v =FHMMN

QI+Coqt↓v(Constructor)

Elica’18

18 / 27

Semantic Derivations must be well-formed. . . πi . . .
cbv constr [. . . πi . . .] t v =FHMMN

QI+Coqt↓v(Constructor)

Elica’18

19 / 27

Semantic Derivations must be well-formed. . . πi . . .
cbv constr [. . . πi . . .] t v =t↓v(Constructor)

Additional predicate:| cbv constr πl (capply c lt) (c capply c0 lv) ⇒andl (map wf πl) ∧ c = c0 ∧lt = map proj left πl ∧ lv = map proj right πl

FHMMN

QI+CoqElica’18

19 / 27

Semantic Derivations must be well-formed. . . πi . . .
cbv constr [. . . πi . . .] t v =t↓v(Constructor)

Additional predicate:| cbv constr πl (capply c lt) (c capply c0 lv) ⇒andl (map wf πl) ∧ c = c0 ∧lt = map proj left πl ∧ lv = map proj right πl
All theorems look like:∀...
let pi := (cbv_update ...) in
wf pi →...

FHMMN

QI+CoqElica’18

19 / 27

Semantic Derivations must be well-formed. . . πi . . .
cbv constr [. . . πi . . .] t v =t↓v(Constructor)

Additional predicate:| cbv constr πl (capply c lt) (c capply c0 lv) ⇒andl (map wf πl) ∧ c = c0 ∧lt = map proj left πl ∧ lv = map proj right πl
All theorems look like:∀...
let pi := (cbv_update ...) in
wf pi →...

(Similar to Proof Structure vs Proof Nets)
FHMMN

QI+CoqElica’18

19 / 27

Handling the existential quantifierti ↓ vi

f(v1 , . . . , vn ) ↓ v

f(t1 , . . . , tn ) ↓ v

FHMMN

QI+Coq(Split)Elica’18

20 / 27

Handling the existential quantifier∃j, tj ∈/ T (C)ti ↓ vi

f(v1 , . . . , vn ) ↓ v

f(t1 , . . . , tn ) ↓ v(Split)In effect, this means that (Split) must be followed by (Functions).

FHMMN

QI+CoqElica’18

20 / 27

Handling the existential quantifier∃j, tj ∈/ T (C)ti ↓ vi

f(v1 , . . . , vn ) ↓ v

f(t1 , . . . , tn ) ↓ v(Split)In effect, this means that (Split) must be followed by (Functions).
Adding the well-formed check:| cbv split l (cbv function . . .)(fapply f0 lt) v0 ⇒ . . .

FHMMN

QI+CoqElica’18

20 / 27

Handling the existential quantifier∃j, tj ∈/ T (C)ti ↓ vi

f(v1 , . . . , vn ) ↓ v

f(t1 , . . . , tn ) ↓ v(Split)In effect, this means that (Split) must be followed by (Functions).
Adding the well-formed check:| cbv split l (cbv function . . .)(fapply f0 lt) v0 ⇒ . . .
This corresponds to defining the semantics with a “double rule”

ti ↓ vif(p1 , . . . , pn ) → r ∈ E σ ∈ S pi σ = vi rσ ↓ v====================================== (F)f(v1 , . . . , vn ) ↓ v
f(t1 , . . . , tn ) ↓ v

FHMMN

QI+CoqElica’18(S)

20 / 27

Big Step Induction
Paper proofs rely on “call trees”, or a
relation, which amounts
to only keeping the (Update) and (Read) rules (the rest isbookkeeping for finding the leftmost outermost redex).
Building these in Coq would be tedious (plus need an extra layerof correction lemmas).

FHMMN

QI+CoqElica’18

21 / 27

Big Step Induction
Paper proofs rely on “call trees”, or a
relation, which amounts
to only keeping the (Update) and (Read) rules (the rest isbookkeeping for finding the leftmost outermost redex).
Building these in Coq would be tedious (plus need an extra layerof correction lemmas).
Instead, we prove a “big step” induction lemma:e (∀H,
e Je He ⇒ P (H))
e ⇒ P (J)e ⇒ ∀I,e P (I)e∀J,
Lemma cbv_big_induction :∀ (P : cbv → Prop),(∀ J,(∀ H, H ∈ (first_activations J) → P H) → P J) →∀ I, P I.

FHMMN

QI+CoqElica’18

21 / 27

Replacing automatic induction
Coq automatically generates structural induction principle forinductive types, but these were often not suitable for our needs.

FHMMN

QI+CoqElica’18

22 / 27

Replacing automatic induction
Coq automatically generates structural induction principle forinductive types, but these were often not suitable for our needs.
Inductive Term: Type := ...
| capply: constructor → list term → term

FHMMN

QI+CoqElica’18

22 / 27

Replacing automatic induction
Coq automatically generates structural induction principle forinductive types, but these were often not suitable for our needs.
Inductive Term: Type := ...
| capply: constructor → list term → term

Coq’s induction:∀ P, ...
(∀ c lt, P (capply c lt)) →∀ t, P t

Quantifying on all possible subterms is way too much, it is sufficient toquantify on the “good” ones (that validate the predicate):

FHMMN

QI+CoqElica’18

22 / 27

Replacing automatic induction
Coq automatically generates structural induction principle forinductive types, but these were often not suitable for our needs.
Inductive Term: Type := ...
| capply: constructor → list term → term

Coq’s induction:∀ P, ...
(∀ c lt, P (capply c lt)) →∀ t, P t

Quantifying on all possible subterms is way too much, it is sufficient toquantify on the “good” ones (that validate the predicate):∀ P, ...
(∀ c lt, (∀ t, t ∈ lt → P t) → P (capply c lt)) →∀ t, P t
FHMMN

QI+CoqElica’18

22 / 27

Completeness: from PR to TRS
The class BC, both in paper and in previous formal proof, isdefined with a “Primitive Recursive” syntax:
REC(PROJ0,1,1 , COMP(SUCCff , [ ], [PROJ1,2,3 ]),COMP(SUCCtt , [ ], [PROJ1,2,3 ]))FHMMN

QI+CoqElica’18

23 / 27

Completeness: from PR to TRS
The class BC, both in paper and in previous formal proof, isdefined with a “Primitive Recursive” syntax:
REC(PROJ0,1,1 , COMP(SUCCff , [ ], [PROJ1,2,3 ]),COMP(SUCCtt , [ ], [PROJ1,2,3 ]))We need to turn that into a Term Rewriting System (7 function
symbols and 10 rules).
Main (Coq) difficulty: create new function symbols. Using integers
is nice but need to keep a global “first available integer”.
I

Solution: use a state monad for translation.

FHMMN

QI+CoqElica’18

23 / 27

Completeness: handling induction

Hard case in inductive proofs is composition, because it’sunbounded composition (need to handle list of subterms).
We need delicate lemmas to ensure that we correctly handle thepremises.
Proposition BC_to_TRS_func_bounds bc st f:
let trs := snd (BC_to_TRS bc st) inf ∈ all_lhs_funcs trs →trs.(first) ≤ f ≤ trs.(last).

FHMMN

QI+CoqElica’18

24 / 27

Conclusion

Conclusion

Formal proof is a lot of work.
Filling in many, many small gaps.
Stating and proving some “obvious but hard to prove” lemmas.
I Correcting errors in the proof.
I
I

Hopefully, ideas or some proofs can be reused by others.
Tool with a good level of automation.

FHMMN

QI+CoqElica’18

26 / 27

Questions? . . . or Cake
(hopefully inclusive)