Skip to content

Commit b5bc28c

Browse files
jcp19jcp19
authored
Adapt spec according to PR 944 from Gobra (#405)
* adapt according to PR 944 from Gobra * fix parsing issues with slayers * fix remaining parsing errors * fix missing parsing error
1 parent e32dd2e commit b5bc28c

17 files changed

+168
-172
lines changed

‎pkg/slayers/scion.go‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -780,9 +780,9 @@ func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType
780780
switch a := hostAddr.(type) {
781781
case *net.IPAddr:
782782
// @ ghost if wildcard {
783-
// @ unfold acc(hostAddr.Mem(), _)
783+
// @ unfold acc(hostAddr.Mem(), _)
784784
// @ } else {
785-
// @ unfold acc(hostAddr.Mem(), R20)
785+
// @ unfold acc(hostAddr.Mem(), R20)
786786
// @ }
787787
if ip := a.IP.To4( /*@ wildcard @*/ ); ip != nil {
788788
// @ ghost if !wildcard && isIPv6(a) {
@@ -805,13 +805,13 @@ func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType
805805
// @ assert !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (isIPv6(hostAddr) && isConvertibleToIPv4(hostAddr) ==> forall i int :: { &b[i] } 0 <= i && i < len(b) ==> &b[i] == &hostAddr.(*net.IPAddr).IP[12+i]))
806806
verScionTmp := a.IP
807807
// @ ghost if wildcard {
808-
// @ fold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), _)
808+
// @ fold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), _)
809809
// @ } else {
810-
// @ fold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20)
811-
// @ package acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(hostAddr.Mem(), R20) {
812-
// @ unfold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20)
813-
// @ fold acc(hostAddr.Mem(), R20)
814-
// @ }
810+
// @ fold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20)
811+
// @ package acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(hostAddr.Mem(), R20) {
812+
// @ unfold acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20)
813+
// @ fold acc(hostAddr.Mem(), R20)
814+
// @ }
815815
// @ }
816816
return T16Ip, verScionTmp, nil
817817
case addr.HostSVC:

‎pkg/slayers/scion_spec.gobra‎

Lines changed: 24 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -409,20 +409,22 @@ requires sl.Bytes(ub, 0, len(ub))
409409
decreases
410410
pure func (s *SCION) EqAbsHeader(ub []byte) bool {
411411
return unfolding s.Mem(ub) in
412-
let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
413-
let high := s.HdrLen*LineLen in
414-
GetAddressOffset(ub) == low &&
415-
GetLength(ub) == int(high) &&
412+
// the '_' in the identifier below is now necessary to avoid
413+
// parsing errors (since the SIF PR in Gobra, low is a keyword).
414+
let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in
415+
let high := s.HdrLen*LineLen in
416+
GetAddressOffset(ub) == low_ &&
417+
GetLength(ub) == int(high) &&
416418
// Might be worth introducing EqAbsHeader as an interface method on Path
417419
// to avoid doing these casts, especially when we add support for EPIC.
418420
typeOf(s.Path) == (*scion.Raw) &&
419-
unfolding s.Path.Mem(ub[low:high]) in
420-
unfolding sl.Bytes(ub, 0, len(ub)) in
421-
let _ := Asserting(forall k int :: {&ub[low:high][k]} 0 <= k && k < high ==>
422-
&ub[low:high][k] == &ub[low + k]) in
423-
let _ := Asserting(forall k int :: {&ub[low:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==>
424-
&ub[low:high][:scion.MetaLen][k] == &ub[low:high][k]) in
425-
let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low:high][:scion.MetaLen])) in
421+
unfolding s.Path.Mem(ub[low_:high]) in
422+
unfolding sl.Bytes(ub, 0, len(ub)) in
423+
let _ := Asserting(forall k int :: {&ub[low_:high][k]} 0 <= k && k < high ==>
424+
&ub[low_:high][k] == &ub[low_ + k]) in
425+
let _ := Asserting(forall k int :: {&ub[low_:high][:scion.MetaLen][k]} 0 <= k && k < scion.MetaLen ==>
426+
&ub[low_:high][:scion.MetaLen][k] == &ub[low_:high][k]) in
427+
let metaHdr := scion.DecodedFrom(binary.BigEndian.Uint32(ub[low_:high][:scion.MetaLen])) in
426428
let seg1 := int(metaHdr.SegLen[0]) in
427429
let seg2 := int(metaHdr.SegLen[1]) in
428430
let seg3 := int(metaHdr.SegLen[2]) in
@@ -437,11 +439,13 @@ opaque
437439
requires s.Mem(ub)
438440
decreases
439441
pure func (s *SCION) ValidScionInitSpec(ub []byte) bool {
440-
return unfolding s.Mem(ub) in
441-
let low := CmnHdrLen+s.AddrHdrLenSpecInternal() in
442-
let high := s.HdrLen*LineLen in
442+
return unfolding s.Mem(ub) in
443+
// the '_' in the identifier below is now necessary to avoid
444+
// parsing errors (since the SIF PR in Gobra, low is a keyword).
445+
let low_ := CmnHdrLen+s.AddrHdrLenSpecInternal() in
446+
let high := s.HdrLen*LineLen in
443447
typeOf(s.Path) == (*scion.Raw) &&
444-
s.Path.(*scion.Raw).GetBase(ub[low:high]).WeaklyValid()
448+
s.Path.(*scion.Raw).GetBase(ub[low_:high]).WeaklyValid()
445449
}
446450

447451
// Checks if the common path header is valid in the serialized scion packet.
@@ -604,11 +608,11 @@ requires s.Mem(ub)
604608
decreases
605609
pure func (s *SCION) GetScionPath(ub []byte) path.Path {
606610
return unfolding s.Mem(ub) in (
607-
typeOf(s.Path) == *epic.Path ?
608-
(let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
609-
unfolding s.Path.Mem(ubPath) in
610-
(path.Path)(s.Path.(*epic.Path).ScionPath)) :
611-
s.Path)
611+
typeOf(s.Path) == *epic.Path ?
612+
(let ubPath := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
613+
unfolding s.Path.Mem(ubPath) in
614+
(path.Path)(s.Path.(*epic.Path).ScionPath)) :
615+
s.Path)
612616
}
613617

614618
ghost

‎pkg/slayers/scmp_typecode_spec.gobra‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,14 @@ package slayers
1818

1919
pred SCMPTypeCodeMem() {
2020
// We don't use a trigger here since triggers of the form scmpTypeCodeInfo[i].codes would generate a ternary expression
21-
// The default trigger generated is: { (i_V0 in domain((getMap(scmpTypeCodeInfo_e8d3837_G().underlyingMapField): Map[Int,Tuple2[Int, Ref]]))) }
21+
// The default trigger generated is: { (i_V0 elem domain((getMap(scmpTypeCodeInfo_e8d3837_G().underlyingMapField): Map[Int,Tuple2[Int, Ref]]))) }
2222
acc(scmpTypeCodeInfo) &&
23-
forall i SCMPType :: { scmpTypeCodeInfo[i] } i in domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes)
23+
forall i SCMPType :: { scmpTypeCodeInfo[i] } i elem domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes)
2424
}
2525

2626
mayInit
2727
requires acc(scmpTypeCodeInfo)
28-
requires forall i SCMPType :: { scmpTypeCodeInfo[i] } i in domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes)
28+
requires forall i SCMPType :: { scmpTypeCodeInfo[i] } i elem domain(scmpTypeCodeInfo) ==> scmpTypeCodeInfo[i].codes != nil ==> acc(scmpTypeCodeInfo[i].codes)
2929
ensures SCMPTypeCodeMem()
3030
decreases
3131
func satisfyInitEnsures() int {

‎router/dataplane.go‎

Lines changed: 30 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -564,8 +564,8 @@ func (d *DataPlane) getInterfaceState(interfaceID uint16) control.InterfaceState
564564
// @ defer fold acc(accBfdSession(d.bfdSessions), R20)
565565
// @ }
566566
if bfdSession, ok := bfdSessions[interfaceID]; ok {
567-
// @ assert interfaceID in domain(d.bfdSessions)
568-
// @ assert bfdSession in range(d.bfdSessions)
567+
// @ assert interfaceID elem domain(d.bfdSessions)
568+
// @ assert bfdSession elem range(d.bfdSessions)
569569
// @ assert bfdSession != nil
570570
// (VerifiedSCION) This checked used to be conjoined with 'ok' in the condition
571571
// of the if stmt above. We broke it down to perform intermediate asserts.
@@ -835,12 +835,12 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
835835
// dPtr as an helper parameter. It always receives the value &d.
836836
// @ requires acc(dPtr, _)
837837
// @ requires let d := *dPtr in
838-
// @ acc(d.Mem(), _) &&
839-
// @ d.WellConfigured() &&
840-
// @ d.getValSvc() != nil &&
841-
// @ d.getValForwardingMetrics() != nil &&
842-
// @ (0 in d.getDomForwardingMetrics()) &&
843-
// @ (ingressID in d.getDomForwardingMetrics()) &&
838+
// @ acc(d.Mem(), _) &&
839+
// @ d.WellConfigured() &&
840+
// @ d.getValSvc() != nil &&
841+
// @ d.getValForwardingMetrics() != nil &&
842+
// @ (0 elem d.getDomForwardingMetrics()) &&
843+
// @ (ingressID elem d.getDomForwardingMetrics()) &&
844844
// @ d.getMacFactory() != nil
845845
// @ requires rd != nil && acc(rd.Mem(), _)
846846
// contracts for IO-spec
@@ -919,8 +919,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
919919
// @ invariant acc(d.Mem(), _) && d.WellConfigured()
920920
// @ invariant d.getValSvc() != nil
921921
// @ invariant d.getValForwardingMetrics() != nil
922-
// @ invariant 0 in d.getDomForwardingMetrics()
923-
// @ invariant ingressID in d.getDomForwardingMetrics()
922+
// @ invariant 0 elem d.getDomForwardingMetrics()
923+
// @ invariant ingressID elem d.getDomForwardingMetrics()
924924
// @ invariant acc(rd.Mem(), _)
925925
// @ invariant processor.sInit() && processor.sInitD() === d
926926
// @ invariant let ubuf := processor.sInitBufferUBuf() in
@@ -991,8 +991,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
991991
// @ invariant acc(d.Mem(), _) && d.WellConfigured()
992992
// @ invariant d.getValSvc() != nil
993993
// @ invariant d.getValForwardingMetrics() != nil
994-
// @ invariant 0 in d.getDomForwardingMetrics()
995-
// @ invariant ingressID in d.getDomForwardingMetrics()
994+
// @ invariant 0 elem d.getDomForwardingMetrics()
995+
// @ invariant ingressID elem d.getDomForwardingMetrics()
996996
// @ invariant acc(rd.Mem(), _)
997997
// @ invariant pkts <= len(msgs)
998998
// @ invariant 0 <= i0 && i0 <= pkts
@@ -1147,7 +1147,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
11471147
// @ ghost t, s := *ioSharedArg.Place, *ioSharedArg.State
11481148
// @ ghost if(newAbsPkt.isValPkt) {
11491149
// @ ApplyElemWitness(s.obuf, ioSharedArg.OBufY, newAbsPkt.ValPkt_1, newAbsPkt.ValPkt_2)
1150-
// @ assert newAbsPkt.ValPkt_2 in AsSet(s.obuf[newAbsPkt.ValPkt_1])
1150+
// @ assert newAbsPkt.ValPkt_2 elem AsSet(s.obuf[newAbsPkt.ValPkt_1])
11511151
// @ assert dp.dp3s_iospec_bio3s_send_guard(s, t, newAbsPkt)
11521152
// @ } else { assert newAbsPkt.isValUnsupported }
11531153
// @ unfold dp.dp3s_iospec_ordered(s, t)
@@ -1188,7 +1188,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
11881188
}
11891189
// @ requires acc(dPtr, _) && *dPtr === d
11901190
// @ requires acc(d.Mem(), _)
1191-
// @ requires result.EgressID in d.getDomForwardingMetrics()
1191+
// @ requires result.EgressID elem d.getDomForwardingMetrics()
11921192
// @ decreases
11931193
// @ outline(
11941194
// ok metric
@@ -1208,7 +1208,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
12081208
}
12091209
// @ unfold acc(d.Mem(), R1)
12101210
// @ assert d.WellConfigured()
1211-
// @ assert 0 in d.getDomForwardingMetrics()
1211+
// @ assert 0 elem d.getDomForwardingMetrics()
12121212
// @ ghost if d.bfdSessions != nil { unfold acc(accBfdSession(d.bfdSessions), R2) }
12131213

12141214
// (VerifiedSCION) we introduce this to avoid problems with the invariants that
@@ -1257,7 +1257,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
12571257
// @ invariant acc(d.Mem(), _) && d.WellConfigured()
12581258
// @ invariant d.getValSvc() != nil
12591259
// @ invariant d.getValForwardingMetrics() != nil
1260-
// @ invariant 0 in d.getDomForwardingMetrics()
1260+
// @ invariant 0 elem d.getDomForwardingMetrics()
12611261
// @ invariant d.getMacFactory() != nil
12621262
// @ invariant dp.Valid()
12631263
// @ invariant d.DpAgreesWithSpec(dp)
@@ -1271,8 +1271,8 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
12711271
// @ requires acc(d.Mem(), _) && d.WellConfigured()
12721272
// @ requires d.getValSvc() != nil
12731273
// @ requires d.getValForwardingMetrics() != nil
1274-
// @ requires 0 in d.getDomForwardingMetrics()
1275-
// @ requires i in d.getDomForwardingMetrics()
1274+
// @ requires 0 elem d.getDomForwardingMetrics()
1275+
// @ requires i elem d.getDomForwardingMetrics()
12761276
// @ requires d.getMacFactory() != nil
12771277
// @ requires c != nil && acc(c.Mem(), _)
12781278
// contracts for IO-spec
@@ -1285,7 +1285,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
12851285
read(i, c, &d /*@, ioLock, ioSharedArg, dp @*/) //@ as rc
12861286
}
12871287
// @ ghost if d.external != nil { unfold acc(accBatchConn(d.external), R50) }
1288-
// @ assert v in range(d.external)
1288+
// @ assert v elem range(d.external)
12891289
// @ assert acc(v.Mem(), _)
12901290
// @ d.InDomainExternalInForwardingMetrics3(ifID)
12911291
// @ ghost if d.external != nil { fold acc(accBatchConn(d.external), R50) }
@@ -1297,7 +1297,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
12971297
// @ requires acc(d.Mem(), _) && d.WellConfigured()
12981298
// @ requires d.getValSvc() != nil
12991299
// @ requires d.getValForwardingMetrics() != nil
1300-
// @ requires 0 in d.getDomForwardingMetrics()
1300+
// @ requires 0 elem d.getDomForwardingMetrics()
13011301
// @ requires d.getMacFactory() != nil
13021302
// @ requires c != nil && acc(c.Mem(), _)
13031303
// contracts for IO-spec
@@ -1334,7 +1334,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
13341334
// @ ensures d.Mem()
13351335
// @ ensures d.MetricsAreSet()
13361336
// @ ensures d.WellConfigured()
1337-
// @ ensures 0 in d.DomainForwardingMetrics()
1337+
// @ ensures 0 elem d.DomainForwardingMetrics()
13381338
// @ ensures d.InternalConnIsSet()
13391339
// @ ensures d.KeyIsSet()
13401340
// @ ensures d.SvcsAreSet()
@@ -1386,14 +1386,14 @@ func (d *DataPlane) initMetrics( /*@ ghost dp io.DataPlaneSpec @*/ ) {
13861386
// @ invariant d.external === dExternal
13871387
// @ invariant acc(&d.forwardingMetrics) && acc(d.forwardingMetrics)
13881388
// @ invariant domain(d.forwardingMetrics) == set[uint16]{0} union visitedSet
1389-
// @ invariant 0 in domain(d.forwardingMetrics)
1389+
// @ invariant 0 elem domain(d.forwardingMetrics)
13901390
// @ invariant acc(&d.internalNextHops, R15)
13911391
// @ invariant d.internalNextHops === dInternalNextHops
13921392
// @ invariant d.internalNextHops != nil ==> acc(d.internalNextHops, R20)
13931393
// @ invariant domain(d.internalNextHops) intersection domain(d.external) == set[uint16]{}
13941394
// @ invariant acc(&d.neighborIAs, R15)
13951395
// @ invariant d.neighborIAs != nil ==> acc(d.neighborIAs, R15)
1396-
// @ invariant forall i uint16 :: { d.forwardingMetrics[i] } i in domain(d.forwardingMetrics) ==>
1396+
// @ invariant forall i uint16 :: { d.forwardingMetrics[i] } i elem domain(d.forwardingMetrics) ==>
13971397
// @ acc(forwardingMetricsMem(d.forwardingMetrics[i], i), _)
13981398
// @ invariant acc(&d.Metrics, R15)
13991399
// @ invariant acc(d.Metrics.Mem(), _)
@@ -1694,7 +1694,7 @@ func (p *scionPacketProcessor) processInterBFD(oh *onehop.Path, data []byte) (er
16941694
}
16951695

16961696
if v, ok := p.d.bfdSessions[p.ingressID]; ok {
1697-
// @ assert v in range(p.d.bfdSessions)
1697+
// @ assert v elem range(p.d.bfdSessions)
16981698
v.ReceiveMessage(bfd /*@ , data @*/)
16991699
return nil
17001700
}
@@ -1742,12 +1742,12 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
17421742
// @ invariant acc(&p.d.internalNextHops, _)
17431743
// @ invariant m === p.d.internalNextHops
17441744
// @ invariant m != nil ==> acc(m, R20)
1745-
// @ invariant m != nil ==> forall a *net.UDPAddr :: { a in range(m) } a in range(m) ==> acc(a.Mem(), _)
1745+
// @ invariant m != nil ==> forall a *net.UDPAddr :: { a elem range(m) } a elem range(m) ==> acc(a.Mem(), _)
17461746
// @ invariant acc(&p.srcAddr, R20) && acc(p.srcAddr.Mem(), _)
17471747
// @ decreases len(p.d.internalNextHops) - len(keys)
17481748
for k, v := range p.d.internalNextHops /*@ with keys @*/ {
17491749
// @ assert acc(&p.d.internalNextHops, _)
1750-
// @ assert forall a *net.UDPAddr :: { a in range(m) } a in range(m) ==> acc(a.Mem(), _)
1750+
// @ assert forall a *net.UDPAddr :: { a elem range(m) } a elem range(m) ==> acc(a.Mem(), _)
17511751
// @ assert acc(v.Mem(), _)
17521752
// @ unfold acc(v.Mem(), _)
17531753
// @ unfold acc(p.srcAddr.Mem(), _)
@@ -1763,7 +1763,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
17631763
// @ assert acc(&p.d.bfdSessions, _)
17641764
// @ ghost if p.d.bfdSessions != nil { unfold acc(accBfdSession(p.d.bfdSessions), _) }
17651765
if v, ok := p.d.bfdSessions[ifID]; ok {
1766-
// @ assert v in range(p.d.bfdSessions)
1766+
// @ assert v elem range(p.d.bfdSessions)
17671767
v.ReceiveMessage(bfd /*@ , data @*/)
17681768
return nil
17691769
}
@@ -2544,8 +2544,8 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @
25442544
// @ ghost if p.d.internalNextHops != nil { unfold acc(accAddr(p.d.internalNextHops), _) }
25452545
expectedSrc, ok := p.d.internalNextHops[pktIngressID]
25462546
// @ ghost if ok {
2547-
// @ assert expectedSrc in range(p.d.internalNextHops)
2548-
// @ unfold acc(expectedSrc.Mem(), _)
2547+
// @ assert expectedSrc elem range(p.d.internalNextHops)
2548+
// @ unfold acc(expectedSrc.Mem(), _)
25492549
// @ }
25502550
// @ unfold acc(p.srcAddr.Mem(), _)
25512551
if !ok || !expectedSrc.IP.Equal(p.srcAddr.IP) {
@@ -4191,7 +4191,7 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /
41914191
// @ ghost if p.d.external != nil { unfold acc(accBatchConn(p.d.external), _) }
41924192
if c, ok := p.d.external[ohp.FirstHop.ConsEgress]; ok {
41934193
// @ p.d.getDomExternalLemma()
4194-
// @ assert ohp.FirstHop.ConsEgress in p.d.getDomExternal()
4194+
// @ assert ohp.FirstHop.ConsEgress elem p.d.getDomExternal()
41954195
// @ p.d.InDomainExternalInForwardingMetrics(ohp.FirstHop.ConsEgress)
41964196
// @ fold p.d.validResult(processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt}, false)
41974197
return processResult{EgressID: ohp.FirstHop.ConsEgress, OutConn: c, OutPkt: p.rawPkt},

‎router/dataplane_concurrency_model.gobra‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -258,7 +258,7 @@ pred ElemWitness(ghost y ElemRA, ghost k Key, ghost e Elem)
258258
ghost
259259
decreases
260260
requires ElemAuth(m, y) && ElemWitness(y, k, e)
261-
ensures ElemAuth(m, y) && ElemWitness(y, k, e) && k in domain(m) && e in AsSet(m[k])
261+
ensures ElemAuth(m, y) && ElemWitness(y, k, e) && k elem domain(m) && e elem AsSet(m[k])
262262
func ApplyElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem)
263263

264264
ghost

0 commit comments

Comments
 (0)