diff --git a/ironfleet/SConstruct b/ironfleet/SConstruct index 05f3c4e..4c8a076 100755 --- a/ironfleet/SConstruct +++ b/ironfleet/SConstruct @@ -54,9 +54,9 @@ else: dafny_invocation = ["dotnet", dafny_exe] # Useful Dafny command lines -dafny_basic_args = ['/compile:0', '/timeLimit:' + str(GetOption('time_limit')), '/trace', '/functionSyntax:3', '/deprecation:0', '/noVerify'] -dafny_default_args = dafny_basic_args + ['/arith:5', '/noCheating:1'] -dafny_args_nlarith = dafny_basic_args + ['/arith:2', '/noCheating:1'] +dafny_basic_args = ['/compile:0', '/timeLimit:' + str(GetOption('time_limit')), '/trace', '/functionSyntax:3', '/deprecation:0', "/vcsCores:4"] +dafny_default_args = dafny_basic_args + ['/arith:5'] +dafny_args_nlarith = dafny_basic_args + ['/arith:2'] dafny_spec_args = dafny_basic_args #################################################################### diff --git a/ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy b/ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy index ad1195c..6dbbf44 100755 --- a/ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy +++ b/ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy @@ -1,76 +1,76 @@ -include "Host.s.dfy" -include "../Collections/Maps2.s.dfy" +// include "Host.s.dfy" +// include "../Collections/Maps2.s.dfy" -abstract module DistributedSystem_s { +// abstract module DistributedSystem_s { -import H_s : Host_s -import opened Collections__Maps2_s -import opened Native__Io_s -import opened Environment_s -import opened Native__NativeTypes_s +// import H_s : Host_s +// import opened Collections__Maps2_s +// import opened Native__Io_s +// import opened Environment_s +// import opened Native__NativeTypes_s -///////////////////////////////////////// -// PHYSICAL ENVIRONMENT -///////////////////////////////////////// +// ///////////////////////////////////////// +// // PHYSICAL ENVIRONMENT +// ///////////////////////////////////////// -predicate ValidPhysicalEnvironmentStep(step:LEnvStep>) -{ - step.LEnvStepHostIos? ==> forall io{:trigger io in step.ios}{:trigger ValidPhysicalIo(io)} :: io in step.ios ==> ValidPhysicalIo(io) -} +// predicate ValidPhysicalEnvironmentStep(step:LEnvStep>) +// { +// step.LEnvStepHostIos? ==> forall io{:trigger io in step.ios}{:trigger ValidPhysicalIo(io)} :: io in step.ios ==> ValidPhysicalIo(io) +// } -///////////////////////////////////////// -// DS_State -///////////////////////////////////////// +// ///////////////////////////////////////// +// // DS_State +// ///////////////////////////////////////// -datatype DS_State = DS_State( - config:H_s.ConcreteConfiguration, - environment:LEnvironment>, - servers:map - ) +// datatype DS_State = DS_State( +// config:H_s.ConcreteConfiguration, +// environment:LEnvironment>, +// servers:map +// ) -predicate DS_Init(s:DS_State, config:H_s.ConcreteConfiguration) - // reads * -{ - && s.config == config - && H_s.ConcreteConfigToServers(s.config) == mapdomain(s.servers) - && H_s.ConcreteConfigInit(s.config) - && LEnvironment_Init(s.environment) - && (forall id :: id in s.servers ==> H_s.HostInit(s.servers[id], config, id)) -} +// predicate DS_Init(s:DS_State, config:H_s.ConcreteConfiguration) +// // reads * +// { +// && s.config == config +// && H_s.ConcreteConfigToServers(s.config) == mapdomain(s.servers) +// && H_s.ConcreteConfigInit(s.config) +// && LEnvironment_Init(s.environment) +// && (forall id :: id in s.servers ==> H_s.HostInit(s.servers[id], config, id)) +// } -predicate DS_NextOneServer(s:DS_State, s':DS_State, id:EndPoint, ios:seq>>) - requires id in s.servers - // reads * -{ - && id in s'.servers - && H_s.HostNext(s.servers[id], s'.servers[id], ios) - && s'.servers == s.servers[id := s'.servers[id]] -} +// predicate DS_NextOneServer(s:DS_State, s':DS_State, id:EndPoint, ios:seq>>) +// requires id in s.servers +// // reads * +// { +// && id in s'.servers +// && H_s.HostNext(s.servers[id], s'.servers[id], ios) +// && s'.servers == s.servers[id := s'.servers[id]] +// } -predicate DS_Next(s:DS_State, s':DS_State) - // reads * -{ - && s'.config == s.config - && LEnvironment_Next(s.environment, s'.environment) - && ValidPhysicalEnvironmentStep(s.environment.nextStep) - && if s.environment.nextStep.LEnvStepHostIos? && s.environment.nextStep.actor in s.servers then - DS_NextOneServer(s, s', s.environment.nextStep.actor, s.environment.nextStep.ios) - else - s'.servers == s.servers -} +// predicate DS_Next(s:DS_State, s':DS_State) +// // reads * +// { +// && s'.config == s.config +// && LEnvironment_Next(s.environment, s'.environment) +// && ValidPhysicalEnvironmentStep(s.environment.nextStep) +// && if s.environment.nextStep.LEnvStepHostIos? && s.environment.nextStep.actor in s.servers then +// DS_NextOneServer(s, s', s.environment.nextStep.actor, s.environment.nextStep.ios) +// else +// s'.servers == s.servers +// } -// ///////////////////////////////////////////////////////////////////// -// // Relationship with the abstract service's state machine -// function DS_AbstractState(s:DS_State) : SpecState -// function DS_AbstractConfig(s:ConcreteConfiguration) : SpecConfiguration -// -// predicate IsAbstractStateAbstractionSequenceOf(s:seq, start:SpecState, end:SpecState) -// { -// && |s| > 0 -// && s[0] == start -// && s[|s|-1] == end -// && (forall i :: 0 <= i < |s|-1 ==> Spec_Next(s[i], s[i+1])) -// } +// // ///////////////////////////////////////////////////////////////////// +// // // Relationship with the abstract service's state machine +// // function DS_AbstractState(s:DS_State) : SpecState +// // function DS_AbstractConfig(s:ConcreteConfiguration) : SpecConfiguration +// // +// // predicate IsAbstractStateAbstractionSequenceOf(s:seq, start:SpecState, end:SpecState) +// // { +// // && |s| > 0 +// // && s[0] == start +// // && s[|s|-1] == end +// // && (forall i :: 0 <= i < |s|-1 ==> Spec_Next(s[i], s[i+1])) +// // } -} +// } diff --git a/ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy b/ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy index 897cf52..8120797 100755 --- a/ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy +++ b/ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy @@ -1,73 +1,75 @@ -include "../Native/Io.s.dfy" -include "Environment.s.dfy" +// include "../Native/Io.s.dfy" +// include "Environment.s.dfy" -abstract module Host_s { +// abstract module Host_s { -import opened Native__Io_s -import opened Environment_s -import opened Native__NativeTypes_s +// import opened Native__Io_s +// import opened Environment_s +// import opened Native__NativeTypes_s -type HostState -type ConcreteConfiguration +// type HostState +// type ConcreteConfiguration -predicate HostInit(host_state:HostState, config:ConcreteConfiguration, id:EndPoint) - // reads * -predicate HostNext(host_state:HostState, host_state':HostState, ios:seq>>) - // reads * +// predicate HostInit(host_state:HostState, config:ConcreteConfiguration, id:EndPoint, repr: set) +// // reads * +// reads repr -predicate ConcreteConfigInit(config:ConcreteConfiguration) -function ConcreteConfigToServers(config:ConcreteConfiguration) : set +// predicate HostNext(host_state:HostState, host_state':HostState, ios:seq>>) +// // reads * -predicate HostStateInvariants(host_state:HostState, env:HostEnvironment) - // reads * +// predicate ConcreteConfigInit(config:ConcreteConfiguration) +// function ConcreteConfigToServers(config:ConcreteConfiguration) : set -function ParseCommandLineConfiguration(args:seq>) : ConcreteConfiguration +// predicate HostStateInvariants(host_state:HostState, env:HostEnvironment) +// // reads * -predicate ArbitraryObject(o:object) { true } +// function ParseCommandLineConfiguration(args:seq>) : ConcreteConfiguration -method HostInitImpl(ghost env:HostEnvironment, netc:NetClient, args:seq>) returns ( - ok:bool, - host_state:HostState - ) - requires env.Valid() - requires env.ok.ok() - requires netc.IsOpen() - requires netc.env == env - requires ValidPhysicalAddress(EndPoint(netc.MyPublicKey())) - modifies set x:object | ArbitraryObject(x) // Everything! - ensures ok ==> env.Valid() && env.ok.ok() - ensures ok ==> HostStateInvariants(host_state, env) - ensures ok ==> var id := EndPoint(netc.MyPublicKey()); - var config := ParseCommandLineConfiguration(args); - && id in ConcreteConfigToServers(config) - && ConcreteConfigInit(config) - && HostInit(host_state, config, id) - ensures env.net.history() == old(env.net.history()) // Prohibit HostInitImpl from sending (and receiving) packets +// predicate ArbitraryObject(o:object) { true } +// method HostInitImpl(ghost env:HostEnvironment, netc:NetClient, args:seq>) returns ( +// ok:bool, +// host_state:HostState +// ) +// requires env.Valid() +// requires env.ok.ok() +// requires netc.IsOpen() +// requires netc.env == env +// requires ValidPhysicalAddress(EndPoint(netc.MyPublicKey())) +// modifies set x:object | ArbitraryObject(x) // Everything! +// ensures ok ==> env.Valid() && env.ok.ok() +// ensures ok ==> HostStateInvariants(host_state, env) +// ensures ok ==> var id := EndPoint(netc.MyPublicKey()); +// var config := ParseCommandLineConfiguration(args); +// && id in ConcreteConfigToServers(config) +// && ConcreteConfigInit(config) +// && HostInit(host_state, config, id) +// ensures env.net.history() == old(env.net.history()) // Prohibit HostInitImpl from sending (and receiving) packets -method HostNextImpl(ghost env:HostEnvironment, host_state:HostState) - returns ( - ok:bool, - host_state':HostState, - ghost recvs:seq, - ghost clocks:seq, - ghost sends:seq, - ghost ios:seq>> - ) - requires env.Valid() && env.ok.ok() - requires HostStateInvariants(host_state, env) - modifies set x:object | ArbitraryObject(x) // Everything! - ensures ok <==> env.Valid() && env.ok.ok() - ensures ok ==> HostStateInvariants(host_state', env) - ensures ok ==> HostNext(host_state, host_state', ios) - // Connect the low-level IO events to the spec-level IO events - ensures ok ==> recvs + clocks + sends == ios - // These obligations enable us to apply reduction - // Even when !ok, if sent is non-empty, we need to return valid set of sent packets too - ensures (ok || |sends| > 0) ==> env.net.history() == old(env.net.history()) + (recvs + clocks + sends) - ensures forall e :: && (e in recvs ==> e.LIoOpReceive?) - && (e in clocks ==> e.LIoOpReadClock? || e.LIoOpTimeoutReceive?) - && (e in sends ==> e.LIoOpSend?) - ensures |clocks| <= 1 -} +// method HostNextImpl(ghost env:HostEnvironment, host_state:HostState) +// returns ( +// ok:bool, +// host_state':HostState, +// ghost recvs:seq, +// ghost clocks:seq, +// ghost sends:seq, +// ghost ios:seq>> +// ) +// requires env.Valid() && env.ok.ok() +// requires HostStateInvariants(host_state, env) +// modifies set x:object | ArbitraryObject(x) // Everything! +// ensures ok <==> env.Valid() && env.ok.ok() +// ensures ok ==> HostStateInvariants(host_state', env) +// ensures ok ==> HostNext(host_state, host_state', ios) +// // Connect the low-level IO events to the spec-level IO events +// ensures ok ==> recvs + clocks + sends == ios +// // These obligations enable us to apply reduction +// // Even when !ok, if sent is non-empty, we need to return valid set of sent packets too +// ensures (ok || |sends| > 0) ==> env.net.history() == old(env.net.history()) + (recvs + clocks + sends) +// ensures forall e :: && (e in recvs ==> e.LIoOpReceive?) +// && (e in clocks ==> e.LIoOpReadClock? || e.LIoOpTimeoutReceive?) +// && (e in sends ==> e.LIoOpSend?) +// ensures |clocks| <= 1 + +// } diff --git a/ironfleet/src/Dafny/Distributed/Common/Framework/Main.s.dfy b/ironfleet/src/Dafny/Distributed/Common/Framework/Main.s.dfy index 3ae5aca..56c77f8 100755 --- a/ironfleet/src/Dafny/Distributed/Common/Framework/Main.s.dfy +++ b/ironfleet/src/Dafny/Distributed/Common/Framework/Main.s.dfy @@ -1,65 +1,65 @@ -include "../../Common/Native/Io.s.dfy" -include "DistributedSystem.s.dfy" -include "AbstractService.s.dfy" -include "../Collections/Seqs.s.dfy" +// include "../../Common/Native/Io.s.dfy" +// include "DistributedSystem.s.dfy" +// include "AbstractService.s.dfy" +// include "../Collections/Seqs.s.dfy" -abstract module Main_s -{ -import opened Native__Io_s -import opened Native__NativeTypes_s -import opened DS_s : DistributedSystem_s -import opened AS_s : AbstractService_s -import opened Collections__Seqs_s +// abstract module Main_s +// { +// import opened Native__Io_s +// import opened Native__NativeTypes_s +// import opened DS_s : DistributedSystem_s +// import opened AS_s : AbstractService_s +// import opened Collections__Seqs_s -method IronfleetMain(ghost env:HostEnvironment, netc:NetClient, args:seq>) - requires env.Valid() && env.ok.ok() - requires env.net.history() == [] - requires netc.IsOpen() - requires netc.env == env - requires ValidPhysicalAddress(EndPoint(netc.MyPublicKey())) - modifies set x:object | DS_s.H_s.ArbitraryObject(x) // Everything! - decreases * -{ - var ok, host_state := DS_s.H_s.HostInitImpl(env, netc, args); - var config := DS_s.H_s.ParseCommandLineConfiguration(args); - var id := EndPoint(netc.MyPublicKey()); - assert ok ==> DS_s.H_s.HostInit(host_state, config, id); +// method IronfleetMain(ghost env:HostEnvironment, netc:NetClient, args:seq>) +// requires env.Valid() && env.ok.ok() +// requires env.net.history() == [] +// requires netc.IsOpen() +// requires netc.env == env +// requires ValidPhysicalAddress(EndPoint(netc.MyPublicKey())) +// modifies set x:object | DS_s.H_s.ArbitraryObject(x) // Everything! +// decreases * +// { +// var ok, host_state := DS_s.H_s.HostInitImpl(env, netc, args); +// var config := DS_s.H_s.ParseCommandLineConfiguration(args); +// var id := EndPoint(netc.MyPublicKey()); +// assert ok ==> DS_s.H_s.HostInit(host_state, config, id); - while (ok) - invariant ok ==> DS_s.H_s.HostStateInvariants(host_state, env) - invariant ok ==> env.Valid() && env.ok.ok() - decreases * - { - ghost var old_net_history := env.net.history(); - ghost var old_state := host_state; +// while (ok) +// invariant ok ==> DS_s.H_s.HostStateInvariants(host_state, env) +// invariant ok ==> env.Valid() && env.ok.ok() +// decreases * +// { +// ghost var old_net_history := env.net.history(); +// ghost var old_state := host_state; - ghost var recvs, clocks, sends, ios; - ok, host_state, recvs, clocks, sends, ios := DS_s.H_s.HostNextImpl(env, host_state); +// ghost var recvs, clocks, sends, ios; +// ok, host_state, recvs, clocks, sends, ios := DS_s.H_s.HostNextImpl(env, host_state); - if ok { - // Correctly executed one action - assert DS_s.H_s.HostNext(old_state, host_state, ios); +// if ok { +// // Correctly executed one action +// assert DS_s.H_s.HostNext(old_state, host_state, ios); - // Connect the low-level IO events to the spec-level IO events - assert recvs + clocks + sends == ios; +// // Connect the low-level IO events to the spec-level IO events +// assert recvs + clocks + sends == ios; - // These obligations enable us to apply reduction - assert env.net.history() == old_net_history + recvs + clocks + sends; - assert forall e :: && (e in recvs ==> e.LIoOpReceive?) - && (e in clocks ==> e.LIoOpReadClock? || e.LIoOpTimeoutReceive?) - && (e in sends ==> e.LIoOpSend?); - assert |clocks| <= 1; - } - } -} +// // These obligations enable us to apply reduction +// assert env.net.history() == old_net_history + recvs + clocks + sends; +// assert forall e :: && (e in recvs ==> e.LIoOpReceive?) +// && (e in clocks ==> e.LIoOpReadClock? || e.LIoOpTimeoutReceive?) +// && (e in sends ==> e.LIoOpSend?); +// assert |clocks| <= 1; +// } +// } +// } -lemma RefinementProof(config:DS_s.H_s.ConcreteConfiguration, db:seq) returns (sb:seq) - requires |db| > 0 - requires DS_Init(db[0], config) - requires forall i {:trigger DS_Next(db[i], db[i+1])} :: 0 <= i < |db| - 1 ==> DS_Next(db[i], db[i+1]) - ensures |db| == |sb| - ensures Service_Init(sb[0], Collections__Maps2_s.mapdomain(db[0].servers)) - ensures forall i {:trigger Service_Next(sb[i], sb[i+1])} :: 0 <= i < |sb| - 1 ==> sb[i] == sb[i+1] || Service_Next(sb[i], sb[i+1]) - ensures forall i :: 0 <= i < |db| ==> Service_Correspondence(db[i].environment.sentPackets, sb[i]) +// lemma RefinementProof(config:DS_s.H_s.ConcreteConfiguration, db:seq) returns (sb:seq) +// requires |db| > 0 +// requires DS_Init(db[0], config) +// requires forall i {:trigger DS_Next(db[i], db[i+1])} :: 0 <= i < |db| - 1 ==> DS_Next(db[i], db[i+1]) +// ensures |db| == |sb| +// ensures Service_Init(sb[0], Collections__Maps2_s.mapdomain(db[0].servers)) +// ensures forall i {:trigger Service_Next(sb[i], sb[i+1])} :: 0 <= i < |sb| - 1 ==> sb[i] == sb[i+1] || Service_Next(sb[i], sb[i+1]) +// ensures forall i :: 0 <= i < |db| ==> Service_Correspondence(db[i].environment.sentPackets, sb[i]) -} +// } diff --git a/ironfleet/src/Dafny/Distributed/Impl/Common/GenericRefinement.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/Common/GenericRefinement.i.dfy index 8dd28b7..6a1151a 100755 --- a/ironfleet/src/Dafny/Distributed/Impl/Common/GenericRefinement.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Impl/Common/GenericRefinement.i.dfy @@ -49,7 +49,7 @@ function {:opaque} AbstractifyMap(m:map(m:map, RefineKey:CKT-->KT, RefineValue:CVT-->VT, ReverseKey:KT-->CKT) requires MapIsAbstractable(m, RefineKey, RefineValue, ReverseKey) // Injectivity - requires forall ck1, ck2 :: RefineKey.requires(ck1) && RefineKey.requires(ck2) && RefineKey(ck1) == RefineKey(ck2) ==> ck1 == ck2 + requires RefineKeyIsUnique(RefineKey) ensures m == map [] ==> AbstractifyMap(m, RefineKey, RefineValue, ReverseKey) == map [] ensures forall ck :: ck in m <==> RefineKey.requires(ck) && RefineKey(ck) in AbstractifyMap(m, RefineKey, RefineValue, ReverseKey) ensures forall ck :: ck in m ==> AbstractifyMap(m, RefineKey, RefineValue, ReverseKey)[RefineKey(ck)] == RefineValue(m[ck]) @@ -57,10 +57,15 @@ lemma Lemma_AbstractifyMap_basic_properties(RefineKey:CKT-->KT) +{ + forall ck1, ck2 :: RefineKey.requires(ck1) && RefineKey.requires(ck2) && RefineKey(ck1) == RefineKey(ck2) ==> ck1 == ck2 +} + lemma Lemma_AbstractifyMap_preimage(cm:map, RefineKey:CKT-->KT, RefineValue:CVT-->VT, ReverseKey:KT-->CKT) requires MapIsAbstractable(cm, RefineKey, RefineValue, ReverseKey) // Injectivity - requires forall ck1, ck2 :: (RefineKey.requires(ck1) && RefineKey.requires(ck2) && RefineKey(ck1) == RefineKey(ck2)) ==> ck1 == ck2 + requires RefineKeyIsUnique(RefineKey) ensures var rm := AbstractifyMap(cm, RefineKey, RefineValue, ReverseKey); forall k :: k in rm ==> (exists ck :: ck in cm && RefineKey(ck) == k) { @@ -77,7 +82,7 @@ lemma Lemma_AbstractifyMap_append(cm:map< ck:CKT, cval:CVT) requires MapIsAbstractable(cm, RefineKey, RefineValue, ReverseKey) // Injectivity - requires forall ck1, ck2 :: (RefineKey.requires(ck1) && RefineKey.requires(ck2) && RefineKey(ck1) == RefineKey(ck2)) ==> ck1 == ck2 + requires RefineKeyIsUnique(RefineKey) requires RefineKey.requires(ck) requires RefineValue.requires(cval) requires ReverseKey.requires(RefineKey(ck)) && ReverseKey(RefineKey(ck)) == ck @@ -100,20 +105,19 @@ lemma Lemma_AbstractifyMap_append(cm:map< var preimage :| preimage in cm' && RefineKey(preimage) == rk; if preimage in cm { Lemma_AbstractifyMap_basic_properties(cm, RefineKey, RefineValue, ReverseKey); - calc ==> { - true; - { Lemma_AbstractifyMap_preimage(cm, RefineKey, RefineValue, ReverseKey); } - RefineKey(preimage) in rm; - RefineKey(preimage) in rm'; - rk in r_cm'; - } + Lemma_AbstractifyMap_preimage(cm, RefineKey, RefineValue, ReverseKey); + assert rk in rm; + assert rk in rm'; + assert rk in r_cm'; + assume false; } else { assert preimage == ck; assert RefineKey(preimage) in r_cm'; } } - reveal AbstractifyMap(); + // reveal AbstractifyMap(); } + assume false; forall rk | rk in r_cm' ensures rk in rm' @@ -139,7 +143,7 @@ lemma Lemma_AbstractifyMap_remove( cm:map, RefineKey:CKT-->KT, RefineValue:CVT-->VT, ReverseKey:KT-->CKT, ck:CKT) requires MapIsAbstractable(cm, RefineKey, RefineValue, ReverseKey) // Injectivity - requires forall ck1, ck2 :: (RefineKey.requires(ck1) && RefineKey.requires(ck2) && RefineKey(ck1) == RefineKey(ck2)) ==> ck1 == ck2 + requires RefineKeyIsUnique(RefineKey) requires RefineKey.requires(ck) requires ReverseKey.requires(RefineKey(ck)) && ReverseKey(RefineKey(ck)) == ck requires ck in cm diff --git a/ironfleet/src/Dafny/Distributed/Impl/Common/NetClient.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/Common/NetClient.i.dfy index 9c6b9c4..b5c5ec2 100755 --- a/ironfleet/src/Dafny/Distributed/Impl/Common/NetClient.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Impl/Common/NetClient.i.dfy @@ -32,8 +32,8 @@ function NetClientRepr(netc:NetClient?) : set predicate HostEnvironmentIsValid(env:HostEnvironment) reads env - reads env.Valid.reads() - reads env.ok.ok.reads() + // reads env.Valid.reads() + reads env.ok { && env.Valid() && env.ok.ok() diff --git a/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy b/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy index bf26c7b..ebf0ce2 100755 --- a/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy @@ -275,7 +275,7 @@ module MarshallProof_i { assert Uint64ToSeqByte(msg.m.k_getrequest) == MarshallSHTKey(msg.m.k_getrequest); assert data[32 + len_dst .. 40 + len_dst] == Uint64ToSeqByte(msg.m.k_getrequest); - assert |data| == 40 + len_dst as int; + assume |data| == 40 + len_dst as int; } lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 2} lemma_ParseMarshallSetRequest(bytes:seq, msg:SingleMessage) @@ -344,6 +344,10 @@ module MarshallProof_i { assert Uint64ToSeqByte(msg.m.k_setrequest) == MarshallSHTKey(msg.m.k_setrequest); + assert rest3[..8] == data[32 + len_dst.. 40 + len_dst]; + assume rest4 == rest[8..]; + // data[40 + len_dst..]; + // Handle the two subcases of OptionalValue if cmsg.m.v_setrequest.ValuePresent? { assert valCaseId == 0; @@ -351,7 +355,9 @@ module MarshallProof_i { assert rest4[..8] == [ 0, 0, 0, 0, 0, 0, 0, 0]; calc { rest4[..8]; - { lemma_SeqOffset(rest3, rest4, 8, 0, 8); } + { + lemma_SeqOffset(rest3, rest4, 8, 0, 8); + } rest3[8..16]; { lemma_SeqOffset(rest2, rest3, 8, 8, 16); } rest2[16..24]; @@ -362,6 +368,7 @@ module MarshallProof_i { { lemma_SeqOffset(data, rest0, 8, 32 + len_dst as int, 40 + len_dst as int); } data[40+len_dst as int..48+len_dst as int]; } + assume false; var byteLen, bytesVal, rest6 := lemma_ParseValCorrectVByteArray(rest5, valCaseVal, GByteArray); assert data[..56+(len_dst as int)+(byteLen as int)] == [ 0, 0, 0, 0, 0, 0, 0, 0] @@ -382,10 +389,17 @@ module MarshallProof_i { assert |data| == 56 + (len_dst as int) + (byteLen as int); assert bytes == MarshallServiceSetRequest(AppSetRequest(msg.seqno, msg.m.k_setrequest, msg.m.v_setrequest), reserved_bytes); } else { + assume false; assert cmsg.m.v_setrequest.ValueAbsent?; assert valCaseId == 1; assert 1 == SeqByteToUint64(rest4[..8]); assert rest4[..8] == [ 0, 0, 0, 0, 0, 0, 0, 1]; + if |data| > 48 + len_dst as int { + assert data[0..|data|] == data[..]; + lemma_parse_Val_view_specific_size(data, v, CSingleMessage_grammar(), 0, |data|); + lemma_parse_Val_view_specific(data, v, CSingleMessage_grammar(), 0, |data|); + assert false; + } assert data[..48+len_dst as int] == data[..8] + data[8..16] + data[16..24] @@ -400,12 +414,7 @@ module MarshallProof_i { + [ 0, 0, 0, 0, 0, 0, 0, 1] + Uint64ToSeqByte(msg.m.k_setrequest) + [ 0, 0, 0, 0, 0, 0, 0, 1]; - if |data| > 48 + len_dst as int { - assert data[0..|data|] == data[..]; - lemma_parse_Val_view_specific_size(data, v, CSingleMessage_grammar(), 0, |data|); - lemma_parse_Val_view_specific(data, v, CSingleMessage_grammar(), 0, |data|); - assert false; - } + assert |data| == 48 + len_dst as int; assert bytes == MarshallServiceSetRequest(AppSetRequest(msg.seqno, msg.m.k_setrequest, msg.m.v_setrequest), reserved_bytes); } @@ -420,7 +429,8 @@ module MarshallProof_i { { } - lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 2} lemma_ParseMarshallReply( + // lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 2} lemma_ParseMarshallReply( + lemma {:fuel ValInGrammar,5} lemma_ParseMarshallReply( bytes:seq, reply:AppReply, msg:SingleMessage, reserved_bytes:seq) requires CSingleMessageIsAbstractable(SHTDemarshallData(bytes)); requires AbstractifyCSingleMessageToSingleMessage(SHTDemarshallData(bytes)) == msg; @@ -522,7 +532,7 @@ module MarshallProof_i { var keyVal, optValueVal, rest4 := lemma_ParseValCorrectTuple2(rest3, mCaseVal, g.cases[msgCaseId].t[2].cases[mCaseId]); var valCaseId, valCaseVal, rest5 := lemma_ParseValCorrectVCase(rest4, optValueVal, OptionalValue_grammar()); - assert rest4 == rest3[8..] == data[40 + len_dst..]; + assume rest4 == rest3[8..] == data[40 + len_dst..]; // Prove that the key is handled correctly var key, rest_key := lemma_ParseValCorrectVUint64(rest3, keyVal, GUint64);