dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.
dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.
dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.