Repository navigation
Conversation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
All eight statements pass lake comparator --paranoid under the six kernels: the derivative matcher decides the grammar notation, parseHead reads exactly the heads of the grammar, the round trip, and framing decides the acceptance and framing rules. The one-off cross-check sends the test heads to Node's llhttp, Go's net/http and h11. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…thout a valid port RFC 9110 section 5.6.1.2 says a recipient must accept lists with empty elements, so chunked, and , chunked list the one coding chunked. The combined value of all Transfer-Encoding lines (section 5.2) is read. RFC 9110 section 9.3.6 says a server must reject a CONNECT that targets an empty or invalid port; here the target must be uri-host ":" port with a port from 1 to 65535. Proofs still open. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
framing_iff, framing_te_cl and framing_two_cl now hold for the new Spec.Accepts. lake comparator --paranoid accepts all 8 statements under all six kernels. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Tests: the oracle now has the CONNECT rule and the Transfer-Encoding list rule. The inputs add CONNECT ports and targets, Transfer-Encoding lists with empty elements and several lines, bad IPv4 tails in IPv6 literals, zone IDs, bare IPv6 hosts and an upper-case V in IPvFuture, with 118 fixed cases. 41 planted bugs: every one makes the tests fail except two that give the same answer on every input. The target counts now keep absolute-form only, authority-form only and both apart. Cross-check: Node and h11 are now judged on the head, as Go was. Real bodies are sent, chunked ones not empty. Each difference is filed under the feature whose change alone flips the other parser's verdict. Page: "this library refuses" replaces "a server must refuse"; HTAB, whitespace before a colon, the round trip and CVE-2023-25690 are corrected; the CONNECT and list rules are described, with a list of which refusals the RFCs require and which are this library's choice. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
RFC 9110 sections 4.2.1 and 4.2.2 say a recipient MUST reject an http or https URI with an empty host, and section 4.2.4 says a recipient SHOULD treat userinfo as an error. So a target whose scheme is http or https, in any case, must now be an http-URI or https-URI with a host that is not empty and no userinfo. A CONNECT target is a host and port, so CONNECT http:80 is still the host http. Five new vectors; the proofs of framing_iff and the vectors are still open. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
httpTargetOK_iff shows Head.httpTargetOK decides Spec.HttpTargetOK, with Grammar.httpTarget = Spec.httpTarget by rfl. framing_iff now handles the new else-if in Head.framing, and framing_te_cl and framing_two_cl take the extra conjunct of Spec.Accepts. head_vectors still ends with and_intros <;> decide +kernel. Before that it unfolds Head.framing and rewrites Head.httpTargetOK to a copy whose two schemes are lists of characters. With the string literals the nanoda checker ran out of stack on the http target vectors. lake comparator --paranoid accepts all 8 statements under all six kernels. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The oracle in tests/run_tests.py now has the rule of RFC 9110 sections 4.2.1, 4.2.2 and 4.2.4, written from the RFCs. If a target's scheme is http or https, in any case (RFC 3986 section 3.1), the target must have "//", an authority with no userinfo, and a host that is not empty. A CONNECT target is a host and a port, so the rule does not apply to it. The generators now make http and https targets in any case. Most have a host, and some have an empty host, no "//", userinfo or an empty port. CONNECT targets now include the hosts http and https. Other schemes, such as httpx and ws, are still made. The fixed cases have every new input of Spec.head_vectors and more examples. TEST-RESULTS.md counts how often the rule was reached. 300000 inputs, 0 failures. tests/planted_bugs.py plants 49 bugs: the 41 from earlier runs and 8 for the new rule. On 300000 inputs the tests catch 47. The other 2 are equivalent, and PLANTED-BUGS.md says why. bar.toml lists the script, and the README says what it found. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
This project now refuses an http or https target with no host and one with userinfo, so in tests/cross_check.py these are reasons to reject, not features this project accepts. "an http or https target with no host" covers a target with no "//" and one with an empty host. "an http or https target with userinfo" is new. A CONNECT target is still exempt. Rerun with the default seed and count, 5991 heads. Same verdict: Node 4246, Go 4654, h11 4561. Where both accept, the body lengths agree every time. All three accept a target with an empty host or with userinfo. Go and h11 also accept one with no "//". Node rejects those, as it rejects every scheme with no "//". Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
This library now refuses an http or https target with no authority, an empty host or userinfo, so the page no longer says it accepts http: and http:///a. SPEC.md states the rule in its accepting section. The empty host is a refusal RFC 9110 sections 4.2.1 and 4.2.2 require. Userinfo (section 4.2.4, SHOULD) and no authority, which is not an http-URI at all, are this library's choices. A CONNECT target is a host and port, so CONNECT http:80 names the host http. The claims tables for framing_iff and head_vectors follow Spec.lean. The cross-check section has the numbers of the new CROSS-CHECK.md: all three parsers accept an empty host and userinfo, and Go and h11 also accept a target with no "//". The tests paragraph has the counts of TEST-RESULTS.md for the rule, and the layout names planted_bugs.py and the three records. The module header of Http/Framing.lean and the docstring of Head.framing, the header of Spec/Defs.lean and the docstring of framing() in tests/run_tests.py now say this library where they said a server. Only comments and docstrings changed in those files. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
takeLine called itself and then put the octet on the front of the result, so the stack grew by one frame per octet of a line. A line of 16 MB aborted httphead check and serve with "Stack overflow detected". parseFields did the same once per field line, and 20,000,000 field lines aborted check. In serve, hexBytes in Main.lean did it once per octet. Each now keeps what it has read in an accumulator and calls itself last: takeLine is takeLineFrom [], parseFields is parseFieldsFrom [], and hexBytes is hexBytesFrom []. The answers are the same. The proofs now go through two equations, takeLine_cons in Proofs/Lines.lean and parseFields_step in Proofs/Fields.lean, which state the old recursion as theorems; the rest of each proof is unchanged. With this change, check prints length 0 for a 16 MB target, invalid for a 16 MB field value that ends in NUL, and length 0 for 30,000,000 field lines, and serve answers the 16 MB heads. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
In a Transfer-Encoding list, each SP after a comma made the derivative alt (alt ... y) y, one level deeper per octet, since mkAlt folded only alt a a. So the time to match grew with the square of the run: through httphead check, chunked, then n spaces, then a comma took 0.049 s for n = 1000, 0.665 s for 4000, 2.600 s for 8000 and 11.272 s for 16000. mkAlt now also folds alt (alt x y) y to alt x y. mkAlt_iff covers the new case. The same inputs now take 0.006 s, 0.014 s, 0.016 s and 0.010 s, and n = 262144 takes 0.259 s. Listing every derivative of each rule the code matches now ends, so each has finitely many: requestTarget 499, httpTarget 243, hostValue 229, authorityForm 229 and chunkedList 15. Before, chunkedList had no end. The header of Http/Match.lean says this, and that it was checked by running the matcher, not proved. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
RFC 9112 section 3.3 builds the target URI from the scheme, "://", the authority and the path. The authority is the CONNECT target, or else the Host value. So GET / with Host: :80 has the target URI http://:80/, and CONNECT :80 has http://:80. RFC 9110 sections 4.2.1 and 4.2.2 say a recipient must reject an http or https URI with an empty host. This library already refused that URI in absolute-form, and accepted it by these two routes. Now a Host value must be empty or Spec.hostNonEmpty [ ":" port ], the new Spec.hostField, and a CONNECT target must be Spec.hostNonEmpty ":" port. An empty Host value is still accepted: section 3.2 has a client send it when the target URI has no authority, and section 3.3 lets the server reject it or apply a default. Spec/Defs.lean says this, and its reason for exempting CONNECT from the http and https rule is now that a CONNECT target is in authority-form, which has no scheme, so CONNECT http:80 names the host http. The code mirrors the rule with Grammar.hostField and Grammar.connectTarget, and framing_iff carries over. head_vectors adds Host: :80, Host: : and CONNECT :80 as rejected and an empty Host as accepted. Its docstring now says an http or https target with no authority, an empty host or userinfo, as the pages do. httphead check now prints reject for Host: :80, Host: :, OPTIONS * with Host: :8080, and CONNECT :80 in HTTP/1.1 and HTTP/1.0. It still prints length 0 for an empty Host and for CONNECT http:80. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
decimal reads one digit at a time over a Nat, and each step costs time that grows with the number so far. So Head.framing took time that grows with the square of the digits. Timed in a probe exe that calls Head.framing on a parsed head, a Content-Length of 65,536 nines took 297 ms and one of 262,144 took 4,074 ms. A CONNECT port of the same lengths took 490 ms and 7,338 ms, since the port was converted twice. For CONNECT, portInRange drops the leading zeros and refuses more than five digits after them, which write 100000 or more, so it converts at most five digits. portInRange_iff proves it gives the spec's 1 <= Spec.decimal port <= 65535. For Content-Length, decimalFast reads the digits by halves: the number that hi ++ lo writes is decimal hi * 10 ^ |lo| + decimal lo, so the work is in a few multiplications of large numbers. Up to 18 digits are read one at a time. decimalFast_eq proves decimalFast = Spec.decimal, so framing_iff is unchanged. Now, in the same probe, Head.framing takes 16 ms, 282 ms and 1,238 ms on a Content-Length of 64 KB, 1 MB and 4 MB of nines, and 35 ms, 332 ms and 964 ms on a CONNECT port of those lengths, most of it in matching the target. decimalFast alone takes 8 ms, 189 ms and 1,119 ms; decimal took 274 ms on the 64 KB value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Main printed length N with toString, which finds one digit at a time, so it took time that grows with the square of the digits. Timed in a scratch exe on 10^k - 1, toString took 1,176 ms for 65,536 digits and 18,914 ms for 262,144. decimalText writes a number below 2^64 with toString, and splits a larger one into its high and low digits by dividing by a power of 10, then writes each part the same way, the low part padded with zeros. It gives the same text as toString: the same exe compared them, and the tool's output for 276 Content-Length values, from 1 to 10,000 digits with leading zeros, is the value without its leading zeros. It takes 7 ms, 47 ms, 312 ms and 1,419 ms for 65,536, 262,144, 1,048,576 and 4,194,304 digits. check also computes the framing once, not twice. Its output is the same byte for byte. httphead check on a head with a Content-Length of nines now takes 0.028 s for 64 KB, 0.613 s for 1 MB and 4.041 s for 4 MB. Before, it took 1.599 s for 64 KB and 25.715 s for 256 KB. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Spec.hostField is the Host rule, Spec.hostValue, without the values that have an empty host and a colon. Its docstring now names Spec.hostValue, which is otherwise no longer used. The Content-Length branch of Head.framing is back on one line, as it was before decimalFast. Neither change alters what the code does. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The oracle now refuses a Host value with an empty host before a colon, such as :80 or :, and a CONNECT target with an empty host, such as :443, as the code does since ed7ab1c. RFC 9112 section 3.3 builds the target URI from the Host value or the CONNECT target, and RFC 9110 sections 4.2.1 and 4.2.2 say a recipient must reject an http URI with an empty host. An empty Host value is still accepted. The oracle writes the rule another way than Spec.hostField: it matches Host = uri-host [ ":" port ] and then checks that the host it read is not empty, unless the whole value is. The generator now writes an empty Host value or one with an empty host before a colon for 5 in 100 Host values, besides the empty hosts that host() gives, and an empty host for 5 in 100 CONNECT targets. The fixed cases add the new inputs of Spec.head_vectors, Host: :80, Host: : and CONNECT :80, and a few more of each kind. TEST-RESULTS.md gets a line that counts the empty Host values and those with an empty host, and the CONNECT line counts the targets with an empty host apart. cross_check.py gives these refusals their own categories, so that features() still names a reason for every head this project refuses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The version rule is HTTP-version = HTTP-name "/" DIGIT "." DIGIT (RFC 9112 section 2.3), but the generator picked no version with major 9, and no fixed case had one. So a slip that put 9 outside the grammar, in the code and the spec together, passed every test. The generator now also picks HTTP/9.9 and HTTP/9.1, and the fixed cases have both. Each is read and then refused, since the major version is not 1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
IPvFuture is "v" 1*HEXDIG "." 1*( unreserved / sub-delims / ":" ), but host() always wrote at least one hex digit and one octet after the dot. Only a chance mutation reached [v.x] or [v1.], once each under the recorded seed, and not at all under some other seeds. host() now writes an IPvFuture with no hex digit for 1 in 10 of them, and one with nothing after the dot for another 1 in 10. The fixed cases add Host: [v.a], Host: [v1.] and GET http://[v1.]/, and TEST-RESULTS.md counts the inputs that hold such a literal. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The line on CONNECT targets that start with http: or https: said they name the host http or https, but some of them, such as http://a:80/ and http:/a, are not a host and port and name no host. It now gives the two counts apart, each with the number accepted. The line on absolute-form targets of another scheme counted only those that do not also fit the authority-form, so it left out targets such as x:443 and ws:80. It now counts every target of another scheme that fits absolute-form, with a method other than CONNECT, which reads such a target as a host and port. It gives those that fit absolute-form only and those that fit both apart. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
te_reason compared each list element whole with chunked, so it filed chunked;q=1 as a Transfer-Encoding whose last coding is not chunked, which is the RFC 9112 section 6.3 MUST. But a transfer-coding is a token with parameters after ";" (RFC 9110 section 10.1.4), so the last coding there is chunked. RFC 9112 section 7.1 says chunked has no parameters and "Their presence SHOULD be treated as an error". te_reason now drops the parameters before it compares the coding names, and files chunked alone with a parameter as "chunked with a parameter". On the first 6000 inputs, 6 heads have that category as their first reason to reject. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The heads are the first 6000 inputs of the differential tests, which now hold Host values and CONNECT targets with an empty host, HTTP/9.9 and HTTP/9.1, and IPvFuture with no hex digit or nothing after the dot. The refusals of an empty host have their own categories, and so does chunked with a parameter. All three parsers accept a Host value with an empty host, such as Host: :80 (Node 47 heads, Go 69, h11 77), and a CONNECT with an empty host (Node 17, Go 12, h11 9). Where both accept and the lengths can be compared, the body lengths still agree every time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Three faults found in review were missed by every test, since no input was long. The stack grew with the length of a line and overflowed at about 10 MB; a Content-Length or CONNECT port was converted in time that grows with the square of its digits; and the derivative of a Transfer-Encoding list grew by a level for each space after a comma. The tests now give six long inputs to httphead check and to httphead serve: a request line of 16 MB, a field value of 16 MB with a NUL at the end, a Content-Length of 1,000,000 digits, a CONNECT port of 1,000,000 nines, one of 1,000,000 zeros then 443, and a Transfer-Encoding value with 64 KB of spaces after a comma. Each answer must be the oracle's, and each run must end within 400, 150, 30, 30, 30 and 10 seconds. That is at least 20 times the longest each took here, over five runs on a machine with 4 cores and other work running: 17.7, 7.1, 1.1, 1.3, 1.2 and 0.07 seconds. The times varied by up to a factor of two between runs, so TEST-RESULTS.md records only the bounds and how many runs were right in time. The tool built at b113837 gets 10 of the 12 runs wrong: it aborts with a stack overflow on both 16 MB inputs, and does not finish the Content-Length, the port of nines or the Transfer-Encoding value in time. The oracle now writes the framing length from the digits without their leading zeros, since int() refuses a string of more than 4300 digits. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
zero-aska
requested changes
Oct 28, 2026
zero-aska
left a comment
zero-aska
left a comment
There was a problem hiding this comment.
This review covers head fd9f415, which is still the head. The PR has no other reviews yet.
The grammar in Spec/Rules.lean matches the ABNF of RFC 9112, RFC 9110 and RFC 3986 rule by rule, and the statements are tight. In Lean, we proved from the PR's own lemmas that any function meeting parseHead_iff, framing_iff or isMatch_iff equals the PR's. At fd9f415, lake build passes, lake comparator --paranoid accepts all 8 theorems, Main.lean calls the proved functions directly, and CI's fresh 300,000-input run has 0 failures.
Blocking
-
SPEC.md and README state the Host and CONNECT rules as they were before ed7ab1c. That commit made
Spec.HostOKusehostFieldandSpec.ConnectOKusehostNonEmpty, but SPEC.md and README.md were last changed at b113837. SPEC.md:63 refuses a Host value only if it "is noturi-host [ ":" port ]". SPEC.md:64 and README.md:50 and :65 require a CONNECT targeturi-host ":" port.:80fits both, since RFC 3986reg-namemay be empty. Yetprintf 'GET / HTTP/1.1\r\nHost: :80\r\n\r\n' | httphead checkprintsreject. So doHost: :andCONNECT :80, andhead_vectorsprovesnonefor all three (Spec.lean:131-132, 138). README.md:50's claim that framing works "exactly when this library accepts the request by the rules below" is therefore false for these inputs. SPEC.md:88 says every refusal is in one of its two lists, but this one is in neither. Fix:- State the real rules in SPEC.md:63-64 and README.md:50 and :65.
- Give the reason Spec/Defs.lean:158-173 already has: RFC 9112 section 3.3, then RFC 9110 section 4.2.1, "MUST reject it as invalid".
- Put the refusal in a list and say why. Section 3.3 also allows a configured default.
- Add the
Host:,Host: :80,Host: :andCONNECT :80vectors at README.md:53 and SPEC.md:140.
-
An empty host in authority-form is accepted for methods other than CONNECT.
printf 'GET :80 HTTP/1.1\r\nHost: a\r\n\r\n' | httphead checkprintslength 0, and so doesOPTIONS :443. RFC 9112 section 3.3 says "If the request-target is in authority-form, the target URI's authority component is the request-target", for any method. The target URI is thenhttp://:80, which RFC 9110 section 4.2.1 says a recipient "MUST reject it as invalid". Spec/Defs.lean:158-169 makes this argument but applies it only to Host and CONNECT. The README's method/target-form choice rests on rules for senders, so it does not cover this. The oracle'sframing()(tests/run_tests.py:300) shares the gap. Fix: inSpec.AcceptsandHead.framing, refuse a target whose first octet is:, which withinrequestTargetis exactly an empty authority-form host. AddGET :80andOPTIONS :vectors givingnone. -
A CONNECT gets a body, and the spec does not say so.
printf 'CONNECT a:443 HTTP/1.1\r\nHost: a\r\nContent-Length: 5\r\n\r\nhello' | httphead checkprintslength 5. WithTransfer-Encoding: chunkedit printschunked. That is the literal RFC 9112 section 6.3 result, and Go 1.24.7 agrees. The problem is that the choice is silent where parsers disagree: RFC 9110 section 9.3.6 says "A CONNECT request message does not have content", and Node 22.22.0 passes those 5 octets to the tunnel. README.md:6 says the framing follows section 9.3.6 "with the choices in SPEC.md", but neither SPEC.md,Spec.ConnectOKnorSpec.FramedAsaddresses CONNECT content. README.md:87 drops the 82 CONNECT heads from the length comparison instead of listing the difference. Fix: preferably refuse a CONNECT with Transfer-Encoding or a non-zero Content-Length, inSpec.ConnectOK,Head.connectOKandhead_vectors, quoting section 9.3.6. SPEC.md:64 already argues that a server need not accept CONNECT. Otherwise, state the 6.3 reading in SPEC.md and list the Node difference. -
tests/planted_bugs.pyfails at this head. Six of its 49 patterns are no longer in the code (bugs 2, 26-29 and 31); at 7e622c3 all 49 matched. For example, planted_bugs.py:65 looks forsome ([], rest'), but Http/Head.lean:52 now hassome (acc.reverse, rest'). The CONNECT plants look fordecimal (portOf h.target) ≤ 65535, which Http/Framing.lean:66 replaced withportInRange. The script stops at bug 2 with itssys.exit(planted_bugs.py:194-195) and never rewrites PLANTED-BUGS.md, so README.md:125's "catch 47 of them" describes older code. No plant covers the new logic:hostNonEmptyinhostFieldandconnectTarget,portInRange, anddecimalBy. Fix: retarget the six plants, add plants for the new logic, rerun, and commit PLANTED-BUGS.md.
Non-blocking
Transfer-Encoding: chunked;a=bprintsrejectbut is in neither list. RFC 9112 section 7.1 says: "Their presence SHOULD be treated as an error". Add it to "Refusals the RFCs allow".- An older script wrote tests/TEST-RESULTS.md at 7e622c3. Its line 10 says
fixed 173, while the script now has 188. Rerun and commit it. verified-bar.md:44 says counts belong in tests/ rather than on the page, so also move the counts at README.md:14, :87 and :125 and SPEC.md:150 there. - Plan #1 lists TE vectors with a tab and with a leading space, but
head_vectorshas neither (for example,Transfer-Encoding:\tchunkedgiveschunked). The plan also says HTTP/1.0 or 1.1, while SPEC.md:62 reads 1.2 to 1.9 as 1.1. Add the vectors, or update the plan. - bar.toml has
spec_authors = ["claude"], but Plan #1 says the PRs come fromahrazzle. List that account too, so check.py excludes it as a reviewer.
Not run by this review
tests/run_tests.py, refused by the session's permission system. The 300,000-input result is from CI job 122624742198 at fd9f415.tests/planted_bugs.py. Finding 4 comes from matching its patterns against the source and reading itsrun().tests/cross_check.py. Node and Go were probed by hand on the CONNECT andGET :80inputs only.- The approval lookup and branch protection: check.py ran here with
--offline, and CI reports items 1 and 7 as OPEN.
The PR is a draft. These four findings need fixing before the spec text can be approved.
Generated by Claude Code
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf
Addresses findings 2 and 3 of zero-aska's review of #3. - Head.framing now refuses a target that begins with `:`, which in a request-target is exactly an authority-form target with an empty host. RFC 9112 section 3.3 makes such a target the authority of the target URI for any method, and RFC 9110 section 4.2.1 says a recipient MUST reject an http URI with an empty host. Spec: Spec.AuthorityHostOK. - Head.framing refuses a CONNECT with Transfer-Encoding or a non-zero Content-Length: RFC 9110 section 9.3.6, "A CONNECT request message does not have content". Spec: Spec.ConnectNoContent. - The old function is Head.framingCore, and framingCore_iff is the old proof; framing_iff is proved from it. - head_vectors gains GET :80, OPTIONS :, CONNECT with Content-Length 5, with chunked, and with Content-Length 0, chunked after a tab and two spaces, and chunked;a=b. - The Python oracle applies both rules, and the fixed cases include the new vectors. Rerun: 300000 inputs, 0 failures. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf
Addresses finding 1 and the non-blocking points of zero-aska's review of #3. - SPEC.md and README.md now say a Host value must be empty or a host that is not empty with an optional port, with the reason (RFC 9112 section 3.3, RFC 9110 section 4.2.1), and list the refusal. - They describe the new authority-form and CONNECT content rules, and list them, with chunked;a=b (RFC 9112 section 7.1). - Counts move out of README.md and SPEC.md into tests/; the cross-check paragraph says its record predates the new rules. - lakefile.toml sets license = "Apache-2.0"; bar.toml lists ahrazzle and orda-aska as spec authors. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf
Addresses finding 4 of zero-aska's review of #3. - The six plants whose text was gone (bare CR, the four CONNECT port plants, CONNECT target form) now target takeLineFrom, portInRange and connectTarget as they are. - New plants: CONNECT leading zeros, the empty host in connectTarget (equivalent, since framing refuses every target that begins with `:`) and in hostField, the authority-form empty-host rule, and three for the CONNECT content rule. - Rerun on 300000 inputs: 53 of 56 caught; the other 3 are recorded as equivalent, with the reason. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf
orda-aska
marked this pull request as ready for review
October 29, 2026 22:05
Author
|
CI update: Generated by Claude Code |
zero-aska
requested changes
Oct 30, 2026
zero-aska
left a comment
zero-aska
left a comment
There was a problem hiding this comment.
Requesting changes: the four earlier findings are fixed, but python3 tests/cross_check.py now stops at its own first check, before it compares any parser.
This review covers head 94e0d79. The PR is marked ready for review.
Earlier findings
- Stale Host and CONNECT rule text: fixed.
- SPEC.md and README.md:50 and :65 now state
[ hostNonEmpty [ ":" port ] ], with the reason: RFC 9112 section 3.3, then RFC 9110 section 4.2.1. - SPEC.md lists the refusal under the refusals the RFCs require. It also says why an empty Host is still accepted.
- README.md:53 and SPEC.md name the
Host:,Host: :80,Host: :andCONNECT :80vectors.
- SPEC.md and README.md:50 and :65 now state
GET :80accepted: fixed.- CONNECT content: fixed, by refusing it.
- planted_bugs.py: fixed.
The earlier non-blocking points are all done.
What I ran on 94e0d79
lake buildwith Lean 4.35.0: passed, 32 jobs. The only warnings are the 8sorryin Spec.lean.check.py --offline --run-tests: items 2-6 PASS, andlake comparator --paranoidaccepts all 8 theorems. Item 1 is OPEN: there is no approval, and the spec hash is 17b764f2f3ef6f259d3e2b561dea826e9ec74f6f53bdc02a70611a40b536155a. Item 7 was skipped, since the run was offline.tests/run_tests.py, run by check.py: 300,000 inputs, 0 failures. The rewritten TEST-RESULTS.md is the committed one.- In Lean, against the built proofs: any
fwith∀ h fr, f h = some fr ↔ Spec.Accepts h frequalsHead.framing. So no wrong program meetsframing_iff. From it I also derived that a target that begins with:is always refused, and that a CONNECT is never framed chunked. Only the three standard axioms are used. - I read the diff since fd9f415 and the code, spec and docs against main. The claims match the statements.
Blocking
tests/cross_check.pyexits at 94e0d79.- With Node 22.22.0 and Go 1.24.7,
python3 tests/cross_check.pyprintsfeatures() does not match this project's verdict on b'connect :80 HTTP/1.1\r\nHost: a\r\n\r\n'and exits with 1. - The script imports the oracle from run_tests.py. That oracle now refuses a target that begins with
:, and a CONNECT with content. features()(tests/cross_check.py:346) has no reason for either refusal, so the check at lines 712-719 fails.- I ran that check alone over the script's 5991 heads. It finds 0 mismatches at fd9f415 and 43 at 94e0d79: 19 heads whose target begins with
:, and 24 CONNECT heads with content. - README.md:125 tells readers to run this script, and plan #1 lists the cross-checks among the tests.
- Fix: add both reasons to
features(). In a scratch copy, that alone brings the check to 0 mismatches. Then rerun the script and commit CROSS-CHECK.md, or keep the note at README.md:87.
- With Node 22.22.0 and Go 1.24.7,
Non-blocking
- The docstring of
Spec.framing_iff(Spec.lean:41-45) does not name the empty-host rule for authority-form targets or the CONNECT content rule. The docstring ofHead.framingCore(Http/Framing.lean) still reads as the full list of refusals. Both should be updated before approval. - No plant covers
decimalBy. A row for it in planted_bugs.py would close that gap. - Plan #1 still says HTTP/1.0 or 1.1, and that a chunked last coding gives chunked. Its "Current work" still calls this PR a draft. Updating it is for its author.
Open items
None of these holds the merge under MERGE-SOP.
- The spec approval (bar item 1) comes later, in its own PR.
- Under the mission#22 decision, the move to
Http.SpecandHttp.Proofscomes in a later PR of this repo. It changes the spec hash, so it should come before an approval. - No note asks for an owner decision.
Generated by Claude Code
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1. This is the first slice of the request-head and framing plan in #1.
This PR implements request-head parsing, RFC-derived target and field grammars, printing, and body framing. Eight challenge statements in
Spec.leanare proved inProofs/. They cover grammar acceptance, printing and parsing, and framing, including conflicting Content-Length and Transfer-Encoding. The PR does not read request bodies or implement a server.Changes since zero-aska's review of
fd9f415fd9f415was the original author's branch. I merged main into it, so the Apache-2.0LICENSEis now in the branch, and added fix commits on top. No history was rewritten.Host: :80,Host: :andCONNECT :80vectors are named on both pages.GET :80.Head.framingnow refuses a target that begins with:, for any method. In arequest-target, that is exactly an authority-form target with an empty host. The new spec definition isSpec.AuthorityHostOK, part ofSpec.Accepts. The old function is nowHead.framingCore, with its proof asframingCore_iff, andframing_iffis proved from it.head_vectorsgainsGET :80andOPTIONS :, both refused. The Python oracle applies the same rule.CONNECTwith Transfer-Encoding, or a Content-Length that is not 0, is refused, per RFC 9110 section 9.3.6, "A CONNECT request message does not have content". The new definition isSpec.ConnectNoContent. The vectors areContent-Length: 5andTransfer-Encoding: chunked(refused) andContent-Length: 0(accepted). SPEC.md lists the refusal and the Go/Node difference it removes.hostNonEmptyinhostFieldandconnectTarget,portInRange(leading zeros), the authority-form rule, and the CONNECT content rule.connectTargetis equivalent now, because the authority-form rule refuses every target that begins with:.tests/PLANTED-BUGS.mdis regenerated.Non-blocking points:
chunked;a=bis in "Refusals the RFCs allow" (RFC 9112 section 7.1) and inhead_vectors.head_vectorsnow hasTransfer-Encoding:\tchunkedandTransfer-Encoding: chunked, both chunked.tests/TEST-RESULTS.mdis regenerated: 300,000 inputs, 0 failures.tests/. The cross-check paragraph now says its record predates the two new rules;tests/cross_check.pywas not rerun.bar.tomlspec_authorsnow listsclaude,ahrazzleandorda-aska.lakefile.tomlsetslicense = "Apache-2.0".Checked on head
94e0d79lake buildpasses on Lean 4.35.0 (32 jobs).#print axiomsgives onlypropext,Classical.choiceandQuot.soundfor the framing theorems andhead_vectors.python3 tests/run_tests.py: 300,000 inputs, 0 failures.python3 tests/planted_bugs.py: 53 of 56 caught, 3 equivalent.bar / bar, which runslake comparator --paranoidsandboxed, passed onb022dfc, which has the same Lean code.Still open:
Spec/Proofs), which mission#22 handles separately.🤖 Generated with Claude Code
https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf