Formal Verification Experiment - #49
Open
ulfjack wants to merge 26 commits into
Open
Conversation
Fetch Lean 4.12.0 via http_archive; add lean_library/lean_test rules and a verification/ tree proving 1+1 executes to 2 through the JVM bytecode semantics. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Add java_verification_test: a macro that compiles a java_library, runs the jvmlean generator over its bytecode to emit Lean obligations, and checks + axiom-audits them via lean_test. `bazel test //verification:chunk` proves the RFC 9112 chunk-size parser's overflow guard makes 32-bit int overflow unreachable, straight from Chunk.java with no hand-transcription. Raise tool_java_language_version to 17 so the generator (an exec-config tool) compiles with Java 12+ APIs. Co-Authored-By: Claude Opus 4.8 <[email protected]>
digitVal/valOf/hexValF are RFC 9112 domain specs, not JVM machinery, so they don't belong in Jvm/Spec.lean. Move them to ChunkedEncodingSpec.lean (namespace ChunkedEncoding) and make the generator's spec import/open a --specs flag, so Jvm/ is purely the trusted machine and the generator carries no domain knowledge. Co-Authored-By: Claude Opus 4.8 <[email protected]>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
|
|
||
| private void out(String s) { | ||
| sb.append(s).append('\n'); | ||
| line += s.chars().filter(c -> c == '\n').count() + 1; |
The generated Lean obligations lived only in bazel-bin, invisible to readers and PR review — yet that file holds the theorem statements and the spliced spec strings. Commit it under verification/Generated/, have lean_test prove the checked-in file directly, and add a <name>_golden diff test that fails if it drifts from what the generator emits. The generator's fresh output moves to a _generated/ build path so both coexist in the diff test's runfiles. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Annotate Chunk.hexVal with its contract (ret = hexValF c) and prove it through the pipeline: 15 obligations (the short-circuit && expands to 15 paths), all closed, audit clean. This turns the "Chunk.hexVal = hexValF" entry in calls.map from an assumed fact into a machine-checked one, so parseHexSize no longer rests on a hand-waved lemma. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Introduce a @returns(expr) method annotation as the single source of truth for a method's postcondition. The generator now: - reads it from the class file and, for each `return <local>;`, synthesises the ensure obligation `ret = expr` (no more per-return Verify.ensure calls); - builds the call-site contract map from these annotations, eta-reducing `hexValF c` to `hexValF`, so calls.map is deleted and parseHexSize's obligations stay byte-identical. Annotate Chunk.hexVal with @returns("hexValF c") and drop its Verify.ensure calls and calls.map. hexVal's 15 obligations are re-proved against the synthetic cut points; parseHexSize is unchanged. Co-Authored-By: Claude Opus 4.8 <[email protected]>
The `specs = ["ChunkedEncodingSpec=ChunkedEncoding"]` in BUILD was a hand-written declaration, redundant with deps and disconnected from the @returns strings that actually use the names. Replace it with a class-level @ImportLeanPackage annotation read from the class file: the generator emits `import`/`open` for each named module, so the spec's Lean dependencies live in the Java source. Unify module and namespace by renaming ChunkedEncodingSpec.lean -> ChunkedEncoding.lean, so the single annotation string drives both import and open. BUILD keeps only the genuine build edge (the lean_library dep); the --specs flag is gone. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Replace the opening Verify.requires("...") call with a @precondition method
annotation, synthesised into the entry cut point by the generator. It is
optional: a method with neither Verify.requires nor @precondition is verified
under True, which is sound (a missing assumption only makes proofs harder). So
hexVal, whose precondition was "True", drops it entirely and is now free of any
Verify.* calls.
Removing the requires call shortens the bytecode, shifting every obligation and
invariant offset by 5; goldens are regenerated and the proofs remapped to the new
inv_<offset> names (tactics unchanged).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Obligations and invariants were named by bytecode offset (obl_5_38_0, inv_43), so any edit that shifted offsets renamed everything. Name cut points by kind and source order instead -- pre, loop0, loop1..., ret0, ret1... -- so obligations are obl_pre_loop0_0, obl_loop0_ret1_0, etc., stable across offset shifts. Offsets stay in the comments. Proofs remapped mechanically; tactics unchanged. Co-Authored-By: Claude Opus 4.8 <[email protected]>
parseSpec is the total specification of a chunk-size parse: the hex value of a non-empty all-HEXDIG field that fits in int32, else -1 (empty, non-hex, or overflow). Prove the valOf facts the error paths will need: nonnegativity, sticky-none, monotonicity (valOf_ge), and the two corollaries parseSpec_none / parseSpec_overflow. Imports Jvm.Semantics for MAXI; not yet used by parseHexSize. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Switch parseHexSize to a single postcondition, ret = parseSpec b off len, that characterizes the return for every input: the hex value of a non-empty all-HEXDIG field that fits in int32, else -1. This replaces the old vacuous `ret = -1` ensures (which said nothing about why -1) with a real contract. Refactor to a single return (one @returns cut point) and reject the empty field per RFC 1*HEXDIG. The two error-path obligations now carry real content, proving parseSpec = -1 from the invariant via parseSpec_none (non-hex byte) and parseSpec_overflow (prefix exceeds MAXI). Audit clean. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Restructure hexVal as an if/else-if chain assigning one `r`, returned once, instead of four early returns. The @returns contract now has a single ret0 cut point (was ret0..ret3); the 15 short-circuit paths all target it. Proofs remap to obl_pre_ret0_0..14, classified by branch (c-48 / c-87 / c-55 / -1) via their path conditions; tactics unchanged. Audit clean. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Replace State's separate (arr : Nat → Int, alen : Nat) with a single arr : Arr, where Arr bundles the index function `get` and the length `len`. A CoeFun makes `a i` mean `a.get i`, so indexing still reads naturally, and Arr.length exposes the length to specs as an Int. baload/arraylength bounds-check against s.arr.len. Specs can now say `b.length` instead of the free-floating `alen`: the length travels with the array. The prelude binds the byte-array parameter as `b : Arr` and no longer emits a standalone `alen`. valOf/parseSpec take an Arr. This is the first step toward supporting more than one array. Co-Authored-By: Claude Opus 4.8 <[email protected]>
A JVM array length is a non-negative int, so it never exceeds MAXI. Carry that as a field of Arr (len_le : len ≤ 2147483647), so b.length ≤ MAXI is a theorem about every array (Arr.length_le) rather than a precondition callers must state. Drop b.length ≤ MAXI from parseHexSize's @precondition and loop invariant; the proofs that needed it now derive it from s.arr.length_le. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Verify and the @Precondition/@Returns/@ImportLeanPackage annotations move from the default package to de.ofahrt.catfish.verify, exposed as the //verification:verify java_library. They are CLASS-retained / compile-only, so real annotated code can depend on them at no runtime cost -- the point being to make this usable on actual Catfish methods, not just the default-package example. The generator matches the fully-qualified annotation descriptors and the packaged Verify owner. Chunk imports the annotations; obligations are unchanged (only the source-line comments shifted for the added imports). Co-Authored-By: Claude Opus 4.8 <[email protected]>
Relocate the de.ofahrt.catfish.verify package (Verify + the @Precondition/ @Returns/@ImportLeanPackage annotations) from verification/java/ into the production tree at java/de/ofahrt/catfish/verify, with its own BUILD following the repo's package convention. Production Catfish code can now depend on //java/de/ofahrt/catfish/verify like any other package; chunk_java does the same. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Add natural-return support to the generator: `return <expr>;` (value on the operand stack, not a bare local) becomes an ensure cut point at the ireturn with a postcondition over the stack top (s.stk = [expr]) -- what real methods need. Sanitise the Lean namespace to the simple class name for packaged subjects. Annotate de.ofahrt.catfish.http.ChunkedBodyState.hexValue with @precondition("digitVal c ≠ none") and @returns("hexValF c"); all 7 obligations proved. The precondition is load-bearing -- the else branch (c-'A'+10) is only correct for A-F, and that branch's proof uses the precondition to pin c to [A-F]. Read the subject library in a coverage-free configuration (attribute transition): under `bazel coverage` a //java/... lib is JaCoCo-instrumented, which the bytecode generator cannot parse. Also remove the now-integrated upload/files.zip. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Add isHexDigitF (HEXDIG membership as 0/1) and isHexDigitF_eq (range-union form) to ChunkedEncoding, and verify the real sibling helper isHexDigit against @returns("isHexDigitF c") -- a boolean method, so the value is the stack top and the postcondition ties the boolean result to digitVal. All 15 paths proved. Note: the state machine itself (advance) is out of scope for the current model -- it is an instance method over mutable object fields (an enum State, three longs), a switch, and a Sink callback, none of which the one-array/int semantics supports. isHexDigit and hexValue are its verifiable pure helpers. Co-Authored-By: Claude Opus 4.8 <[email protected]>
A reference decoder for RFC 9112 §7.1 chunked transfer-coding as a byte-driven state machine: St (sizeStart/size/sizeLF/data/dataCR/dataLF/done/error) with the counter carried in the constructors that use it, chunkStep as the transition, and decode = foldl. Chunk-ext and the trailer section are elided for now. Faithful to the grammar: chunk-size is 1*HEXDIG with no digit cap (the code's 15-digit limit is an implementation defense, not RFC); sizeStart-vs-size enforces 1* without a boolean. The value ≤ MAXI rejection is Catfish recipient policy. Named chunkStep (not step) to avoid clashing with Jvm.step under `open`. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Add ChunkedRefinement.lean: a design-level proof that the real advance
control flow refines the St state machine, one input byte at a time.
- ClassState mirrors advance's instance fields (enum state +
currentChunkSize / chunkSizeDigits / chunkDataLeft).
- α maps those fields onto St (SIZE+digits=0 -> sizeStart, SIZE+digits>0
-> size, SIZE_CR -> sizeLF, DATA -> data, ...).
- advanceStep transcribes advance's core per-byte transition; Wf is the
field-consistency invariant it needs (digits=0 -> size=0).
- advanceStep_refines: alpha (advanceStep cs b) = chunkStep (alpha cs) b.
- advanceStep_wf: Wf is preserved.
- foldl_advanceStep_refines / advance_refines_decode: advance is a fold,
so from the initial state it computes exactly `decode`.
This verifies the design (field layout + transitions implement the spec),
not the JVM bytecode of advance (that needs object fields, long, switch,
and the Sink in the semantics). Chunk-ext, the trailer section, and the
15-digit cap are elided to match the St spec. Wired in as a lean_test so
the axiom audit fails the build on any sorry.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
ChunkedEncoding.lean is a domain spec of what chunked encoding *is*; it
should not reach into the machine model. Drop `import Jvm.Semantics` and
the two things that leaked in:
- the byte source: valOf/parseSpec now take `b : Nat → Int` instead of
`Jvm.Arr`. A Jvm.Arr coerces to Nat → Int (CoeFun), so the obligation
passes `s.arr` unchanged.
- the size cap: parseSpec/chunkStep now take a `maxLen : Int` parameter
(the restricted spec) rather than hardcoding Jvm.MAXI. The RFC has no
cap; it is the recipient's policy. The obligation supplies MAXI, via
@returns("parseSpec MAXI b off.toNat len.toNat") in Chunk.java.
chunkStep now applies the cap on the first digit too (matching Catfish's
per-digit guard), which also removes the digitVal_range/if_pos hack from
the refinement's first-digit case. The parseHexSize hand-proofs are
unchanged: maxLen is implicit in parseSpec_none/parseSpec_overflow and
unifies to MAXI. chunked_encoding no longer depends on :semantics.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Chunk.java was the initial synthetic demo of the pipeline (a standalone RFC 9112 chunk-size parser). The real Catfish subject is now ChunkedBodyState (hexValue/isHexDigit verified, advance modelled by the state machine + refinement), so the demo is redundant. Removes Chunk.java, its obligations/proofs/goldens, and the chunk / chunk_hexval / chunk_java BUILD targets. Also drops the now-orphaned valOf/parseSpec spec and its lemmas from ChunkedEncoding.lean -- they existed only to specify parseHexSize. The reusable HEXDIG primitives (digitVal, hexValF, isHexDigitF) and the framing state machine stay. Co-Authored-By: Claude Opus 4.8 <[email protected]>
Extend the St state machine past the last-chunk into the trailer section:
trailer-section = *( field-line CRLF )
then the terminal CRLF that ends the message. A zero-size chunk now goes
to `trailerStart` (not straight to `done`), field-lines are consumed as
opaque content (trailerLine/trailerLineCR), and `done` is reached only on
the terminal CRLF. Pinning the terminal to an exact CRLF is what closes
the request-smuggling surface in the spec, rather than treating the
zero-size chunk as the end.
ChunkedRefinement mirrors this: CState/advanceStep/α gain the four
TRAILER* states, so the one-byte simulation and the fold now cover trailer
framing too. Elisions vs the real advance shrink to chunk-ext, the
15-digit cap, and the trailer-section DoS byte-bound (all recipient policy
or resource limits, not framing grammar).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Extend the trusted machine model with 64-bit `long` support, the next
capability advance needs (currentChunkSize/chunkDataLeft/decodedByteCount
are longs):
- wrap64 (64-bit two's-complement) + wrap64_id/wrap64_id' lemmas.
- opcodes ladd/lsub/lmul, lcmp (pushes -1/0/1), and the i2l/l2i
conversions. i2l preserves the value; l2i keeps the low 32 bits.
Longs stay one operand-stack/local slot here rather than the JVMS two:
values are untyped Ints, so lload/lstore/lconst/ldc2_w reuse
iload/istore/push and only the width-specific ops are new. The generator
maps real (two-slot) long bytecode onto these; the reserved second slot is
simply never referenced by another variable.
Examples/LongArith.lean smoke-tests i2l/lmul/lcmp (a 64-bit product that
would overflow int, matching advance's overflow guard) and ladd/lsub,
executed through run/step with a clean-axiom audit.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Demonstrate the target shape for a join-aware VCG. `sign(x) = x>0 ? 1 : -1`
compiles to a diamond whose arms rejoin at the single ireturn; the returned
value there is a phi node. The path-enumerating VCG would emit one
obligation per arm -- merging at the join yields ONE, whose postcondition
is the phi expanded by its branch condition:
s'.stk = [if x > 0 then 1 else -1]
The proof is the uniform recipe validated for the full isHexDigit merge
(one obligation, clean axioms, ~7s): by_cases on each branch predicate
fixes the guards so `run` reduces with no internal fork, then split <;>
omega discharges the guarded result. This is what the generator will emit
per merged obligation, replacing the 15-way (isHexDigit) / 7-way
(hexValue) path fan-out.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
The path-enumerating VCG emitted one obligation per acyclic path between cut points, so short-circuit && / || exploded: isHexDigit -> 15, hexValue -> 7. A loop-free @returns method has a single postcondition; merging at the join (the returns) collapses it to ONE obligation. Generator (Vcg/Emit): - merged mode = loop-free (no back edges) + @returns + no explicit Verify.invariant/ensure. It skips the per-return cut points and emits one obligation `obl_pre_post`: from the entry, run to halt (N = longest path), conclude the shared postcondition `s.stk = [<@returns>]`. The per-path model is untouched for everything else (future loops). - the branch predicates (phi guards) are collected and listed in a comment for the proof's by_cases. Proof shape (uniform, per the sign example): by_cases on each guard fixes the phi so `run` reduces with no internal fork, then the merged value is related to the spec. isHexDigit closes via isHexDigitF_eq; hexValue via a new hexValF_eq plus the precondition's range and `wrap` (omega handles the emod). 22 per-path proofs collapse to 2. Co-Authored-By: Claude Opus 4.8 <[email protected]>
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
2 participants
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.
No description provided.