at main
2 folders
20 files
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: describe the client from RFC 2131 figure 5, then diff
The client's rules lived in the reducer that executes them, so the only
way to ask what RFC 2131 says about a phase and an event was to read the
code that answers it. Client_control is that table read from the
specification instead: seven phases against fourteen events, an answer
in every one of the 98 cells, and the sentence of RFC 2131 it comes from
beside it. 37 cells are arrows and the other 61 are refusals that say
which question the specification did not answer there and why there was
none to answer -- a deadline this phase did not arm, a reply belonging
to another exchange, a check on an address the client is already using.
Two readings of figure 5 are made once and used throughout. A discard
the figure draws is an arrow and a discard the prose states is a
refusal: "DHCPOFFER/Collect replies" on SELECTING, "DHCPOFFER/Discard"
on REQUESTING and "DHCPOFFER, DHCPACK, DHCPNAK/Discard" on BOUND enter
the phase they are already in, while s.4.4.1's "Any arriving DHCPACK
messages must be silently discarded" refuses. Both leave the phase
alone; the difference is whether the specification considered the cell.
And INIT-REBOOT is folded into INIT, because the figure draws it as a
second start state whose only arrow sends the DHCPREQUEST of s.4.4.2,
exactly as INIT's only arrow sends the DHCPDISCOVER of s.4.4.1.
test_client_control drives every cell through the reducer's own entry
points and compares two things: the phase the client lands in, and what
it answered. The answer is compared and not just the phase because
three cells differ from their neighbours in nothing else -- a DHCPACK
that binds a lease against a DHCPOFFER that is discarded, a spent budget
that sends nothing against a DHCPDECLINE that sends, and a client that
gives up, which from outside looks exactly like a refusal. Figure 5
draws no arrow anywhere that stops a client, so a failure is what tells
those two apart, and a pair diff would have reported all three clean.
Five cells disagree and all five are pinned with the text that decides
them. They are one habit: the reducer ends the exchange where RFC 2131
goes on. An offer carrying no server identifier fails the exchange
where s.4.4.1 has the client go on collecting -- and any host on the
broadcast domain can send one. A spent retransmission budget fails
where s.3.1 step 5 reverts to INIT and begins again. And in RENEWING
and REBINDING a spent budget fails where s.4.4.5 has no count to spend,
the schedule there ending at T2 and at the lease expiry. The fixes
follow, one commit each, and retire the pins.
dhcp: pin table 5's zero flags field on a DHCPDECLINE
RFC 2131 table 5, the DHCPDECLINE/DHCPRELEASE column, sets 'flags' to 0.
The client built its DHCPDECLINE through the same helper as its DISCOVER
and REQUEST, which defaults to the broadcast flag, so every decline asked
for a broadcast reply to a message no server answers. s.4.4.4's "the
client broadcasts DHCPDECLINE messages" is the IP destination and not
this bit; the DHCPRELEASE already cleared it.
The reducer's line rode in with the previous commit's pathspec; this is
the test that pins it, and with it the rest of table 5's decline column:
ciaddr 0, the requested-IP option, the server identifier, and no
parameter request list.
Found by reading table 5 rather than the reducer. The header field is
below the control table's alphabet, so the description could not see it,
and the description/reducer diff reported the cell clean throughout.
dhcp: describe the client from RFC 2131 figure 5, then diff
The client's rules lived in the reducer that executes them, so the only
way to ask what RFC 2131 says about a phase and an event was to read the
code that answers it. Client_control is that table read from the
specification instead: seven phases against fourteen events, an answer
in every one of the 98 cells, and the sentence of RFC 2131 it comes from
beside it. 37 cells are arrows and the other 61 are refusals that say
which question the specification did not answer there and why there was
none to answer -- a deadline this phase did not arm, a reply belonging
to another exchange, a check on an address the client is already using.
Two readings of figure 5 are made once and used throughout. A discard
the figure draws is an arrow and a discard the prose states is a
refusal: "DHCPOFFER/Collect replies" on SELECTING, "DHCPOFFER/Discard"
on REQUESTING and "DHCPOFFER, DHCPACK, DHCPNAK/Discard" on BOUND enter
the phase they are already in, while s.4.4.1's "Any arriving DHCPACK
messages must be silently discarded" refuses. Both leave the phase
alone; the difference is whether the specification considered the cell.
And INIT-REBOOT is folded into INIT, because the figure draws it as a
second start state whose only arrow sends the DHCPREQUEST of s.4.4.2,
exactly as INIT's only arrow sends the DHCPDISCOVER of s.4.4.1.
test_client_control drives every cell through the reducer's own entry
points and compares two things: the phase the client lands in, and what
it answered. The answer is compared and not just the phase because
three cells differ from their neighbours in nothing else -- a DHCPACK
that binds a lease against a DHCPOFFER that is discarded, a spent budget
that sends nothing against a DHCPDECLINE that sends, and a client that
gives up, which from outside looks exactly like a refusal. Figure 5
draws no arrow anywhere that stops a client, so a failure is what tells
those two apart, and a pair diff would have reported all three clean.
Five cells disagree and all five are pinned with the text that decides
them. They are one habit: the reducer ends the exchange where RFC 2131
goes on. An offer carrying no server identifier fails the exchange
where s.4.4.1 has the client go on collecting -- and any host on the
broadcast domain can send one. A spent retransmission budget fails
where s.3.1 step 5 reverts to INIT and begins again. And in RENEWING
and REBINDING a spent budget fails where s.4.4.5 has no count to spend,
the schedule there ending at T2 and at the lease expiry. The fixes
follow, one commit each, and retire the pins.
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.
hex: split the hex codec out of ascii into nox-hex
ascii conflated two concerns: ASCII charset predicates (is_digit,
is_hex_digit, hex_value, hex_char, is_printable) and a full RFC 4648
base16 codec (Ascii.Hex) whose bytesrw stream filters dragged bytesrw
into every consumer that only wanted a char predicate.
The codec now lives in its own package, nox-hex (module Hex), with the
ohex-derived implementation, the unit/fuzz suites and the throughput
bench moved along. ascii keeps the charset predicates, gains the
documented unboxed hex_value_int the codec hot loop uses, and loses
the bytesrw dependency. The nox- prefix avoids the existing community
hex package on opam.
All ~45 consuming packages migrate from Ascii.Hex to Hex, with dune
stanzas and opam metadata updated; stanzas and opam packages whose
only ascii use was the codec drop the ascii dependency. The duplicated
of_hex helpers in the bytesrw-* test suites (dupfind cluster 3) now
alias Hex.decode.