Applications to program equivalence and verification

D1

while a&b do
  p
done
while a do
  q;
  while a&b do
    p;
  done
done

# ---

while a do
  if b then
    p
  else
    q
done

a,b: tests on some variables
p,q: prog actions

Uninterpreted simple imperative programs

Book by Manna

—

regex: syntax
reglang: denotational semantics
DFA: operational semantics
Kleene's theorem: reglang ≡ DFA

–

Regex over finite alphabet A

e := 0 | 1
   | a ∈ A
   | e;e
   | e+e
   | e*

Deno sem (ie, reglang).

[e]: (2^A)* = P(A*)

Denesting rule in regex: (a+b)* = ((a*b)*a*

from old compiler optimization stuff??

Equational program refinement question by Kleene??? 1956

Kozen 90s

Kleene's theorem:

Let L be a ~~regular~~ language. Then:

L = [e] is the denotational semantics of some regular exp e
L is accepted by a DFA

Chomsky hierarchy

Regular set

if it's built from an empty set, empty word, char, cat, alt, etc ???

Syntax of regexp was set up to mimick that of regular sets.

Semantics of regex being 'rational'…

Brzozowski proved L -> DFA correspondence: Brzozowski derivatives

A small step operational semantics

Derivative is with respect to letter. What is the next continuation?

Lₐ = {u | au ∈ L}

δₐ(0) = 0
δₐ(1) = 0
δₐ(c) = if a=c then 1 else 0
δₐ(e1;e2) = δₐ(e1);e2 + E(e1);δₐ(e2)
δₐ(e1+e2) = δₐ(e1) + δₐ(e2)
δₐ(e*) = δₐ(e);e*

This does not yet give a start state. We can pick it ourselves. We can give e itself as the start state.

—

What is a DFA?

S: Finite set of states
F: S -> 2
δ: S -> Sᴬ
- Only one transition allowed for each input

Write down the type to match your intent. Once you get the type right, difficult to go wrong afterwards. Kind of what Brzozowski did.

E: RE -> 2
- Tells if the re accepts the empty word
δ: RE -> REᴬ

E: RE -> 2
E(0) = false = E(a)
E(1) = true = E(a*)
E(e1;e2) = E(e1) ∧ E(e2)
E(e1+e2) = E(e1) ∨ E(e2)

E is a test. 2 is again a regex (0 or 1). Cool!

—

Is this guaranteed to have finite states? Think what happens for (a*)*

e = (a*)* e = (1;a*)(a**) = (0a* + 1a*);a** + (1a*)(a**)

(1a*)(a**) will keep repeating. => infinite number of states.

It doesn't simplify 0a* = 0 or 1a* = a*.

Soln: Look at equiv classes of derivatives.

Method1: Delete repeated term in a plus. If one deletion is found, that's it.

Brzozowski: Take derivative wrt ACI (assoc, comm, idempotency) ACI ould've been obtained for free if we had δₐ(e): RE -> P(RE)

Ie, getting a set of regex and then joining them together.

Thanks to Antimirov. Who apparently showed that RE modulo ACI is same as a 'set approach'.

Antimirov derivatives:

δₐ(0) = 0
δₐ(1) = 0
δₐ(c) = if a=c then 1 else 0
δₐ(e1;e2) = 

δₐ(e1+e2) = δₐ(e1) + δₐ(e2)
δₐ(e*) = δₐ(e);e*

Antimirov gives NFA Remove duplicates and plus them all. Thompson's construction.

allows ε transitions
Eg: for e;f final of e are connected to start of f by ε transitions

D2

We saw how to go from regex to reglang: e → Aₐ

Let's now see the other direction.

Transitions can be thought of as a square matrix S*S -> S^A

where A is alphabet

Entries will be allowed letters??? Like Mat[i][j] being a+b ?? No, they are essentially regexes.

Multiplication is Cat

What is Star?

Proof is algebraic. DBT: And relatively recent. State elim method

delete states, replace trans with regex till only 2 states are left
only 1 final state => don't delete
multiple final state ??

Example:

a+bb*a ≡ ((a+bb*a)a*b)* + 1
init and final empty

Order of state elim different => regex diff but equiv

Often, automata for things involving counting is easier to write than their regex.

Kleene's original question: Given two regex, can we show that they are equiv?

Kleene algebra is a structure.

(K,0,1,+,;,*)

K: Set
0,1: constants
*, +, ⋅: operations

+ is ACI
0 is identity of +
1 is neutral element of ⋅
0 is absorbant element of ⋅

These are the laws of adjoint semi lattice. or wast it joint??

Associativty and 1 for ⋅: monoid

Also a semiring. How??

–

Unfolding of star can be done on either side:

e* ≡ 1 + e;e* e* ≡ 1 + e*;e

An ordering.

e≤f ↔︎ e+f≡f

(kind of like a subset relation)

aka natural order on a semiring.

e;x + f ≤ x
------------
e*f ≤ x

(replace sth with no star, with sth with a star)

e* = least fixed point of the order ≤ (axiomatized ???)

Saloma conjecture was answered later.

HW:

x*x* ≡ x*
x* ≡ (x*)*
xy = yz → x*y ≡ yz*
(a+b)* ≡ (a*b)*a*
- This is hard. denesting rule

Kleene algebra examples:

2^(A*): Set of all (regular?) languages: (2^(A*), ∅, {ε}, ∪, ⋅, *)
binary relations: (Rel, ∅, Δ, ∪, ⋅, *)
- ∅: Empty relation
- Δ: Diagonal relation: relates x to x
- *: Transitive closure
(Mat(k),0,1,+, x, *)
- Mat(k): square matrices of size k ???
- 0: zero matrix
- 1: diagonal / identity matrix

Star: Define for 2x2 matrix, then inductive define.

DBT: Then what about 3x3

⎡ a  b ⎤*  = 
⎣ c  d ⎦


⎡ (a+bd*c)*    first;bd*⎤
⎣  ....        (d+ca*b)*⎦

This 2x2 matrix can be extended to larger matrix. For example, 3x3.

⎡ _  _ |_ ⎤
⎢ _  _ |_ ⎥
⎢------|--⎥
⎣ _  _ |_ ⎦

—

Kozen 1993

[e] = [f] ↔︎ e≡ₖₐf
- Soundness: LTR
- completeness: RTL

Reglang are the model. Minimum model required to describe a Kleene algebra.

Kozen's proof:

e      ≡       f
↓              ↓
Aₑ             Af
↓              ↓
Aₑ'            Af'
↓              ↓
Mₑ'    ≡       Mf'

An NFA is made from every regex.
- Using Thompson's construction (a more recent proof builds it more directly)
Determinize them.
Automata are minimized
- It is known that every DFA has a unique version modulo state renaming.
- A canonical form in a finite sequence of steps
- If they are same, the DFAs would be isomorphic

Uses matrices. Matrix of regexs like yesterday. Can be proven sound just by using KA axioms

Reasoning about simple imperative progs.

For conditionals, we need to add something more than plain KA. ie, KAT.

The tests are like tests for the current state.

KAT = KA + a boolean algebra

But how to do that?

B ⊆ K

B is a sub-algebra of K The operations got to be the same.

the BA is such that it can use he same operations as the KA

KA with a BA embedded = KAT

(K,0,1,+,;,*)

with

(B,0,1,+,;,-)

where - is complement I guess??

A = {p,q,r,s,t, b0, b1, b2}

Prog actions are with p,q
tests/conditionals are with b0,b1

Right, we need to add more euqations for KAT (only for things in B)

b+1 ≡ 1
(a+b)' ≡ a'b'
(ab)' ≡ a'+b'
ab = ba (only for BA ∵ it's conjuction, not for the general KA)
a'' = a
0' = 1

(yeah, de-Morgan's laws)

DBT: Is 1' = 0 mentioned ??

Remark: BA doesn't use the star operation. It doesn't need * to be a boolean algebra. HW: Any b* is 1.

This doesn't work for languages with effects. Our assumption: Sequential, effect-free progs.

OT: Concurrent KA

partial distributed commutative lattice ??? for tests needed.
language that allows sampling

if b then p else q ≡ bp + b'q
while b do p ≡ (bp)*b'

Compiler optimizations possible like this.

Next lecture:

reachablility in a network
netKAT ??

—-

HW:

x*x* ≡ x*

x*x*
(1+xx*)x*

D3

Semantics of KAT: deno and op

e := 0 | 1
   | p ∈ P
   | e+e
   | e;e
   | e*
   | b ∈ B

b := t ∈ T
   | 0 | 1
   | b ∨ b
   | b ∧ b
   | b'

T = set of primitive tests

Alphabet A is split into disjoint union of T and P

A = T U P

The b-s are like assert b.

After an assert, we know something about the state.

If we have an α like t1⋅t2'⋅…tn where there's a t for each variable, it's a full test or valuation.

Atoms of BA are generated by T ???

Atoms are just subset of the set of tests Think of atoms as states.

Atom = 2^T

Action = like program

α₀p₀α₁p₁α₂p₂…αₙpₙ

Take an atom, programs might change it, and we are left with a final state.

(αp)*α

BDD: Binary decision diagrams FDD = Forward DD. (essentially BDD with vals)

Damien Pous popl'15

[e]: 2^((At.P)*At)

guarded string

[b] = {α | α ≤ b} [p] = {αpβ | α β ∈ At}

p can transform any α into any β

[e+f] = [e] ∪ [f] [e;f] = [e] ◇ [f]

can't just concat because there are two guards. Last atom of e1 and first atom of e2 should be same So there's a new operator ◇ which checks the compatiblity. If not same, then it's undefined. Abort.

[if b then p else q]

Recall that this is just bp + b'q

[bp]                    U   [b'q]
[b]◇[p]
{α|α≤b}◇{αpβ|α β∈At}
{αpβ|α≤b}
{αpβ|α≤b}               +  {αqβ|α≤b'}

Finite traces

[while b do p]

{β , α₀pβ, α₀pα₁pβ, α₀pα₁pα₂pβ, …} b'

One way of considering infintie traces = 0

[while true do skip] = 0

This view

is often helpful in verification.
says that any two non-terminating progs are same!

Hoare triplets

⊢ {b} C {c}

↔

bCc' ≡ 0

Kozen:

bC ≤ Cc
a program C with precndition b has same out as a prog C without any precond that ends at postcondition c.

Let's have a look at the denesting rule.

(x+y)* ≤ (x*y)*x*

1 ≤ (x*y)*x*

1 ≤ x* 1 ≤ (x*y)*

1;1

xx*(yx*)* ≤ x*(yx*)*

ignore the yx* for now

xx* ≤ x*

(yx*)(yx*)* ≤ (yx*)* ≤ x*(yx*)*

Fixpoint and sliding rules

Example from lec1:

while b:
  p
  while c:
    q

(bp)*b'(cq)*c'

and

if b then
  p
  while b∨c
    if c then
      q
    else
      p

bp((b∨c)_)*(b∨c)' + b'
  (cq + c'p)

bp((b+c)(cq + c'p))*(b+c)' + b'
bp((b+c)(cq + c'p))*b'c' + b'

Can use denesting and sliding rules to show that these two programs are equiv.

netKAT: a special KAT POPL'15/16

Nate Foster

Packet forwarding and nodes in a network.

Packets have:

fields and each field has got a val
All vals are defined
nodes can forward/drop packets based on packet field vals (tests)
nodes can also modify value of the packet (actions)

An example netKAT prog:

sw: switch
pt: port
type ∈ {ssh, ..}
dst: destination

(sw=2);(type=ssh);  (pt ← 4);(dst←10.2.10.2)

First part filters packets. If that test passes, packet attrs are modified.

Some simplification rules:

f ← n; f ← m ≡ f ← m
f = n; f ← n ≡ f = n
f ← n; f = n ≡ f ← n

D4

NetKAT

A special action: dup/obs (duplicate, observation)

remembers what the packet looked like
eg: sw←2 ⋅ dup ⋅ sw←5
With it possible to check traces

[|f<-n|](π) = {π[n/f]}

[|f=n|](π) = {∅ if π(f)≠n {π} if π(f)=n}

is like multicast

[|e + e'|](π) = [e](π) ∪ [e'](π)

In netkat, all are complete assignments and complete tests.

~~α is not just bool, but is from a finite set ??~~

Netkat:

action and test are isomorphic, just the 'perspective' changes.

—

netkat axioms

f <- n; f <-m ≡ f←

Every field has a value. No field can be left undefined. Set of values is finite.

For a given field f,

  Σ     f = n
n ∈ Val

Two given e equivalence

[e] = [f] ↔︎ e ≡ f

by means of the netKAT axioms.

netkat

bdd instead of matrices more capable
openflow, p4
SPP (like 2-sorted BDD)

match-action table

At switch 2, for every line l

sw=2; Σ tₗ;aₗ
      l

— netkat apps

reachability check

Is B reachable from A.

top: topology
switch: switch policy

sw=A; top;(switch;top)*; sw=B

If top;(switch;top)* is 0, not reachable.

Quite efficient too.

–

Another netkat app: Forwarding loop

Does a packet keep coming back to the same switch?

Temporal NetKAT @ Princeton