feat(verify): teach Z3 verifier about element-section table resolver (v1.0.4 Track B)#126
Merged
Merged
Conversation
…(v1.0.4 Track B) Drops directize's Z3 bypass from v1.0.2. The verifier now resolves 'i32.const N; call_indirect (type T)' to the same 'pure_call_<F>(args)' Z3 expression that PR-K3 uses for direct 'call F' — proving them equal under congruence closure. ## What changed verify.rs: - VerificationSignatureContext gains a 'table_resolver: HashMap<(u32, u32), u32>' field, populated via crate::optimize::build_table_resolver(module). - New 'resolve_indirect_call(table_idx, slot, expected_type)' helper returns Some(func_idx) only if BOTH the resolver maps the slot AND the resolved function's signature is byte-identical to the indirect- call's declared type. - The CallIndirect encoder now checks whether the popped slot BV is concrete via z3 0.19.7's BV::as_u64() (works for our I32Const(N) encoding which produces BV::from_i64(n, 32)). If concrete AND resolved, it encodes the result as 'pure_call_<F>(args)' via FuncDecl::apply — SAME function symbol PR-K3 uses for direct Call, so two equivalent forms produce structurally equal BVs. - The resolved-call path SKIPS the global/memory havoc that the fallback indirect-call encoding performs. Soundness justification: the resolved callee's purity is a property of the underlying func symbol (pure_call_F has no state-modification semantics). lib.rs: - 'build_table_resolver' and 'TableResolver' alias are now pub(crate) so the verifier can use them. - directize() now constructs TranslationValidator::new_with_context() with the populated sig context. Z3 verification is BACK; the v1.0.2 comment block explaining the Z3 bypass is replaced with one explaining the Z3-active mode. ## Tests All 3 existing directize tests pass with Z3 verification active: - test_directize_folds_known_indirect_call - test_directize_skips_non_const_index - test_directize_skips_out_of_range_index The structural guards (no Unknown + slot resolves + signature matches) remain as defense-in-depth. Z3 is now the load-bearing proof. ## Why this matters v1.0.2 deferred Track 3 with an honest explanation: 'The verifier encodes call_indirect and call F as INDEPENDENT uninterpreted functions [so] congruence cannot prove them equal.' This PR teaches the verifier the resolver, mapping resolved-indirect calls to the SAME function symbol PR-K3 uses for direct calls. The congruence axiom does the rest. ## v1.0.5+ follow-ups - Multi-result resolved indirect calls (currently fall through to the fresh-symbolic path; needs Z3 tuple sort). - Concrete-slot detection beyond BV::as_u64() (e.g., propagating through I32Eqz / I32Eq folded constants). - A regression test in verify.rs's own test module asserting structural BV equality between 'call F' and resolved 'call_indirect'. Trace: REQ-1, REQ-6, REQ-11
avrabe
added a commit
that referenced
this pull request
May 18, 2026
Four-track parallel sprint with FULL success (vs v1.0.3 where Track 3 died): #125 Track A async-callback adapter pass (#70 first piece) #126 Track B verifier table-resolver teaching (drops directize Z3 bypass) #127 Track C ægraph rewrite engine + 3 identity rules #128 Track D island-model parallel optimization (#71) Plus a subagent new-issues sweep that found zero issues since v1.0.3. +20 tests, 380+ total. Code-section bytes unchanged on the current corpus — all four tracks ship infrastructure that will produce measurable wins once their consumers land in v1.0.5+.
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.
Drops directize's Z3 bypass from v1.0.2. The verifier now resolves
i32.const N; call_indirect (type T)to the samepure_call_<F>(args)Z3 expression PR-K3 uses for directcall F. All 3 directize tests pass with Z3 verification ACTIVE.🤖 Generated with Claude Code