feat: lookup constraints for function calls

[letypequividelespoubelles]

No description provided.

[Copilot]

Pull request overview

This PR adds constraint-generation support for VM function calls by emitting lookup constraints at call sites, including handling of conditional calls via materialised path selectors. It also extends unit test coverage with new call/switch fixtures and adjusts some execution/trace and logical simplification behavior to support the new constraint wiring.

Changes:

• Emit per-call lookup constraints in pkg/zkc/constraints/translator.go, including optional gating via PC selectors and (materialised) branch/path selectors.
• Extend skip-condition factoring and proposition simplification to better support conditional execution paths involved in call lookups.
• Add/enable new unit tests and fixtures for call patterns and switch-based dispatch under constraints mode.

Reviewed changes

Copilot reviewed 14 out of 14 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
testdata/zkc/unit/switch_11.zkc	New unit program exercising switch-driven calls.
testdata/zkc/unit/switch_11.accepts	Accepted inputs for switch_11 fixture.
testdata/zkc/unit/call_05.zkc	New unit program testing different callees chosen by branching.
testdata/zkc/unit/call_05.accepts	Accepted inputs for call_05 fixture.
testdata/zkc/unit/call_06.zkc	New unit program testing b = f(a) + 1 behavior.
testdata/zkc/unit/call_06.accepts	Accepted inputs for call_06 fixture (currently malformed JSON).
testdata/zkc/unit/call_07.zkc	New unit program testing x = f(x) + 1 with aliasing/rewrite patterns.
testdata/zkc/unit/call_07.accepts	Accepted inputs for call_07 fixture (currently malformed JSON).
pkg/zkc/vm/internal/transform/factor_skip_conditions.go	Factor skip conditions when needed for call lookup source selectors; add call detection helper.
pkg/zkc/vm/internal/trace/full_observer.go	Refactor terminal-state recording to avoid losing rows after returning from a callee.
pkg/zkc/constraints/translator.go	Core change: compute module metadata and emit lookup constraints for Call/UnconditionalCall, including selector materialisation logic.
pkg/util/logical/proposition.go	Add consensus/resolution step during proposition simplification to collapse redundant branches.
pkg/test/zkc_unit_test.go	Run call-related fixtures in constraints mode; add tests for new fixtures.
pkg/test/util/check_valid.go	Remove commented-out trace printing in failure path.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 26 out of 26 changed files in this pull request and generated 3 comments.

[Copilot]

Pull request overview

Copilot reviewed 26 out of 26 changed files in this pull request and generated no new comments.

Comments suppressed due to low confidence (1)

pkg/zkc/constraints/translator.go:263

• The IS_PC_* selectors (and $ret) are now used as lookup selectors for call constraints (see addCallLookups / emitCallLookup), but initMultiLineFraming does not constrain these 1-bit registers to be boolean (0/1). For lookup soundness, selectors must be boolean; otherwise non-{0,1} values can scale/weight lookups and satisfy constraints incorrectly.

	// pc_decoding, none when PC==0).
	exclusivity := mir.NewVanishingConstraint("is_pc_exclusivity", ctx, util.None[int](),
		pc_i.Multiply(sum).Equals(pc_i).AsLogical())
	//
	constraints := []mir.Constraint[F]{padding, init, reset, first, decoding, exclusivity}

[Copilot]

Pull request overview

Copilot reviewed 26 out of 26 changed files in this pull request and generated 3 comments.