example sumrange in progress, part cumulative array proved

examples/in_progress/sumrange.mlw

+
+
+module ArraySum
+
+  use export int.Int
+  use export array.Array
+
+  function sum (array int) int int : int
+  (** [sum a i j] denotes the sum Sum_{i <= k < j} a[k] *)
+
+  axiom sum_def_empty :
+    forall a : array int, i j : int. j <= i -> sum a i j = 0
+
+  axiom sum_def_non_empty :
+    forall a: array int, i j : int. i < j /\ 0 <= i < a.length ->
+      sum a i j = a[i] + sum a (i+1) j
+
+(*
+  lemma sum_right_aux : forall a x j.
+    0 < j <= a.length -> 0 < x <= j ->
+    sum a (j-x) j = sum a (j-x) (j-1) + a [j-1]
+*)
+    
+  lemma sum_right : forall a : array int, i j : int.
+    0 <= i < j <= a.length  ->
+    sum a i j = sum a i (j-1) + a[j-1]
+
+end
+
+
+
+module Simple
+
+  use import ArraySum
+  use import ref.Ref
+
+  (** [query a i j] returns the sum of elements in [a] between
+      index [i] inclusive and index [j] exclusive *)
+  let query (a:array int) (i j:int) : int
+    requires { 0 <= i <= j <= a.length }
+    ensures { result = sum a i j }
+  = let s = ref 0 in
+    for k=i to j-1 do
+      invariant { !s = sum a i k }
+      s := !s + a[k]
+    done;
+    !s
+
+end
+
+
+module CumulativeArray
+
+  use array.Array
+  use import ArraySum
+
+  predicate is_cumulative_array_for (c:array int) (a:array int) =
+    c.length = a.length + 1 /\
+    forall i. 0 <= i < c.length -> c[i] = sum a 0 i
+
+  (** [create a] builds the cumulative array associated with [a]. *)
+  let create (a:array int) : array int
+    ensures { is_cumulative_array_for result a }
+  = let l = a.length in
+    let s = Array.make (l+1) 0 in
+    for i=1 to l do
+      invariant { forall k. 0 <= k < i -> s[k] = sum a 0 k }
+      s[i] <- s[i-1] + a[i-1]
+    done;
+    s
+
+
+  lemma sum_concat : forall a:array int, i j k:int.
+    0 <= i <= j <= k <= a.length ->
+    sum a i k = sum a i j + sum a j k
+
+  (** [query c i j a] returns the sum of elements in [a] between
+      index [i] inclusive and index [j] exclusive, in constant time *)
+  let query (c:array int) (i j:int) (ghost a:array int): int
+    requires { is_cumulative_array_for c a }
+    requires { 0 <= i <= j < c.length }
+    ensures { result = sum a i j }
+  = c[j] - c[i]
+  
+
+  lemma sum_frame : forall a1 a2 : array int, i j : int.
+    0 <= i <= j ->
+    j <= a1.length ->
+    j <= a2.length ->
+    (forall k : int. i <= k < j -> a1[k] = a2[k]) ->
+    sum a1 i j = sum a2 i j
+
+
+  let rec lemma sum_update (a:array int) (i v l h:int) : unit
+    requires { 0 <= l <= i < h <= a.length }
+    variant { h }
+    ensures { sum (a[i<-v]) l h = sum a l h + v - a[i] }
+  = if h > i + 1 then sum_update a i v l (h-1)
+(*>*)
+
+  (** [update c i v a] updates cell [a[i]] to value [v] and updates
+      the cumulative array [c] accordingly *)
+  let update (c:array int) (i:int) (v:int) (ghost a:array int) : unit
+    requires { (*<a*) is_cumulative_array_for c a (*>*) } (*<e*)
+    requires { 0 <= i < a.length } (*>*)
+    writes  { (*<u*) c, a (*>*) }
+    ensures { is_cumulative_array_for c a }
+    ensures { a[i] = v }
+    ensures { forall k. 0 <= k < a.length /\ k <> i ->
+              a[k] = (old a)[k] }
+  = (*<c*) 'Init:
+    let incr = v - c[i+1] + c[i] in
+    a[i] <- v;
+    for j=i+1 to c.length-1 do
+      invariant { forall k. j <= k < c.length -> c[k] = sum a 0 k - incr }
+      invariant { forall k. 0 <= k < j -> c[k] = sum a 0 k }
+      c[j] <- c[j] + incr
+    done
+    (*>*)
+
+end
+
+
+
+
+
+
+module CumulativeTree
+
+  use array.Array
+  use import ArraySum
+  use import int.ComputerDivision
+
+  type indexes =
+    { low : int;
+      high : int;
+      isum : int;
+    }
+
+  type tree = Leaf indexes | Node indexes tree tree
+
+  function indexes (t:tree) : indexes =
+    match t with
+    | Leaf ind -> ind
+    | Node ind _ _ -> ind
+    end
+
+(* QUESTION 11 *)
+
+(*<e*)
+  predicate is_indexes_for (ind:indexes) (a:array int) (i j:int) =
+    ind.low = i /\ ind.high = j /\
+    0 <= i < j <= a.length /\
+    ind.isum = sum a i j
+(*>*)
+
+  predicate is_tree_for (t:tree) (a:array int) (i j:int) =
+    match t with
+    | Leaf ind ->
+        (*<a*) is_indexes_for ind a i j /\ j = i+1 (*>*)
+    | Node ind l r ->
+        (*<a*) is_indexes_for ind a i j /\
+        i = l.indexes.low /\ j = r.indexes.high /\
+        let m = l.indexes.high in
+        m = r.indexes.low /\
+        i < m < j /\ m = div (i+j) 2 /\
+        is_tree_for l a i m /\
+        is_tree_for r a m j (*>*)
+    end
+
+(* QUESTION 12 *)
+
+(*<e*)
+  let rec lemma sum_concat (a:array int) (i j k:int) : unit
+    requires { 0 <= i <= j <= k <= a.length }
+    variant { j - i }
+    ensures { sum a i k = sum a i j + sum a j k }
+  = if i < j then sum_concat a (i+1) j k
+(*>*)
+
+  let rec tree_of_array (a:array int) (i j:int) : tree
+    requires { (*<a*) 0 <= i < j <= a.length (*>*) }
+    variant { (*<v*) j - i (*>*) }
+    ensures { (*<a*) is_tree_for result a i j (*>*) }
+    = if i+1=j then begin
+       (*<c*) Leaf { low = i; high = j; isum = a[i] } (*>*)
+       end
+      else
+        begin
+        let m = div (i+j) 2 in
+        (*<c*)
+        assert { i < m < j };
+        let l = tree_of_array a i m in
+        let r = tree_of_array a m j in
+        let s = l.indexes.isum + r.indexes.isum in
+        assert { s = sum a i j };
+        Node { low = i; high = j; isum = s} l r
+        (*>*)
+        end
+
+(* QUESTION 13 *)
+
+  let create (a:array int) : tree
+    requires { (*<a*) a.length >= 1 (*>*) }
+    ensures { is_tree_for result a 0 a.length }
+  = (*<c*) tree_of_array a 0 a.length (*>*)
+
+
+(* QUESTION 14 *)
+
+  let rec query_aux (t:tree) (ghost a: array int)
+      (i j:int) : int
+    requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
+    requires { (*<a*) 0 <= t.indexes.low <= i < j <= t.indexes.high <= a.length (*>*) }
+    variant { (*<v*) t (*>*) }
+    ensures { (*<a*) result = sum a i j (*>*) }
+  = (*<c*)
+    match t with
+    | Leaf ind ->
+      ind.isum
+    | Node ind l r ->
+      let k1 = ind.low in
+      let k3 = ind.high in
+      if i=k1 && j=k3 then ind.isum else
+      let m = l.indexes.high in
+      if j <= m then query_aux l a (*k1 m*) i j else
+      if i >= m then query_aux r a (*m k3*) i j else
+      query_aux l a (*k1 m*) i m + query_aux r a (*m k3*) m j
+    end
+    (*>*)
+
+(* QUESTION 16 *)
+
+  let query (t:tree) (ghost a: array int) (i j:int) : int
+    requires { 0 <= i <= j <= a.length }
+    requires { (*<a*) is_tree_for t a 0 a.length (*>*) }
+    ensures { result = sum a i j }
+  = (*<c*) if i=j then 0 else query_aux t a (*0 a.length*) i j (*>*)
+
+(*<e*) (* version arthur *)
+
+predicate is_disjoint (ind:indexes) (i j:int) =
+   (j <= ind.low) || (i >= ind.high)
+
+predicate is_fully_covered (ind:indexes) (i j:int) =
+   i <= ind.low && ind.high <= j
+
+use import int.MinMax
+
+let rec query2 (t:tree) (ghost a: array int)
+      (i j:int) : int
+    requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
+(*    requires { (*<a*) 0 <= t.indexes.low <= i /\ j <= t.indexes.high <= a.length (*>*) } *)
+    variant { (*<v*) t (*>*) }
+    ensures { (*<a*) result = sum a (max t.indexes.low i) (min t.indexes.high j) (*>*) }
+= let ind = indexes t in
+  if is_disjoint ind i j then 0
+    else if is_fully_covered ind i j then ind.isum
+    else
+      match t with
+      | Leaf _ -> absurd
+         (* car on a forcément is_disjoint ou bien is_fully_covered *)
+      | Node _ l r ->
+            query2 l a i j + query2 r a i j
+          (* utiliser un lemme de découpage des intersections *)
+    end
+
+  let query3 (t:tree) (ghost a: array int) (i j:int) : int
+    requires { 0 <= i <= j <= a.length }
+    requires { (*<a*) is_tree_for t a 0 a.length (*>*) }
+    ensures { result = sum a i j }
+  = (*<c*) query2 t a i j (*>*)
+
+(*>*)
+
+(* QUESTIONS 17 and 18 *)
+
+(*<e*)
+  let rec lemma is_tree_for_frame (t:tree) (a:array int) (k v i j:int)
+    requires { 0 <= k < a.length }
+    requires { k < i \/ k >= j }
+    requires { is_tree_for t a i j }
+    variant { t }
+    ensures { is_tree_for t a[k<-v] i j }
+  = match t with
+    | Leaf _ -> ()
+    | Node _ l r ->
+      is_tree_for_frame l a k v i l.indexes.high;
+      is_tree_for_frame r a k v l.indexes.high j;
+    end
+
+  let rec lemma sum_right (a : array int) (i j : int)
+    requires { 0 <= i < j <= a.length }
+    variant { j - i }
+    ensures { sum a i j = sum a i (j-1) + a[j-1] }
+  = if i < j-1 then sum_right a (i+1) j
+
+  let rec lemma sum_frame (a1 a2 : array int) (i j : int) : unit
+    requires { 0 <= i <= j }
+    requires { j <= a1.length }
+    requires { j <= a2.length }
+    requires { forall k : int. i <= k < j -> a1[k] = a2[k] }
+    variant { j - i }
+    ensures { sum a1 i j = sum a2 i j }
+  = if i < j then sum_frame a1 a2 (i+1) j
+
+
+  let rec lemma sum_update (a:array int) (i v l h:int) : unit
+    requires { 0 <= l <= i < h <= a.length }
+    variant { h }
+    ensures { sum (a[i<-v]) l h = sum a l h + v - a[i] }
+  = if h > i + 1 then sum_update a i v l (h-1)
+(*>*)
+
+  let rec update_aux (t:tree) (i:int) (ghost a :array int) (v:int) : (tree,int)
+    requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
+(*<e*) requires { t.indexes.low <= i < t.indexes.high }
+    variant { t } (*>*)
+    returns { (t',delta) ->
+        (*<a*)  delta = v - a[i] /\
+        t'.indexes.low = t.indexes.low /\
+        t'.indexes.high = t.indexes.high /\
+        is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high (*>*) }
+  = (*<c*) match t with
+    | Leaf ind ->
+        assert { i = ind.low };
+        (Leaf { ind with isum = v }, v - ind.isum)
+    | Node ind l r ->
+        let m = l.indexes.high in
+      if i < m then
+        let l',delta = update_aux l i a v in
+        assert { is_tree_for l' a[i<-v] t.indexes.low m };
+        assert { is_tree_for r a[i<-v] m t.indexes.high };
+        (Node {ind with isum = ind.isum + delta } l' r, delta)
+      else
+        let r',delta = update_aux r i a v in
+        assert { is_tree_for l a[i<-v] t.indexes.low m };
+        assert { is_tree_for r' a[i<-v] m t.indexes.high };
+        (Node {ind with isum = ind.isum + delta} l r',delta)
+    end(*>*)
+
+(* QUESTION 19 *)
+
+  let update (t:tree) (ghost a:array int) (i v:int) : tree
+     requires { (*<a*) 0 <= i < a.length (*>*) } (*<e*)
+     requires { is_tree_for t a 0 a.length } (*>*)
+     writes { a }
+     ensures { a[i] = v }
+     ensures { forall k. 0 <= k < a.length /\ k <> i -> a[k] = (old a)[k] }
+     ensures { is_tree_for result a 0 a.length }
+  = let t,_ = (*<c*) update_aux t i a v (*>*) in
+    a[i] <- v;
+    t
+
+
+(* complexity *)
+
+  use import int.MinMax
+
+  function depth (t:tree) : int =
+    match t with
+    | Leaf _ -> 0
+    | Node _ l r -> 1 + max (depth l) (depth r)
+    end
+
+  use import ref.Ref
+
+  let rec update_compl (t:tree) (i:int) (ghost a :array int) (v:int) (ghost c:ref int): (tree,int)
+     requires { (*<a*) is_tree_for t a t.indexes.low t.indexes.high (*>*) }
+(*<e*) requires { t.indexes.low <= i < t.indexes.high }
+     requires { !c >= depth t }
+     variant { t } (*>*)
+     returns { (t',delta) ->
+        (*<a*)  delta = v - a[i] /\
+        t'.indexes.low = t.indexes.low /\
+        t'.indexes.high = t.indexes.high /\
+        is_tree_for t' a[i<-v] t'.indexes.low t'.indexes.high (*>*) }
+  = c := !c - 1;
+    match t with
+    | Leaf ind ->
+      (*<c*) assert { i = ind.low };
+        (Leaf { ind with isum = v }, v - ind.isum)
+        (*>*)
+    | Node ind l r ->
+      (*<c*)      let m = l.indexes.high in
+      if i < m then
+        let l',delta = update_compl l i a v c in
+        assert { is_tree_for l' a[i<-v] t.indexes.low m };
+        assert { is_tree_for r a[i<-v] m t.indexes.high };
+        (Node {ind with isum = ind.isum + delta } l' r, delta)
+      else
+        let r',delta = update_compl r i a v c in
+        assert { is_tree_for l a[i<-v] t.indexes.low m };
+        assert { is_tree_for r' a[i<-v] m t.indexes.high };
+        (Node {ind with isum = ind.isum + delta} l r',delta) (*>*)
+    end
+
+  use import bv.Pow2int
+
+  let rec lemma depth_is_log (t:tree) (a :array int) (k:int)
+     requires { k >= 0 }
+     requires { is_tree_for t a t.indexes.low t.indexes.high }
+     requires { t.indexes.high - t.indexes.low <= pow2 k }
+     variant { t }
+     ensures { depth t <= k }
+  = match t with
+    | Leaf _ -> ()
+    | Node _ l r ->
+       depth_is_log l a (k-1);
+       depth_is_log r a (k-1)
+    end
+
+end

examples/in_progress/sumrange/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../sumrange.mlw">
+<theory name="ArraySum" proved="true" sum="c43abcc65051af09a54f471f27f69208">
+ <goal name="sum_right" proved="true">
+ <transf name="assert" proved="true" arg1="(forall x. 0 &lt; x &lt; j -&gt; sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])">
+  <goal name="sum_right.0" proved="true">
+  <transf name="induction" proved="true" arg1="x">
+   <goal name="sum_right.0.0" proved="true">
+   <proof prover="2"><result status="valid" time="0.00"/></proof>
+   </goal>
+   <goal name="sum_right.0.1" proved="true">
+   <proof prover="2"><result status="valid" time="0.02"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="sum_right.1" proved="true">
+  <transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
+   <goal name="sum_right.1.0" proved="true">
+   <proof prover="1"><result status="valid" time="0.09"/></proof>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Simple" proved="true" sum="17809040d6493313e8bff554cd196ef3">
+ <goal name="WP_parameter query" expl="VC for query" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ <transf name="split_goal_wp" proved="true" >
+  <goal name="WP_parameter query.0" expl="postcondition" proved="true">
+  <proof prover="1"><result status="valid" time="0.01"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter query.1" expl="loop invariant init" proved="true">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter query.2" expl="index in array bounds" proved="true">
+  <proof prover="1"><result status="valid" time="0.01"/></proof>
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="WP_parameter query.3" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter query.4" expl="postcondition" proved="true">
+  <proof prover="1"><result status="valid" time="0.01"/></proof>
+  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="CumulativeArray" proved="true" sum="26b3e456f7b133ab67010bf9177097cd">
+ <goal name="WP_parameter create" expl="VC for create" proved="true">
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="sum_concat" proved="true">
+ <transf name="induction" proved="true" arg1="k">
+  <goal name="sum_concat.0" proved="true">
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="sum_concat.1" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter query" expl="VC for query" proved="true">
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="sum_frame" proved="true">
+ <transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
+  <goal name="sum_frame.0" proved="true">
+  <transf name="induction" proved="true" arg1="x">
+   <goal name="sum_frame.0.0" proved="true">
+   <proof prover="2"><result status="valid" time="0.01"/></proof>
+   </goal>
+   <goal name="sum_frame.0.1" proved="true">
+   <proof prover="2"><result status="valid" time="0.02"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="sum_frame.1" proved="true">
+  <transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
+   <goal name="sum_frame.1.0" proved="true">
+   <proof prover="2"><result status="valid" time="0.01"/></proof>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter sum_update" expl="VC for sum_update" proved="true">
+ <proof prover="2"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="WP_parameter update" expl="VC for update" proved="true">
+ <proof prover="1"><result status="valid" time="0.05"/></proof>
+ </goal>
+</theory>
+<theory name="CumulativeTree" sum="6ef30ae4a2b600c91ffdb138f2642e54">
+ <goal name="WP_parameter sum_concat" expl="VC for sum_concat">
+ </goal>
+ <goal name="WP_parameter tree_of_array" expl="VC for tree_of_array">
+ </goal>
+ <goal name="WP_parameter create" expl="VC for create">
+ </goal>
+ <goal name="WP_parameter query_aux" expl="VC for query_aux">
+ </goal>
+ <goal name="WP_parameter query" expl="VC for query">
+ </goal>
+ <goal name="WP_parameter query2" expl="VC for query2">
+ </goal>
+ <goal name="WP_parameter query3" expl="VC for query3">
+ </goal>
+ <goal name="WP_parameter is_tree_for_frame" expl="VC for is_tree_for_frame">
+ </goal>
+ <goal name="WP_parameter sum_right" expl="VC for sum_right">
+ </goal>
+ <goal name="WP_parameter sum_frame" expl="VC for sum_frame">
+ </goal>
+ <goal name="WP_parameter sum_update" expl="VC for sum_update">
+ </goal>
+ <goal name="WP_parameter update_aux" expl="VC for update_aux">
+ </goal>
+ <goal name="WP_parameter update" expl="VC for update">
+ </goal>
+ <goal name="WP_parameter update_compl" expl="VC for update_compl">
+ </goal>
+ <goal name="WP_parameter depth_is_log" expl="VC for depth_is_log">
+ </goal>
+</theory>
+</file>
+</why3session>