at main
3 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.
ocaml-dhcp: compare pool addresses as the unsigned numbers they are
The lease pool ordered the int32 behind each address, which ranks every address from 128.0.0.0 up below 0.0.0.1. That refused 10.0.0.1 .. 192.168.1.100, a valid pool, and admitted 192.168.1.1 .. 10.0.0.1, which is not a range: the reversed pool sized itself at 1230503681 addresses and handed out 21.253.86.249, an address in no configured network. Ordering with Ipaddr.V4.compare, the unsigned comparison the lease database's address map is already keyed on, refuses a reversed pool and serves one that crosses 128.0.0.0.
The number of addresses in a range was read as a signed int32 as well, so a pool wider than 2^31 counted as a negative number and the fallback probe ended before its first step: a client whose hint address was already taken got nothing while the pool still held billions of free addresses. Wire.UInt32 reads the same four bytes without a sign.
The server's range membership carried the same comparison. A pool crossing 128.0.0.0 contained no address at all there, so no requested address was ever granted from it, and a static host address inside such a pool passed the configuration check that keeps fixed and dynamic addresses apart.
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.
ocaml-dhcp: compare pool addresses as the unsigned numbers they are
The lease pool ordered the int32 behind each address, which ranks every address from 128.0.0.0 up below 0.0.0.1. That refused 10.0.0.1 .. 192.168.1.100, a valid pool, and admitted 192.168.1.1 .. 10.0.0.1, which is not a range: the reversed pool sized itself at 1230503681 addresses and handed out 21.253.86.249, an address in no configured network. Ordering with Ipaddr.V4.compare, the unsigned comparison the lease database's address map is already keyed on, refuses a reversed pool and serves one that crosses 128.0.0.0.
The number of addresses in a range was read as a signed int32 as well, so a pool wider than 2^31 counted as a negative number and the fallback probe ended before its first step: a client whose hint address was already taken got nothing while the pool still held billions of free addresses. Wire.UInt32 reads the same four bytes without a sign.
The server's range membership carried the same comparison. A pool crossing 128.0.0.0 contained no address at all there, so no requested address was ever granted from it, and a static host address inside such a pool passed the configuration check that keeps fixed and dynamic addresses apart.