Verify assumptions in SCION.DecodeFromBytes

pkg/slayers/path/empty/empty_spec.gobra

@@ -34,6 +34,13 @@ func (e Path) DowngradePerm(buf []byte) {
  fold e.NonInitMem()
 }
 
+ghost
+pure
+decreases
+func (p Path) DecodeFromBytesSpec(b []byte, err error) (res bool) {
+ return true
+}
+
 Path implements path.Path
 
 // Definitions to allow *Path to be treated as a path.Path

pkg/slayers/path/epic/epic.go

@@ -138,7 +138,7 @@ func (p *Path) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 // DecodeFromBytes deserializes the buffer b into the Path. On failure, an error is returned,
 // otherwise SerializeTo will return nil.
 // @ requires p.NonInitMem()
-// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R40)
+// @ preserves acc(slices.AbsSlice_Bytes(b, 0, len(b)), R42)
 // @ ensures len(b) < MetadataLen ==> r != nil
 // @ ensures r == nil ==> p.Mem(b)
 // @ ensures r != nil ==> p.NonInitMem() && r.ErrorMem()
@@ -148,8 +148,8 @@ func (p *Path) DecodeFromBytes(b []byte) (r error) {
  return serrors.New("EPIC Path raw too short", "expected", int(MetadataLen), "actual", int(len(b)))
  }
  //@ unfold p.NonInitMem()
- //@ slices.SplitByIndex_Bytes(b, 0, len(b), PktIDLen, R40)
- //@ preserves acc(slices.AbsSlice_Bytes(b, 0, PktIDLen), R40)
+ //@ slices.SplitByIndex_Bytes(b, 0, len(b), PktIDLen, R42)
+ //@ preserves acc(slices.AbsSlice_Bytes(b, 0, PktIDLen), R42)
  //@ preserves acc(&p.PktID)
  //@ preserves acc(&p.PHVF)
  //@ preserves acc(&p.LHVF)
@@ -159,56 +159,56 @@ func (p *Path) DecodeFromBytes(b []byte) (r error) {
  //@ ensures slices.AbsSlice_Bytes(p.LHVF, 0, len(p.LHVF))
  //@ decreases
  //@ outline(
- //@ ghost slices.Reslice_Bytes(b, 0, PktIDLen, R40)
+ //@ ghost slices.Reslice_Bytes(b, 0, PktIDLen, R42)
  p.PktID.DecodeFromBytes(b[:PktIDLen])
  p.PHVF = make([]byte, HVFLen)
  p.LHVF = make([]byte, HVFLen)
  //@ fold slices.AbsSlice_Bytes(p.PHVF, 0, len(p.PHVF))
  //@ fold slices.AbsSlice_Bytes(p.LHVF, 0, len(p.LHVF))
- //@ slices.Unslice_Bytes(b, 0, PktIDLen, R40)
+ //@ slices.Unslice_Bytes(b, 0, PktIDLen, R42)
  //@ )
- //@ slices.SplitByIndex_Bytes(b, PktIDLen, len(b), PktIDLen+HVFLen, R40)
+ //@ slices.SplitByIndex_Bytes(b, PktIDLen, len(b), PktIDLen+HVFLen, R42)
  //@ preserves acc(&p.PHVF)
  //@ preserves slices.AbsSlice_Bytes(p.PHVF, 0, len(p.PHVF))
- //@ preserves acc(slices.AbsSlice_Bytes(b, PktIDLen, PktIDLen + HVFLen), R40)
+ //@ preserves acc(slices.AbsSlice_Bytes(b, PktIDLen, PktIDLen + HVFLen), R42)
  //@ decreases
  //@ outline(
- //@ slices.Reslice_Bytes(b, PktIDLen, PktIDLen+HVFLen, R40)
+ //@ slices.Reslice_Bytes(b, PktIDLen, PktIDLen+HVFLen, R42)
  //@ unfold slices.AbsSlice_Bytes(p.PHVF, 0, len(p.PHVF))
- //@ unfold acc(slices.AbsSlice_Bytes(b[PktIDLen:(PktIDLen+HVFLen)], 0, HVFLen), R41)
- copy(p.PHVF, b[PktIDLen:(PktIDLen+HVFLen)] /*@, R41 @*/)
- //@ fold acc(slices.AbsSlice_Bytes(b[PktIDLen:(PktIDLen+HVFLen)], 0, HVFLen), R41)
+ //@ unfold acc(slices.AbsSlice_Bytes(b[PktIDLen:(PktIDLen+HVFLen)], 0, HVFLen), R42)
+ copy(p.PHVF, b[PktIDLen:(PktIDLen+HVFLen)] /*@, R42 @*/)
+ //@ fold acc(slices.AbsSlice_Bytes(b[PktIDLen:(PktIDLen+HVFLen)], 0, HVFLen), R42)
  //@ fold slices.AbsSlice_Bytes(p.PHVF, 0, len(p.PHVF))
- //@ slices.Unslice_Bytes(b, PktIDLen, PktIDLen+HVFLen, R40)
+ //@ slices.Unslice_Bytes(b, PktIDLen, PktIDLen+HVFLen, R42)
  //@ )
- //@ slices.CombineAtIndex_Bytes(b, 0, PktIDLen+HVFLen, PktIDLen, R40)
- //@ slices.SplitByIndex_Bytes(b, PktIDLen+HVFLen, len(b), MetadataLen, R40)
+ //@ slices.CombineAtIndex_Bytes(b, 0, PktIDLen+HVFLen, PktIDLen, R42)
+ //@ slices.SplitByIndex_Bytes(b, PktIDLen+HVFLen, len(b), MetadataLen, R42)
  //@ preserves acc(&p.LHVF)
  //@ preserves slices.AbsSlice_Bytes(p.LHVF, 0, len(p.LHVF))
- //@ preserves acc(slices.AbsSlice_Bytes(b, PktIDLen+HVFLen, MetadataLen), R40)
+ //@ preserves acc(slices.AbsSlice_Bytes(b, PktIDLen+HVFLen, MetadataLen), R42)
  //@ decreases
  //@ outline(
- //@ slices.Reslice_Bytes(b, PktIDLen+HVFLen, MetadataLen, R40)
+ //@ slices.Reslice_Bytes(b, PktIDLen+HVFLen, MetadataLen, R42)
  //@ unfold slices.AbsSlice_Bytes(p.LHVF, 0, len(p.LHVF))
- //@ unfold acc(slices.AbsSlice_Bytes(b[PktIDLen+HVFLen:MetadataLen], 0, HVFLen), R41)
- copy(p.LHVF, b[(PktIDLen+HVFLen):MetadataLen] /*@, R41 @*/)
- //@ fold acc(slices.AbsSlice_Bytes(b[PktIDLen+HVFLen:MetadataLen], 0, HVFLen), R41)
+ //@ unfold acc(slices.AbsSlice_Bytes(b[PktIDLen+HVFLen:MetadataLen], 0, HVFLen), R42)
+ copy(p.LHVF, b[(PktIDLen+HVFLen):MetadataLen] /*@, R42 @*/)
+ //@ fold acc(slices.AbsSlice_Bytes(b[PktIDLen+HVFLen:MetadataLen], 0, HVFLen), R42)
  //@ fold slices.AbsSlice_Bytes(p.LHVF, 0, len(p.LHVF))
- //@ slices.Unslice_Bytes(b, PktIDLen+HVFLen, MetadataLen, R40)
+ //@ slices.Unslice_Bytes(b, PktIDLen+HVFLen, MetadataLen, R42)
  //@ )
- //@ slices.CombineAtIndex_Bytes(b, 0, MetadataLen, PktIDLen+HVFLen, R40)
+ //@ slices.CombineAtIndex_Bytes(b, 0, MetadataLen, PktIDLen+HVFLen, R42)
  p.ScionPath = &scion.Raw{}
  //@ fold p.ScionPath.Base.NonInitMem()
  //@ fold p.ScionPath.NonInitMem()
- //@ slices.Reslice_Bytes(b, MetadataLen, len(b), R40)
+ //@ slices.Reslice_Bytes(b, MetadataLen, len(b), R42)
  ret := p.ScionPath.DecodeFromBytes(b[MetadataLen:])
  //@ ghost if ret == nil {
  //@ fold p.Mem(b)
  //@ } else {
  //@ fold p.NonInitMem()
  //@ }
- //@ slices.Unslice_Bytes(b, MetadataLen, len(b), R40)
- //@ slices.CombineAtIndex_Bytes(b, 0, len(b), MetadataLen, R40)
+ //@ slices.Unslice_Bytes(b, MetadataLen, len(b), R42)
+ //@ slices.CombineAtIndex_Bytes(b, 0, len(b), MetadataLen, R42)
  return ret
 }
 
@@ -278,17 +278,17 @@ type PktID struct {
 // DecodeFromBytes deserializes the buffer (raw) into the PktID.
 // @ requires len(raw) >= PktIDLen
 // @ preserves acc(i)
-// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R41)
+// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R42)
 // @ ensures 0 <= i.Timestamp
 // @ ensures 0 <= i.Counter
 // @ decreases
 func (i *PktID) DecodeFromBytes(raw []byte) {
- //@ unfold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R41)
+ //@ unfold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R42)
  //@ assert forall i int :: { &raw[:4][i] } 0 <= i && i < 4 ==> &raw[:4][i] == &raw[i]
  i.Timestamp = binary.BigEndian.Uint32(raw[:4])
  //@ assert forall i int :: { &raw[4:8][i] } 0 <= i && i < 4 ==> &raw[4:8][i] == &raw[4 + i]
  i.Counter = binary.BigEndian.Uint32(raw[4:8])
- //@ fold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R41)
+ //@ fold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R42)
 }
 
 // SerializeTo serializes the PktID into the buffer (b).

pkg/slayers/path/epic/epic_spec.gobra

@@ -105,4 +105,11 @@ pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
  return unfolding acc(p.Mem(buf), _) in buf[MetadataLen:]
 }
 
+ghost
+pure
+decreases
+func (p *Path) DecodeFromBytesSpec(b []byte, err error) (res bool) {
+ return true
+}
+
 (*Path) implements path.Path

pkg/slayers/path/hopfield.go

@@ -79,17 +79,13 @@ type HopField struct {
 // @ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R45)
 // @ ensures h.Mem()
 // @ ensures err == nil
+// @ ensures unfolding h.Mem() in
+// @ BytesToIO_HF(raw, 0, 0, HopLen) == h.ToIO_HF()
 // @ decreases
 func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
  if len(raw) < HopLen {
  return serrors.New("HopField raw too short", "expected", HopLen, "actual", len(raw))
  }
- //@ preserves acc(h)
- //@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
- //@ ensures h.ConsIngress >= 0
- //@ ensures h.ConsEgress >= 0
- //@ decreases
- //@ outline(
  //@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
  h.EgressRouterAlert = raw[0]&0x1 == 0x1
  h.IngressRouterAlert = raw[0]&0x2 == 0x2
@@ -98,20 +94,16 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
  h.ConsIngress = binary.BigEndian.Uint16(raw[2:4])
  //@ assert &raw[4:6][0] == &raw[4] && &raw[4:6][1] == &raw[5]
  h.ConsEgress = binary.BigEndian.Uint16(raw[4:6])
- //@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
- //@ )
- //@ preserves acc(&h.Mac)
- //@ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
- //@ decreases
- //@ outline(
- //@ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
  //@ assert forall i int :: { &h.Mac[:][i] } 0 <= i && i < len(h.Mac[:]) ==>
  //@ &h.Mac[i] == &h.Mac[:][i]
  //@ assert forall i int :: { &raw[6:6+MacLen][i] } 0 <= i && i < len(raw[6:6+MacLen]) ==>
  //@ &raw[6:6+MacLen][i] == &raw[i+6]
  copy(h.Mac[:], raw[6:6+MacLen] /*@ , R47 @*/)
+ //@ assert forall i int :: {&h.Mac[:][i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == raw[6:6+MacLen][i]
+ //@ assert forall i int :: {&h.Mac[i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == h.Mac[i]
+ //@ AbsMac_Lemma(raw[6:6+MacLen], h.Mac)
+ //@ assert BytesToIO_HF(raw, 0, 0, HopLen) == h.ToIO_HF()
  //@ fold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46)
- //@ )
  //@ fold h.Mem()
  return nil
 }

pkg/slayers/path/infofield.go

@@ -64,6 +64,8 @@ type InfoField struct {
 // @ preserves acc(inf)
 // @ preserves acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R45)
 // @ ensures err == nil
+// @ ensures BytesToIntermediateAbsInfoField(raw, 0, 0, InfoLen) ==
+// @ inf.ToIntermediateAbsInfoField()
 // @ decreases
 func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
  if len(raw) < InfoLen {

pkg/slayers/path/infofield_spec.gobra

@@ -103,8 +103,10 @@ requires forall i int :: { &raw[i] } middle <= i && i < end ==>
  acc(&raw[i], _)
 decreases
 pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int) (IntermediateAbsInfoField) {
- return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
- let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
+ return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==>
+ &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
+ let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==>
+ &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
  IntermediateAbsInfoField(IntermediateAbsInfoField_{
  AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
  UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),

pkg/slayers/path/io_msgterm_spec.gobra

@@ -16,7 +16,10 @@
 
 package path
 
-import "verification/io"
+import (
+ "verification/io"
+ . "github.com/scionproto/scion/verification/utils/definitions"
+)
 
 // At the moment, we assume that all cryptographic operations performed at the code level
 // imply the desired properties at the IO spec level because we cannot currently prove in
@@ -28,8 +31,22 @@ decreases
 pure func AbsUInfoFromUint16(SegID uint16) set[io.IO_msgterm]
 
 ghost
+ensures len(res) == MacLen
+ensures forall i int :: { mac[i] } 0 <= i && i < MacLen ==> res[i] == mac[i]
 decreases
-pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm)
+pure func macSequence(mac [MacLen]byte) (res seq[byte])
+
+ghost
+requires len(mac) == MacLen
+decreases
+pure func absMac_Internal(mac seq[byte]) (io.IO_msgterm)
+
+ghost
+opaque
+decreases
+pure func AbsMac(mac [MacLen]byte) (io.IO_msgterm) {
+ return absMac_Internal(macSequence(mac))
+}
 
 // The following function converts a slice with at least `MacLen` elements into
 // an (exclusive) array containing the mac. Note that there are no permissions
@@ -44,3 +61,24 @@ ensures len(res) == MacLen
 ensures forall i int :: { res[i] } 0 <= i && i < MacLen ==> mac[i] == res[i]
 decreases
 pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte)
+
+
+ghost
+requires len(mac1) == MacLen
+requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50)
+requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> mac1[i] == mac2[i]
+ensures forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50)
+ensures AbsMac(FromSliceToMacArray(mac1)) == AbsMac(mac2)
+decreases
+func AbsMac_Lemma(mac1 []byte, mac2 [MacLen]byte) {
+ mac1a := FromSliceToMacArray(mac1)
+ assert forall i int :: { mac2[i] } 0 <= i && i < MacLen ==> mac1a[i] == mac2[i]
+ assert len(mac1a) == len(mac2)
+ assert len(mac1a) == 6
+ mac1s := macSequence(mac1a)
+ mac2s := macSequence(mac2)
+ assert forall i int :: { mac1s[i] } 0 <= i && i < MacLen ==> mac1s[i] == mac1a[i]
+ assert forall i int :: { mac1s[i] } 0 <= i && i < MacLen ==> mac2s[i] == mac2[i]
+ assert macSequence(FromSliceToMacArray(mac1)) == macSequence(mac2)
+ assert reveal AbsMac(FromSliceToMacArray(mac1)) == reveal AbsMac(mac2)
+}

pkg/slayers/path/onehop/onehop.go

@@ -66,7 +66,7 @@ type Path struct {
 }
 
 // @ requires o.NonInitMem()
-// @ preserves acc(slices.AbsSlice_Bytes(data, 0, len(data)), R40)
+// @ preserves acc(slices.AbsSlice_Bytes(data, 0, len(data)), R42)
 // @ ensures (len(data) >= PathLen) == (r == nil)
 // @ ensures r == nil ==> o.Mem(data)
 // @ ensures r != nil ==> o.NonInitMem()
@@ -79,29 +79,29 @@ func (o *Path) DecodeFromBytes(data []byte) (r error) {
  }
  offset := 0
  //@ unfold o.NonInitMem()
- //@ slices.SplitByIndex_Bytes(data, 0, len(data), path.InfoLen, R41)
- //@ slices.Reslice_Bytes(data, 0, path.InfoLen, R41)
+ //@ slices.SplitByIndex_Bytes(data, 0, len(data), path.InfoLen, R42)
+ //@ slices.Reslice_Bytes(data, 0, path.InfoLen, R42)
  if err := o.Info.DecodeFromBytes(data[:path.InfoLen]); err != nil {
  // @ Unreachable()
  return err
  }
- //@ slices.Unslice_Bytes(data, 0, path.InfoLen, R41)
+ //@ slices.Unslice_Bytes(data, 0, path.InfoLen, R42)
  offset += path.InfoLen
- //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset+path.HopLen, R41)
- //@ slices.Reslice_Bytes(data, offset, offset+path.HopLen, R41)
+ //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset+path.HopLen, R42)
+ //@ slices.Reslice_Bytes(data, offset, offset+path.HopLen, R42)
  if err := o.FirstHop.DecodeFromBytes(data[offset : offset+path.HopLen]); err != nil {
  // @ Unreachable()
  return err
  }
- //@ slices.Unslice_Bytes(data, offset, offset+path.HopLen, R41)
- //@ slices.CombineAtIndex_Bytes(data, 0, offset+path.HopLen, offset, R41)
+ //@ slices.Unslice_Bytes(data, offset, offset+path.HopLen, R42)
+ //@ slices.CombineAtIndex_Bytes(data, 0, offset+path.HopLen, offset, R42)
  offset += path.HopLen
- //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset+path.HopLen, R41)
- //@ slices.Reslice_Bytes(data, offset, offset+path.HopLen, R41)
+ //@ slices.SplitByIndex_Bytes(data, offset, len(data), offset+path.HopLen, R42)
+ //@ slices.Reslice_Bytes(data, offset, offset+path.HopLen, R42)
  r = o.SecondHop.DecodeFromBytes(data[offset : offset+path.HopLen])
- //@ slices.Unslice_Bytes(data, offset, offset+path.HopLen, R41)
- //@ slices.CombineAtIndex_Bytes(data, offset, len(data), offset+path.HopLen, R41)
- //@ slices.CombineAtIndex_Bytes(data, 0, len(data), offset, R41)
+ //@ slices.Unslice_Bytes(data, offset, offset+path.HopLen, R42)
+ //@ slices.CombineAtIndex_Bytes(data, offset, len(data), offset+path.HopLen, R42)
+ //@ slices.CombineAtIndex_Bytes(data, 0, len(data), offset, R42)
  //@ ghost if r == nil { fold o.Mem(data) } else { fold o.NonInitMem() }
  return r
 }

pkg/slayers/path/onehop/onehop_spec.gobra

@@ -51,4 +51,11 @@ pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
  return unfolding acc(o.Mem(ub), _) in o.Len(ub) <= len(ub)
 }
 
+ghost
+pure
+decreases
+func (p *Path) DecodeFromBytesSpec(b []byte, err error) (res bool) {
+ return true
+}
+
 (*Path) implements path.Path

pkg/slayers/path/path.go

@@ -81,12 +81,19 @@ type Path interface {
  // (VerifiedSCION) There are implementations of this interface (e.g., scion.Raw) that
  // store b and use it as internal data.
  //@ requires NonInitMem()
- //@ preserves acc(sl.AbsSlice_Bytes(b, 0, len(b)), R40)
+ //@ preserves acc(sl.AbsSlice_Bytes(b, 0, len(b)), R42)
  //@ ensures err == nil ==> Mem(b)
  //@ ensures err != nil ==> err.ErrorMem()
  //@ ensures err != nil ==> NonInitMem()
+ //@ ensures err == nil ==> DecodeFromBytesSpec(b, err)
  //@ decreases
  DecodeFromBytes(b []byte) (err error)
+ //@ ghost
+ //@ pure
+ //@ requires Mem(b)
+ //@ requires acc(sl.AbsSlice_Bytes(b, 0, len(b)), R42)
+ //@ decreases
+ //@ DecodeFromBytesSpec(b []byte, err error) (res bool)
  // Reverse reverses a path such that it can be used in the reversed direction.
  // XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
  //@ requires Mem(underlyingBuf)
@@ -219,7 +226,7 @@ func (p *rawPath) SerializeTo(b []byte /*@, ghost underlyingBuf []byte @*/) (e e
 }
 
 // @ requires p.NonInitMem()
-// @ preserves acc(sl.AbsSlice_Bytes(b, 0, len(b)), R40)
+// @ preserves acc(sl.AbsSlice_Bytes(b, 0, len(b)), R42)
 // @ ensures p.Mem(b)
 // @ ensures e == nil
 // @ decreases

pkg/slayers/path/path_spec.gobra

@@ -16,7 +16,9 @@
 
 package path
 
-import "github.com/scionproto/scion/verification/utils/slices"
+import "github.com/scionproto/scion/verification/utils/slices"
+
+
 
 /** rawPath spec **/
 pred (r *rawPath) Mem(underlyingBuf []byte) {
@@ -37,6 +39,13 @@ func (p *rawPath) DowngradePerm(ghost buf []byte) {
  fold p.NonInitMem()
 }
 
+ghost
+pure
+decreases
+func (p *rawPath) DecodeFromBytesSpec(b []byte, err error) (res bool) {
+ return true
+}
+
 (*rawPath) implements Path
 
 /** End of rawPath spec **/