IxVM ingress: panic-on-miss rbtree lookups for ptr_val-keyed maps#472
Draft
arthurpaulino wants to merge 3 commits into
Draft
IxVM ingress: panic-on-miss rbtree lookups for ptr_val-keyed maps#472arthurpaulino wants to merge 3 commits into
arthurpaulino wants to merge 3 commits into
Conversation
`ix name-of --ixe <path> <hex>`: given a 32-byte hex address, scan the `.ixe` env's `named` map and print the fully-qualified Lean.Name of the const stored under that address. Prints an error + exits 1 if no named const matches (the address might be an unnamed intermediate constant or a blob). Complements `ix addr-of` (name → address). Used to backtrack from an assertion-failure address logged mid-kernel-execution to the offending Lean constant.
Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).
The `addr_pos_map` / `block_start_map` lookups are keyed by `ptr_val`. Aiur's memory AIR strictly increments the pointer column, so the memory table is a function ptr -> values: `ptr_val` equality implies content equality (no false collisions), but the converse can fail — a malicious witness may de-intern (same content stored at several pointers), which the AIR permits. An honest prover interns (the executor dedups `store` by content) and so always hits. Switch the three guaranteed-present probes from `rbtree_map_lookup_or_default(.., 0)` to the panic-on-miss `rbtree_map_lookup` (no `Nil` arm — the non-exhaustive match is the assert-present): - `lookup_block_start`: soundness fix. Its stored values are raw 0-based block starts, so `0` is a valid position (the first block), not an out-of-band sentinel. A de-interned `block_addr` would miss, default to 0, and silently resolve a projection to `off` instead of `block_start + off` — aliasing the wrong constant. Panic-on-miss rejects that witness. - `lookup_addr_pos` / `build_ref_idxs_and_blobs`: the miss branch was a content-based `address_eq` linear scan that was dead for honest provers (same-cell build/lookup makes a miss impossible; `augment_with_blob_refs` keys every ref from the same list cells `build_ref_idxs_and_blobs` probes, and `build_convert_inputs` passes `all_addrs` as both the map source and the head-address list). Delete the dead scan (`lookup_addr_pos_linear`) and the `all_addrs`/`pos_map` params that fed it. No ptr-inequality is used to infer data-inequality anywhere; the `canon_addr_map` / `visited_set` / `skip_set` / `emit_addrs` probes keep `_or_default` because "absent" is a legitimate branch there. Regen codegen + re-pin FFT costs (small shifts from the lookup-function split; measured, not padding — the cost model is w*h*log2(h) with h = uniqueRows).
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.
The
addr_pos_map/block_start_maplookups are keyed byptr_val.Aiur's memory AIR strictly increments the pointer column, so the memory
table is a function ptr -> values:
ptr_valequality implies contentequality (no false collisions), but the converse can fail — a malicious
witness may de-intern (same content stored at several pointers), which
the AIR permits. An honest prover interns (the executor dedups
storeby content) and so always hits.
Switch the three guaranteed-present probes from
rbtree_map_lookup_or_default(.., 0)to the panic-on-missrbtree_map_lookup(noNilarm — the non-exhaustive match is theassert-present):
lookup_block_start: soundness fix. Its stored values are raw 0-basedblock starts, so
0is a valid position (the first block), not anout-of-band sentinel. A de-interned
block_addrwould miss, default to0, and silently resolve a projection to
offinstead ofblock_start + off— aliasing the wrong constant. Panic-on-missrejects that witness.
lookup_addr_pos/build_ref_idxs_and_blobs: the miss branch was acontent-based
address_eqlinear scan that was dead for honest provers(same-cell build/lookup makes a miss impossible;
augment_with_blob_refskeys every ref from the same list cells
build_ref_idxs_and_blobsprobes, and
build_convert_inputspassesall_addrsas both the mapsource and the head-address list). Delete the dead scan
(
lookup_addr_pos_linear) and theall_addrs/pos_mapparams that fedit.
No ptr-inequality is used to infer data-inequality anywhere; the
canon_addr_map/visited_set/skip_set/emit_addrsprobes keep_or_defaultbecause "absent" is a legitimate branch there.Regen codegen + re-pin FFT costs (small shifts from the lookup-function
split; measured, not padding — the cost model is whlog2(h) with
h = uniqueRows).