странный индекс вне диапазона В Дафни

Когда я запускаю свой код, я получаю ошибку индекса вне диапазона. Та же проблема возникает и с оператором ensures.

Мой код:

datatype CACHE_STATE = I| S| E
  datatype MSG_CMD = Empty| ReqS| ReqE| Inv| InvAck| GntS| GntE
  type NODE=nat
  type DATA=nat
type boolean=bool
class  class_0  {
var 
Data : DATA,
Cmd : MSG_CMD
}
class  class_1  {
var 
Data : DATA,
State : CACHE_STATE
}    

class TopC{
var
AuxData : DATA,
MemData : DATA,
CurPtr : NODE,
CurCmd : MSG_CMD,
ExGntd : boolean,
ShrSet : array<boolean>,
InvSet : array<boolean>,
Chan3 : array<class_0 > ,
Chan2 : array<class_0 > ,
Chan1 : array<class_0 > ,
Cache : array<class_1 > }    

method n_RecvInvAck(top:TopC,i:nat, N0:nat,p1:nat,p2:nat )
requires 0<= i<N0
requires top.Chan3.Length ==N0
 requires top.ShrSet.Length ==N0
 requires N0>0
requires 0<= p1 <top.Chan3.Length
requires 0<= p2 <top.Chan3.Length
requires p1
 requires N0>0
requires (i==p2)
requires   ((top.Chan3[i].Cmd == InvAck) && (!(top.CurCmd == Empty)))
modifies top.Chan3[i] 
modifies top.ShrSet
modifies top

ensures  (!((top.ShrSet[p1] == true) && (top.ExGntd == true) && 
  (top.ShrSet[p2] == true)))


{
  top.Chan3[i].Cmd := Empty;
  top.ShrSet[i] := false;
  if (top.ExGntd == true) {
    top.ExGntd := false;
    top.MemData := top.Chan3[i].Data;
  }
}