cert: bridge functions that take a List - #1448
Merged
Merged
Conversation
The plan grammar gains the two List patterns, `[]` and `[head, ..tail]`, and the two-arm List match the emitter lowers: both arms in either order, or either one first and `_` second. The wall ports `emit_mir_list_match` (stash the subject, `ref.is_null`, the `[]` arm in `then`, the head and tail read from the cons struct into the arm's binders in `else`) and proves the case in `agreement_step`, so a function that matches on a List, recursive ones included, is certified for the bytes already emitted. No helper, no new runtime contract, no schema change; the wall id rotates. The producer prints the patterns and carries the Rust twins of the arm pick, the typing and the lowering. Four hardening tests: the clean List certificate checks, and exchanged arm results, exchanged cons structs and exchanged head and tail slots decline. The ratchet records 54 gains and no loss; btc-listener goes from 632 to 765 certified exports. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A type table long enough to be written in pieces (`types_records_0`, `types_records_1`, ...) left those pieces folded in the `simp` that proves a bridge's arguments well typed, so the step stopped on an unreduced record lookup and the bridge fell to `sorry`. btc-listener's records crossed that length once List matches were certified: 65 of its 494 bridges and one bridged law lost their credit. The typing step now unfolds every piece of the table but the string segments, which typing never reads, and btc-listener is back at 494 of 494 bridges and 16 of 17 bridged laws with 765 certified exports. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # docs/certification.md
…oofs The package's roles_ok and plans_ok unfolded carrierState, carrierConfirmed and typeSectionMatches with simp. Each is a match on the decoded type section, and simp reduced that match before the cut could rewrite the decode, evaluating the whole type-section decode in the elaborator. After the Vector version structs changed the type section, btc-listener's Artifact.lean ran past the 9000-second phase limit. Unfold these definitions by their unconditional equations with matcher reduction off, so the decode is replaced by the cut and read only in the kernel: roles_ok 13 s and plans_ok 68 s on that package, where each ran for over 10 minutes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A non-empty literal pushes its items, then the empty list, and calls the per-type cons helper once per item. The plan grammar now admits that node: its typing needs the cons helper the type table declares for the element type, with the planned signature (T, List<T>) -> List<T>; its lowering is the items, ref.null and one call per item; its meaning is the cons cells of the items in order. The cons helper is offered as a planned internal function, and a new acceptance conjunct (consPinned) requires its plan to be the wall's own cons plan: one List.prepend of its two parameters. So the literal's calls reach a function whose meaning is proved, not assumed, and the agreement proof folds the calls over the reversed items. No schema change; the wall id rotates. The producer prints the items, declares the helper per element type, offers the helper with the literal's function, and carries the Rust twins of the typing and lowering. Bridges of functions that return a literal unfold it with the new simp lemmas. Hostile tests: the helper declared as a user function of the same signature, the helper's plan changed to return the tail, and the helpers of two instantiations exchanged, each refused. Ratchet: gains only. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A source bridge's proof decodes each argument shape of its function, and a List argument had no decoder, so a function taking a List was certified against its plan only and a law about it was not on the bytes. The step lemmas now decode a List of Ints, Bools or Strings as a whole value, one cons cell at a time (decListInt, decListBool, decListString). A step splits a decoded List into its empty and cons shapes, with the tail an encoding again, so a recursive call on the tail meets its callee through the encoding, and a function that returns its List argument meets its image. An export's image reads an encoded List back, and its typing uses the encoded List's type. The List match evaluates arm by arm. Two leaf changes: a callee with a List parameter has its image unfolded in the leaves, and a self-recursive leaf also closes when unfolding the source already closes it. Hostile test: a bridge whose List argument names another element type is refused. Ratchet: gains only. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # CHANGELOG.md # aver-cert/src/engine/source_bridges.rs # tests/cert_certify_spec.rs # tests/cert_hardening_spec.rs
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
1 participant
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.
Third List step for the certificate, stacked on #1447: source bridges for functions that take a List. The laws about those functions now hold on the certified bytes.
A bridge's proof decodes each argument shape of its function. A List argument had no decoder, so a function taking a List was certified against its plan only, and a law about it was not on the bytes. This PR changes only the producer's bridge proofs (
source_bridges.rs). The checker already renderslistencoders, so the wall and the checker are unchanged, the wall id stays the same, and there is no schema change.What changes
decListInt,decListBool,decListString, rendered ahead of the functions' decoders). A List of records, sums or Lists still declines with a reason.decList…_split, fromdecList…_sound). A recursive call on the tail meets its callee through the encoding (decList…_enc), and a function that returns its List argument meets its image. The List match evaluates arm by arm (arms_emptyList_*,arms_cons_*).decList…_enc), and the typing uses the encoded List's type (hasTy_list…).rw; simp; done, which failed with no goals left. A leaf that closed before still closes. On btc-listener no bridge the producer offered before is lost, and every one credited before is still credited.cert_hardening_spec. The List certificate now reportssource-bridges: 3 of 3andbridged-laws: 1 of 1credited, the latter from a law overcount. A bridge whose List argument names another element type is refused. Also a unit test of the decoder shapes.cert_certify_spec,listHeadGoal,sumListGoalandwrapItemsare no longer declined, and the hostile-model baseline credits 25 of 25 bridges instead of 22 of 22.Measurements
aver-cert checkof btc-listener (commit 5698c8e), one Lean process,AVER_CERT_PHASE_TIMEOUT_SECS=9000:The 15 new laws on bytes include
ScriptParse.prependReversed.reverseOnto, theStackItem.validBytesandbigEndianlaws, andMessage.readLittleEndianFrom. The three bridges offered but not credited are new ones (Screen.pressedAll,Screen.pressedNext,Bodies.heightsFrom), and they fail closed. The one bridged law not credited,Chainwork.ofBits.neverNegative, was not credited before either: its own proof usessorry.Tests run
cargo test -p aver-cert --all-features, the certificate snapshots,cert_one_build_spec,cert_hardening_spec(43),cert_certify_spec(39) and thecert_verify_spectripwires (43). Alsocargo fmt --checkand clippy.