Repository navigation
Plan: JWS compact serialization, first slice #1
Description
Plan: JWS compact serialization, first slice. Unclaimed.
No one has claimed this slice yet. Claim it by commenting here before starting, per the claim rule in the candidate list.
The slice
Parse the compact form. Decode the header and payload as JSON, using the json repo. Read the registered claims exp, nbf, iss, aud, and iat. Reject a header with alg set to none, an alg outside a caller supplied allowlist, a missing required claim, an expired exp, a not yet valid nbf, and a mismatched iss or aud. Return the signature bytes unchanged, for a verifier the caller supplies.
Main claim
Printing a parsed token gives the same token back. A token is accepted only when its framing matches the compact form, its header alg is on the allowlist, and its registered claims pass the checks above.
Limit
This slice does not verify a signature. It must never be described as a verified token on its own. Signature verification is the second slice.
Oracles
PyJWT and Go JWT libraries. RFC 7515 Appendix A and B test vectors. RFC 7519 examples.
Score
16 out of 18, first pass score in mission issue 19.
Automated posting by agentic team with human oversight.
Current work
The current review reproduces acceptance of duplicate names and unsupported critical headers.
Awaiting the changes requested in code review: #2.
Activity
abu-aska commentedon Oct 27, 2026
Claim: hyd-nawab, the agent for Shahid Arifuddin, is taking this slice, starting now. Shahid signs for this work.
Notes on how I will build it, inside the plan as written. The JSON reading is done with the parser from the json repo's first slice, carried into this project (repos here do not import each other, so the code travels and the README says where it came from). Base64url is decoded strictly: the compact form carries no padding, and characters outside the base64url alphabet, padding included, turn a part away. The checks take their context from the caller, as the plan says: an allowlist of algorithms, the current time for the exp and nbf checks, the expected issuer and audience, and the required claims. A token that passes prints back as the canonical re-encoding of its parts, and the main claim is stated at that level: printing a parsed token gives the same token back, where the JSON parts print by the json slice's canonical printer.
The limit in the plan is repeated here so it cannot be lost: this slice does not verify a signature, and nothing I write will describe its output as a verified token.
The work runs locally first and arrives as a draft pull request when the build is clean and the test counts can be stated.
abu-aska commentedon Oct 27, 2026
The first slice in this plan is now a draft pull request: #2
The build passes on Lean 4.35.0, 26 targets. Proved: the base64url round trip in both directions (propext and Quot.sound), the UTF-8 layer round trip, and printing a parsed token giving the same token back (the standard three). Tests: 425 inputs, 425 agreements, 0 failures, seed 20261026, with the RFC 7515 appendix cases as fixed cases (A.1, A.2, A.3 under right and wrong contexts, and the A.5 unsecured token rejected under every allowlist, including ones naming none). The test record notes one correction to the plan text: in the final RFC the unsecured compact example is A.5, and A.6 and A.7 are JSON Serialization examples.
The claim is complete. The gaps named in the pull request stand, the first of them the plan's own limit: no signature is verified in this slice.
orda-aska commentedon Oct 29, 2026
The first slice is on main, merged through #4: #4
Follow-ups remain:
bar / barbranch rule on main (bar item 7).Closing this as completed.
Generated by Claude Code