forked from microsoft/Ironclad
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
224 additions
and
208 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
128 changes: 64 additions & 64 deletions
128
ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<EndPoint, seq<byte>>) | ||
| { | ||
| step.LEnvStepHostIos? ==> forall io{:trigger io in step.ios}{:trigger ValidPhysicalIo(io)} :: io in step.ios ==> ValidPhysicalIo(io) | ||
| } | ||
| // predicate ValidPhysicalEnvironmentStep(step:LEnvStep<EndPoint, seq<byte>>) | ||
| // { | ||
| // 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<EndPoint,seq<byte>>, | ||
| servers:map<EndPoint,H_s.HostState> | ||
| ) | ||
| // datatype DS_State = DS_State( | ||
| // config:H_s.ConcreteConfiguration, | ||
| // environment:LEnvironment<EndPoint,seq<byte>>, | ||
| // servers:map<EndPoint,H_s.HostState> | ||
| // ) | ||
|
|
||
| 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<LIoOp<EndPoint,seq<byte>>>) | ||
| 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<LIoOp<EndPoint,seq<byte>>>) | ||
| // 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<SpecState>, 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<SpecState>, 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])) | ||
| // // } | ||
|
|
||
| } | ||
| // } | ||
|
|
124 changes: 63 additions & 61 deletions
124
ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<LIoOp<EndPoint, seq<byte>>>) | ||
| // reads * | ||
| // predicate HostInit(host_state:HostState, config:ConcreteConfiguration, id:EndPoint, repr: set<object>) | ||
| // // reads * | ||
| // reads repr | ||
|
|
||
| predicate ConcreteConfigInit(config:ConcreteConfiguration) | ||
| function ConcreteConfigToServers(config:ConcreteConfiguration) : set<EndPoint> | ||
| // predicate HostNext(host_state:HostState, host_state':HostState, ios:seq<LIoOp<EndPoint, seq<byte>>>) | ||
| // // reads * | ||
|
|
||
| predicate HostStateInvariants(host_state:HostState, env:HostEnvironment) | ||
| // reads * | ||
| // predicate ConcreteConfigInit(config:ConcreteConfiguration) | ||
| // function ConcreteConfigToServers(config:ConcreteConfiguration) : set<EndPoint> | ||
|
|
||
| function ParseCommandLineConfiguration(args:seq<seq<byte>>) : ConcreteConfiguration | ||
| // predicate HostStateInvariants(host_state:HostState, env:HostEnvironment) | ||
| // // reads * | ||
|
|
||
| predicate ArbitraryObject(o:object) { true } | ||
| // function ParseCommandLineConfiguration(args:seq<seq<byte>>) : ConcreteConfiguration | ||
|
|
||
| method HostInitImpl(ghost env:HostEnvironment, netc:NetClient, args:seq<seq<byte>>) 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<seq<byte>>) 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<NetEvent>, | ||
| ghost clocks:seq<NetEvent>, | ||
| ghost sends:seq<NetEvent>, | ||
| ghost ios:seq<LIoOp<EndPoint, seq<byte>>> | ||
| ) | ||
| 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<NetEvent>, | ||
| // ghost clocks:seq<NetEvent>, | ||
| // ghost sends:seq<NetEvent>, | ||
| // ghost ios:seq<LIoOp<EndPoint, seq<byte>>> | ||
| // ) | ||
| // 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 | ||
|
|
||
| // } |
Oops, something went wrong.