#338: meld's const-expr folding (meld-core/src/segments.rs parse_const_expr_with_value, merger.rs convert_init_expr) drops trailing arithmetic after a leading global.get — e.g. global.get \$base; i32.const 100; i32.add folds to just global.get \$base — silently corrupting PIE base+N global inits and data/elem offsets. Evaluating a const-expr offset is pure i32/i64 QF_BV arithmetic.
Proposal: gate folding with an ordeal prove_equiv check per initializer/offset: folded_value == eval(orig_const_expr). A dropped/incorrect fold becomes a caught SAT counterexample instead of a silent miscompile; a correct fold gets a certificate. Secondary: adapter pointer-fixup/copy-layout offset arithmetic (meld-core/src/adapter/fact.rs) via prove_equiv + the load/store trap lib.
Enabler: the equivalence toolkit — ordeal roadmap pulseengine/ordeal#66 (v0.12.0); fits as-is. Boundary: const-expr eval + address arithmetic is QF_BV; ∀-modules remap injectivity (Rocq) and #297 whole-module behavioral equivalence (needs a runtime) are OUT.
#338: meld's const-expr folding (
meld-core/src/segments.rsparse_const_expr_with_value,merger.rsconvert_init_expr) drops trailing arithmetic after a leadingglobal.get— e.g.global.get \$base; i32.const 100; i32.addfolds to justglobal.get \$base— silently corrupting PIEbase+Nglobal inits and data/elem offsets. Evaluating a const-expr offset is pure i32/i64 QF_BV arithmetic.Proposal: gate folding with an ordeal
prove_equivcheck per initializer/offset:folded_value == eval(orig_const_expr). A dropped/incorrect fold becomes a caught SAT counterexample instead of a silent miscompile; a correct fold gets a certificate. Secondary: adapter pointer-fixup/copy-layout offset arithmetic (meld-core/src/adapter/fact.rs) viaprove_equiv+ the load/store trap lib.Enabler: the equivalence toolkit — ordeal roadmap pulseengine/ordeal#66 (v0.12.0); fits as-is. Boundary: const-expr eval + address arithmetic is QF_BV; ∀-modules remap injectivity (Rocq) and #297 whole-module behavioral equivalence (needs a runtime) are OUT.