Inductive proofs in Dafny #4132

rahxephon89 · 2023-06-04T19:27:00Z

rahxephon89
Jun 4, 2023

Hi, I am trying to understand how Dafny proves inductive properties by using the following code example:

function sum(v: seq<int>): int 
 {
     if (|v| == 0) then 0 
     else v[|v|-1] + sum(v[..(|v|-1)])
 }

datatype R = R(v: seq<int>, total: int)

method add(r: R, x: int) returns (new_r : R)
requires r.total == sum(r.v)
ensures new_r.total == sum(new_r.v)
{
    new_r := R(r.v + [x], r.total + x);
   
}

This is the boogie code generated by Dafny, which has been minimized manually.

// dafny 4.1.0.0

type Ty;
const unique TInt: Ty;
function TSeq(Ty) : Ty;
type Box;

axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

function $Box<T>(T) : Box;
function $Unbox<T>(Box) : T;
function $IsBox<T>(T, Ty) : bool;

axiom (forall<T> v: T, t: Ty ::
  { $IsBox($Box(v), t) }
  $IsBox($Box(v), t) <==> $Is(v, t));

axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt));

axiom (forall v: Seq Box, t0: Ty ::
  { $Is(v, TSeq(t0)) }
  $Is(v, TSeq(t0))
     <==> (forall i: int ::
      { Seq#Index(v, i) }
      0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));

function $Is<T>(T, Ty) : bool;

type DatatypeType;
const $FunctionContextHeight: int;

type LayerType;
const $LZ: LayerType;
function $LS(LayerType) : LayerType;

type Seq _;
function Seq#Length<T>(Seq T) : int;

axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

function Seq#Empty<T>() : Seq T;

axiom (forall<T>  :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0);

function Seq#Build<T>(s: Seq T, val: T) : Seq T;

axiom (forall<T> s: Seq T, v: T ::
  { Seq#Build(s, v) }
  Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));

axiom (forall<T> s: Seq T, i: int, v: T ::
  { Seq#Index(Seq#Build(s, v), i) }
  (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v)
     && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));

function Seq#Append<T>(Seq T, Seq T) : Seq T;

axiom (forall<T> s0: Seq T, s1: Seq T ::
  { Seq#Length(Seq#Append(s0, s1)) }
  Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));

function Seq#Index<T>(Seq T, int) : T;

axiom (forall<T> s0: Seq T, s1: Seq T, n: int ::
  { Seq#Index(Seq#Append(s0, s1), n) }
  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n))
     && (Seq#Length(s0) <= n
       ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));

function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;
function Seq#Drop<T>(s: Seq T, howMany: int) : Seq T;

axiom (forall<T> s: Seq T, t: Seq T, n: int ::
  { Seq#Take(Seq#Append(s, t), n) } { Seq#Drop(Seq#Append(s, t), n) }
  n == Seq#Length(s)
     ==> Seq#Take(Seq#Append(s, t), n) == s && Seq#Drop(Seq#Append(s, t), n) == t);

// Constructor function declaration
function #_module.R.R(Seq Box, int) : DatatypeType;

function _module.R.R_q(DatatypeType) : bool;

// Constructor questionmark has arguments
axiom (forall d: DatatypeType ::
  { _module.R.R_q(d) }
  _module.R.R_q(d)
     ==> (exists a#13#0#0: Seq Box, a#13#1#0: int ::
      d == #_module.R.R(a#13#0#0, a#13#1#0)));

function Tclass._module.R() : Ty;

// Constructor $Is
axiom (forall a#14#0#0: Seq Box, a#14#1#0: int ::
  { $Is(#_module.R.R(a#14#0#0, a#14#1#0), Tclass._module.R()) }
  $Is(#_module.R.R(a#14#0#0, a#14#1#0), Tclass._module.R())
     <==> $Is(a#14#0#0, TSeq(TInt)) && $Is(a#14#1#0, TInt));

function _module.R.v(DatatypeType) : Seq Box;

// Constructor injectivity
axiom (forall a#16#0#0: Seq Box, a#16#1#0: int ::
  { #_module.R.R(a#16#0#0, a#16#1#0) }
  _module.R.v(#_module.R.R(a#16#0#0, a#16#1#0)) == a#16#0#0);

function _module.R.total(DatatypeType) : int;

// Constructor injectivity
axiom (forall a#19#0#0: Seq Box, a#19#1#0: int ::
  { #_module.R.R(a#19#0#0, a#19#1#0) }
  _module.R.total(#_module.R.R(a#19#0#0, a#19#1#0)) == a#19#1#0);

// function declaration for _module._default.sum
function _module.__default.sum($ly: LayerType, v#0: Seq Box) : int;

// layer synonym axiom
axiom (forall $ly: LayerType, v#0: Seq Box ::
  { _module.__default.sum($LS($ly), v#0) }
  _module.__default.sum($LS($ly), v#0) == _module.__default.sum($ly, v#0));

// definition axiom for _module.__default.sum (revealed)
axiom 0 <= $FunctionContextHeight
   ==> (forall $ly: LayerType, v#0: Seq Box ::
    { _module.__default.sum($LS($ly), v#0) }
       (0 < $FunctionContextHeight && $Is(v#0, TSeq(TInt)))
       ==>  _module.__default.sum($LS($ly), v#0)
           == (if Seq#Length(v#0) == 0
             then 0
             else $Unbox(Seq#Index(v#0, Seq#Length(v#0) - 1)): int
               + _module.__default.sum($ly, Seq#Take(v#0, Seq#Length(v#0) - 1))));

procedure {:verboseName "add (correctness)"} Impl$$_module.__default.add(r#0: DatatypeType
       where $Is(r#0, Tclass._module.R())
         ,
    x#0: int)
   returns (new_r#0: DatatypeType
       where $Is(new_r#0, Tclass._module.R()));
  free requires 1 == $FunctionContextHeight;
  // user-defined preconditions
  requires _module.R.total(r#0) == _module.__default.sum($LS($LS($LZ)), _module.R.v(r#0));
  // user-defined postconditions
  ensures _module.R.total(new_r#0)
     == _module.__default.sum($LS($LS($LZ)), _module.R.v(new_r#0));

implementation {:verboseName "add (correctness)"} Impl$$_module.__default.add(r#0: DatatypeType, x#0: int)
   returns (new_r#0: DatatypeType)
{
    // AddMethodImpl: add, Impl$$_module.__default.add
    assume _module.R.R_q(r#0);
    new_r#0 := #_module.R.R(Seq#Append(_module.R.v(r#0), Seq#Build(Seq#Empty(): Seq Box, $Box(x#0))),
      _module.R.total(r#0) + x#0);
}

I understand the meaning of most definitions and axioms in the code above but could not figure out how the SMT solver can prove it, especially the use of LayerType. Could anyone give some hints on the mechanism at the backend ? Thanks

Answered by atomb

Jun 5, 2023

I think that this paper could be a helpful resource in understanding how LayerType works.

View full answer

atomb · 2023-06-05T15:53:14Z

atomb
Jun 5, 2023
Maintainer

I think that this paper could be a helpful resource in understanding how LayerType works.

3 replies

rahxephon89 Jun 5, 2023
Author

Thanks, Aaron! I will read it. I just found out that after removing existence of LayerType, the following code can also verify. I am wondering why it is the case though.

// Command Line Options: -print:test.bpl test.dfy

type Ty;

const unique TInt: Ty;

function TSeq(Ty) : Ty;

type Box;

axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

function $Box<T>(T) : Box;

function $Unbox<T>(Box) : T;

function $IsBox<T>(T, Ty) : bool;

axiom (forall<T> v: T, t: Ty ::
  $IsBox($Box(v), t) <==> $Is(v, t));

axiom (forall v: int :: //{ $Is(v, TInt) } 
$Is(v, TInt));

axiom (forall v: Seq Box, t0: Ty ::
  $Is(v, TSeq(t0))
     <==> (forall i: int ::
      0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));

function $Is<T>(T, Ty) : bool;

type DatatypeType;

const $FunctionContextHeight: int;


type Seq _;

function Seq#Length<T>(Seq T) : int;

axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

function Seq#Empty<T>() : Seq T;

axiom (forall<T>  :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0);

function Seq#Build<T>(s: Seq T, val: T) : Seq T;

axiom (forall<T> s: Seq T, v: T ::
  Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));

axiom (forall<T> s: Seq T, i: int, v: T ::
  (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v)
     && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));

function Seq#Append<T>(Seq T, Seq T) : Seq T;

axiom (forall<T> s0: Seq T, s1: Seq T ::
  Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));

function Seq#Index<T>(Seq T, int) : T;

axiom (forall<T> s0: Seq T, s1: Seq T, n: int ::
  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n))
     && (Seq#Length(s0) <= n
       ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));

function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;

axiom (forall<T> s: Seq T, t: Seq T, n: int ::
  n == Seq#Length(s)
     ==> Seq#Take(Seq#Append(s, t), n) == s); //&& Seq#Drop(Seq#Append(s, t), n) == t);

// Constructor function declaration
function #_module.R.R(Seq Box, int) : DatatypeType;

function _module.R.R_q(DatatypeType) : bool;

// Constructor questionmark has arguments
axiom (forall d: DatatypeType ::
  //{ _module.R.R_q(d) }
  _module.R.R_q(d)
     ==> (exists a#13#0#0: Seq Box, a#13#1#0: int ::
      d == #_module.R.R(a#13#0#0, a#13#1#0)));

function Tclass._module.R() : Ty;

// Constructor $Is
axiom (forall a#14#0#0: Seq Box, a#14#1#0: int ::
  $Is(#_module.R.R(a#14#0#0, a#14#1#0), Tclass._module.R())
     <==> $Is(a#14#0#0, TSeq(TInt)) && $Is(a#14#1#0, TInt));

function _module.R.v(DatatypeType) : Seq Box;

// Constructor injectivity
axiom (forall a#16#0#0: Seq Box, a#16#1#0: int ::
  _module.R.v(#_module.R.R(a#16#0#0, a#16#1#0)) == a#16#0#0);

function _module.R.total(DatatypeType) : int;

// Constructor injectivity
axiom (forall a#19#0#0: Seq Box, a#19#1#0: int ::
  _module.R.total(#_module.R.R(a#19#0#0, a#19#1#0)) == a#19#1#0);

// function declaration for _module._default.sum
function _module.__default.sum(v#0: Seq Box) : int;

// definition axiom for _module.__default.sum (revealed)
axiom(forall v#0: Seq Box ::
        _module.__default.sum(v#0)
           == (if Seq#Length(v#0) == 0
             then 0
             else $Unbox(Seq#Index(v#0, Seq#Length(v#0) - 1)): int
               + _module.__default.sum(Seq#Take(v#0, Seq#Length(v#0) - 1))));


procedure {:verboseName "add (correctness)"} Impl$$_module.__default.add(r#0: DatatypeType
       where $Is(r#0, Tclass._module.R())
         ,
    x#0: int)
   returns (new_r#0: DatatypeType
       where $Is(new_r#0, Tclass._module.R()));
  // user-defined preconditions
  requires _module.R.total(r#0) == _module.__default.sum(_module.R.v(r#0));
  // user-defined postconditions
  ensures _module.R.total(new_r#0)
     == _module.__default.sum(_module.R.v(new_r#0));

implementation {:verboseName "add (correctness)"} Impl$$_module.__default.add(r#0: DatatypeType, x#0: int)
   returns (new_r#0: DatatypeType)
{
    // AddMethodImpl: add, Impl$$_module.__default.add
    assume _module.R.R_q(r#0);
    new_r#0 := #_module.R.R(Seq#Append(_module.R.v(r#0), Seq#Build(Seq#Empty(): Seq Box, $Box(x#0))),
      _module.R.total(r#0) + x#0);
}

atomb Jun 5, 2023
Maintainer

In this case, one application of the definition axiom for sum is sufficient to prove the goal. Explicit inductive reasoning isn't required.

rahxephon89 Jun 6, 2023
Author

Thanks!

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Inductive proofs in Dafny #4132

{{title}}

Replies: 1 comment 3 replies

{{title}}

{{title}}

{{title}}

{{title}}

Select a reply

Inductive proofs in Dafny #4132

rahxephon89 Jun 4, 2023

Replies: 1 comment · 3 replies

atomb Jun 5, 2023 Maintainer

rahxephon89 Jun 5, 2023 Author

atomb Jun 5, 2023 Maintainer

rahxephon89 Jun 6, 2023 Author

rahxephon89
Jun 4, 2023

Replies: 1 comment 3 replies

atomb
Jun 5, 2023
Maintainer

rahxephon89 Jun 5, 2023
Author

atomb Jun 5, 2023
Maintainer

rahxephon89 Jun 6, 2023
Author