1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
module Chains
open Order
#set-options "--z3rlimit 10"

/// A function of type `ub (≥)` is a binary operator respecting the order (≥)
type ub #a (o: order a) = x:a -> y:a -> r:a {o x r /\ o y r}

/// `it (∇) f x0` is a sequence (a function `ℕ → t`), `f x0 ∇ it (∇) f x0 (n-1)`
let rec it (#t: Type) (#o: order t) (w:ub o) (f:t->t) (x0:t) (n: nat): t
  = if n = 0 then x0 else let xn = it w f x0 (n-1) in w xn (f xn)

/// `stabilizes` stipulates the sequence generated by `it` for an binary operator `w` stabilizes after `n` 
let stabilizes #t (#o:order t) (w:ub o) (f: t->t) (x0:t) (n:nat): prop
  = forall (i: nat). i >= n <==> it w f x0 (i+1) `o` it w f x0 i

/// A *w*idening *op*erator is a binary operator respecting a given
/// order that stabilizes at some point for every abstract operator
/// and value (whence `∀f x0. ∃n. ...`)
type wop #a (o: order a) = w: ub o {forall f x0. exists n. stabilizes w f x0 n}

/// `stabilizes_at` witnesses the time at which an `it` generated sequence stabilizes
let stabilizes_at #t (#o:order t) (w:wop o) (f:t->t) (x0:t):GTot (n:nat{stabilizes w f x0 n})
  = IndefiniteDescription.indefinite_description_ghost nat (stabilizes w f x0)

/// Miscelanous lemmas
let rec shift_it0 #t (#o: order t) (w: ub o) (f:t -> t) (x0:t) (n: nat)
  : Lemma (ensures it w f x0 (n+1) == it w f (w x0 (f x0)) n)
          [SMTPat (it w f (w x0 (f x0)) n)]
  = if n = 0 then () else shift_it0 w f x0 (n-1)
let shift_it1 #t (#o: order t) (w: ub o) (f:t -> t) (x0:t) (n: nat)
  : Lemma (ensures it w f x0 (n+2) == it w f (w x0 (f x0)) (n+1))
          [SMTPat (it w f (w x0 (f x0)) (n+1))]
  = assert ((n+1)+1 == n+2); shift_it0 w f x0 (n+1)
let equiv_lemma (x: nat) (y: pos) (right: nat -> bool)
  : Lemma (requires (forall(i:nat). i>=x <==> right i) /\ (forall(i:nat). i>=y <==> right (i+1)))
          (ensures  y == x - 1) = ()
let shift_it (#t:Type0) (#o:order t) (w:wop o) (f:t->t) (x0:t)
  : Lemma (ensures stabilizes_at w f x0=0 \/ stabilizes_at w f (w x0 (f x0))=stabilizes_at w f x0 - 1)
  = if stabilizes_at w f x0 = 0 then () else (
      let x1 = w x0 (f x0) in
      let wl, wr = stabilizes_at w f x0, stabilizes_at w f x1 in
      if wr=0 then () else (
        let p (i:nat) = it w f x0 (i+1) `o` it w f x0 i in
        assert (forall (i:nat). i>=wr <==> it w f x0 (i+2) `o` it w f x0 (i+1));
        equiv_lemma wl wr p))
let shift_it2 #t (#o: order t) (w: wop o) (f: t -> t) (α0: t)
  : Lemma (ensures it w f α0 (stabilizes_at w f α0) == it w f (α0 `w` f α0) (stabilizes_at w f (α0 `w` f α0))) (decreases stabilizes_at w f α0)
  = if stabilizes_at w f α0 = 0 then () else
      (shift_it w f α0; let α1 = α0 `w` f α0 in shift_it0 w f α0 (stabilizes_at w f α0-1))
let unfold_lemma #t (#o: order t) (w: wop o) (f:t -> t) (x: t) (n: nat)
  : Lemma (it w f x (n + 1) == it w f x n `w` f (it w f x n)) = ()
let rec it_stability #t (#o: order t) (w: ub o) f x0 (n: nat)
  : Lemma (requires it w f x0 1 `o` it w f x0 0) (ensures it w f x0 (n+1) `o` it w f x0 n)
  = if n=0 then () else it_stability w f x0 (n-1)
let equiv_lemma' (x: nat) (p: nat -> bool)
  : Lemma (requires forall(i:nat). i>=x <==> p (i+1)) (ensures forall(i:pos). i>=x+1 <==> p i)
  = let h (i:pos):Lemma (i>=x+1 <==> p i) = assert (i-1>=x <==> i>=x+1)
    in Classical.forall_intro h


/// Computes a fixpoint for `f` using widening
let rec fp0 #t (#o: order t) (w: wop o) (f:t -> t) (x0: t)
  : Tot (αn: t {αn == it w f x0 (stabilizes_at w f x0)}) (decreases (stabilizes_at w f x0))
  = let x1 = x0 `w` f x0 in if o x0 x1 && o x1 x0 then x0
    else ( shift_it w f x0; shift_it2 w f x0; fp0 w f x1)

/// Reformulation with a better type refinement
let fp #t (#o:order t) (w:wop o) (f:t->t) (x0:t): x:t{x==x `w` f x}
  = unfold_lemma w f x0 (stabilizes_at w f x0); fp0 w f x0

/// Now, we connect this formulation to (among other) our interval
/// domain
open Fixpoint

/// A operator that computes upper bound in a finite lattice is a
/// widening operator
let rec it_terminates_in_finite_lattice 
  #t (#o: order t) (w: ub o) f x0 (m: measure o)
  : Lemma (ensures exists n. stabilizes w f x0 n)
          (decreases m.max - m.f x0)
  = let x1 = x0 `w` f x0 in
    if m.f x0 = m.max then ()
    else if m.f x1 = m.f x0 then Classical.forall_intro (Classical.move_requires (it_stability w f x0))
         else (
           it_terminates_in_finite_lattice w f x1 m;
           let wn = IndefiniteDescription.indefinite_description_ghost nat (stabilizes w f x1) in
           let p (i:nat) = it w f x0 (i+1) `o` it w f x0 i in
           equiv_lemma' wn p;
           assert (forall (i: nat). i >= wn+1 <==> it w f x0 (i+1) `o` it w f x0 i);
           assert (stabilizes w f x0 (wn+1)))