## Call-by-value reduction of SK terms

Problem 2 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq scripts of the proofs made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.

Topics: Semantics of languages

Tools: Why3

References: The 2nd Verified Software Competition

see also the index (by topic, by tool, by reference, by year)

```(* The 2nd Verified Software Competition (VSTTE 2012)

Problem 2:
Combinators S and K *)

module Combinators

type term = S | K | App term term

(* specification of the CBV reduction *)

predicate is_value (t: term) = match t with
| K | S -> true
| App K v | App S v -> is_value v
| App (App S v1) v2 -> is_value v1 /\ is_value v2
| _ -> false
end

(* contexts *)

type context = Hole | Left context term | Right term context

predicate is_context (c: context) = match c with
| Hole -> true
| Left c _ -> is_context c
| Right v c -> is_value v && is_context c
end

function subst (c: context) (t: term) : term = match c with
| Hole -> t
| Left c1 t2 -> App (subst c1 t) t2
| Right v1 c2 -> App v1 (subst c2 t)
end

(* one step reduction
(the notion of context is inlined in the following definition) *)

inductive (-->) (t1 t2: term) =
| red_K:
forall c: context. is_context c ->
forall v1 v2: term. is_value v1 -> is_value v2 ->
subst c (App (App K v1) v2) --> subst c v1
| red_S:
forall c: context. is_context c ->
forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 ->
subst c (App (App (App S v1) v2) v3) -->
subst c (App (App v1 v3) (App v2 v3))

lemma red_left:
forall t1 t2 t: term. t1 --> t2 -> App t1 t --> App t2 t

lemma red_right:
forall v t1 t2: term. is_value v -> t1 --> t2 -> App v t1 --> App v t2

clone import relations.ReflTransClosure
with type t = term, predicate rel = (-->)
predicate (-->*) (t1 t2: term) = relTR t1 t2

lemma red_star_left:
forall t1 t2 t: term. t1 -->* t2 -> App t1 t -->* App t2 t

lemma red_star_right:
forall v t1 t2: term. is_value v -> t1 -->* t2 -> App v t1 -->* App v t2

(* task 1: implement CBV reduction *)

let rec reduction (t: term) : term
diverges (* there are non-normalizable terms... *)
ensures { t -->* result /\ is_value result }
= match t with
| S -> S
| K -> K
| App t1 t2 -> match reduction t1 with
| K -> App K (reduction t2)
| S -> App S (reduction t2)
| App K v1 -> let _ = reduction t2 in v1
| App S v1 -> App (App S v1) (reduction t2)
| App (App S v1) v2 ->
let v3 = reduction t2 in reduction (App (App v1 v3) (App v2 v3))
| _ -> absurd
end
end

exception BenchFailure

constant i : term = App (App S K) K

let test_SKK ()
diverges (* would be hard to prove terminating *)
raises { BenchFailure -> true }
= let t1 = reduction (App i i) in
if t1 <> i then raise BenchFailure;
let t2 = reduction (App (App (App (App K K) K) K) K) in
if t2 <> K then raise BenchFailure;
(t1, t2)

(* an irreducible term is a value *)

lemma reducible_or_value:
forall t: term. (exists t': term. t-->t') \/ is_value t

predicate irreducible (t: term) = forall t': term. not (t-->t')

lemma irreducible_is_value:
forall t: term. irreducible t <-> is_value t

use import int.Int

inductive only_K (t: term) =
| only_K_K:
only_K K
| only_K_App:
forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2)

lemma only_K_reduces:
forall t: term. only_K t ->
exists v: term. t -->* v /\ is_value v /\ only_K v

function size (t: term) : int = match t with
| K | S -> 0
| App t1 t2 -> 1 + size t1 + size t2
end

lemma size_nonneg: forall t: term. size t >= 0

let rec reduction2 (t: term) : term variant { t }
requires { only_K t }
ensures { only_K result /\ is_value result }
= match t with
| S -> S
| K -> K
| App t1 t2 -> match reduction2 t1 with
| K -> App K (reduction2 t2)
| S -> App S (reduction2 t2)
| App K v1 -> let _ = reduction2 t2 in v1
| App S v1 -> App (App S v1) (reduction2 t2)
| App (App S v1) v2 ->
let v3 = reduction2 t2 in reduction2 (App (App v1 v3) (App v2 v3))
| _ -> absurd
end
end

function ks (n: int) : term

axiom ksO: ks 0 = K
axiom ksS: forall n: int. n >= 0 -> ks (n+1) = App (ks n) K

lemma ks1: ks 1 = App K K

lemma only_K_ks: forall n: int. n >= 0 -> only_K (ks n)

lemma ks_inversion: forall n: int. n >= 0 ->
n = 0 \/ n > 0 /\ ks n = App (ks (n-1)) K

lemma ks_injective:
forall n1 n2: int. n1 >= 0 -> n2 >= 0 -> ks n1 = ks n2 -> n1 = n2

use import int.Div2

let rec reduction3 (t: term) : term
requires { exists n: int. n >= 0 /\ t = ks n }
diverges (* TODO: prove termination ... *)
ensures { is_value result /\
forall n: int. n >= 0 -> (t = ks (2*n)   -> result = K)
/\ (t = ks (2*n+1) -> result = App K K) }
= match t with
| S -> S
| K -> K
| App t1 t2 -> match reduction3 t1 with
| K -> App K (reduction3 t2)
| S -> App S (reduction3 t2)
| App K v1 -> let _ = reduction3 t2 in v1
| App S v1 -> App (App S v1) (reduction3 t2)
| App (App S v1) v2 ->
let v3 = reduction3 t2 in reduction3 (App (App v1 v3) (App v2 v3))
| _ -> absurd
end
end

lemma ks_value:
forall n: int. 0 <= n -> is_value (ks n) -> 0 <= n <= 1

lemma ks_even_odd:
forall n: int. 0 <= n -> ks (2*n)   -->* K
/\ ks (2*n+1) -->* App K K

end
```

# Why3 Proof Results for Project "vstte12_combinators"

## Theory "vstte12_combinators.Combinators": fully verified in 13.37 s

 Obligations Alt-Ergo (0.99.1) CVC3 (2.4.1) Coq (8.6.1) Eprover (1.8-001) Spass (3.7) Vampire (0.6) Z3 (3.2) red_left --- --- --- --- --- --- 3.80 red_right --- --- --- --- --- --- 3.82 red_star_left --- --- 0.27 --- --- --- --- red_star_right --- --- 0.28 --- --- --- --- 5. VC for reduction --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.01 --- --- --- --- --- --- 2. postcondition 0.01 --- --- --- --- --- --- 3. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction --- --- 0.27 --- 0.03 0.04 --- 2. VC for reduction 0.00 --- --- --- --- --- --- 4. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction --- --- 0.26 --- 0.03 0.06 --- 2. VC for reduction 0.00 --- --- --- --- --- --- 5. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction --- --- 0.22 --- 0.07 0.03 --- 2. VC for reduction 0.01 --- --- --- --- --- --- 6. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction --- --- 0.20 0.04 0.04 0.08 --- 2. VC for reduction 0.02 --- --- --- --- --- --- 7. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction --- --- 0.26 --- --- 0.32 --- 2. VC for reduction 0.01 --- --- --- --- --- --- 8. unreachable point 0.04 --- --- --- --- --- --- 6. VC for test_SKK 0.01 --- --- --- --- --- --- reducible_or_value --- --- 0.69 --- --- --- --- irreducible_is_value --- --- 1.76 --- --- --- --- only_K_reduces --- --- 0.69 --- --- --- --- size_nonneg --- --- 0.36 --- --- --- --- 11. VC for reduction2 --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.01 --- --- --- --- --- --- 2. postcondition 0.01 --- --- --- --- --- --- 3. variant decrease 0.02 --- --- --- --- --- --- 4. precondition 0.04 --- --- --- --- --- --- 5. variant decrease 0.01 --- --- --- --- --- --- 6. precondition 0.10 --- --- --- --- --- --- 7. postcondition 0.02 --- --- --- --- --- --- 8. variant decrease 0.03 --- --- --- --- --- --- 9. precondition 0.02 --- --- --- --- --- --- 10. postcondition 0.01 --- --- --- --- --- --- 11. variant decrease 0.02 --- --- --- --- --- --- 12. precondition 0.02 --- --- --- --- --- --- 13. postcondition 0.04 --- --- --- --- --- --- 14. variant decrease 0.03 --- --- --- --- --- --- 15. precondition 0.03 --- --- --- --- --- --- 16. postcondition 0.04 --- --- --- --- --- --- 17. variant decrease 0.03 --- --- --- --- --- --- 18. precondition 0.04 --- --- --- --- --- --- 19. variant decrease --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction2 --- 0.02 --- 0.01 --- --- --- 2. VC for reduction2 --- 0.02 --- 0.05 --- --- --- 3. VC for reduction2 --- 0.16 --- 0.58 --- --- --- 20. precondition --- --- --- --- --- --- --- split_goal_wp 1. precondition --- 0.07 0.29 0.61 --- --- --- 21. postcondition 0.01 --- --- --- --- --- --- 22. unreachable point 0.08 --- --- --- --- --- --- ks1 0.01 --- --- --- --- --- --- only_K_ks --- --- 0.30 --- --- --- --- ks_inversion 0.01 --- --- --- --- --- --- ks_injective --- --- 0.71 --- --- --- --- 16. VC for reduction3 --- --- --- --- --- --- --- split_goal_wp 1. postcondition 0.07 --- --- --- --- --- --- 2. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction3 0.01 0.01 --- --- --- --- 0.00 2. VC for reduction3 0.01 --- --- --- --- --- --- 3. precondition --- 0.02 --- --- --- --- --- 4. precondition --- 0.06 --- --- --- --- --- 5. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction3 0.01 --- --- --- --- --- --- 2. VC for reduction3 --- --- 1.50 --- --- --- --- 3. VC for reduction3 --- --- 0.78 --- --- --- --- 6. precondition --- 0.05 --- --- --- --- --- 7. postcondition --- --- 1.07 --- --- --- --- 8. precondition --- 0.09 --- --- --- --- --- 9. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for reduction3 0.06 0.02 --- --- --- --- 0.13 2. VC for reduction3 --- --- 0.68 --- --- --- --- 3. VC for reduction3 0.10 --- --- --- --- --- --- 10. precondition --- 0.07 --- --- --- --- --- 11. postcondition --- --- 1.86 --- --- --- --- 12. precondition --- 0.08 --- --- --- --- --- 13. precondition --- --- 0.68 --- --- --- --- 14. postcondition --- --- 0.88 --- --- --- --- 15. unreachable point 0.08 0.02 --- --- --- --- 0.04 ks_value --- --- 0.34 --- --- --- --- ks_even_odd --- --- 0.32 --- --- --- ---