Overeager substitution in dead code elimination?

[andres-erbsen]

It looks like "DCE" inlines a let binder that is in fact used, causing synthesis to fail with Invalid identifier in arithmetic expression Z.zselect. @JasonGross do you have a guess for what is going on here?

After rewriting RewriteArith_0:
let x15 := Z.zselect(x13₁, (0, 38)) in

After rewriting DCE after RewriteArith_0:
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), ((x12₂ << 0x140) + x8₁)))) in

Log: https://gist.github.com/andres-erbsen/bbfb1994c4e8294be35c5ab59966faf2#file-sat_add-log-L249-L281
Source: andres-erbsen@48c3e62#diff-fc27e1c96d797f696a0116daf62647b093f90d5f4cf52eba7896076151990554

[JasonGross]

I do not. I guess the DCE calculation is buggy? Strange that it hasn't shown up before this...

[JasonGross]

Hmm, it's possible that the DCE code does not know how to handle lambdas, and the thunked branches of the if statements are messing it up?

[JasonGross]

Nope, the code seems to handle lambdas fine. If you can paste valid Coq code that computes to the expression before DCE, such that vm_compute on DCE results in the mis-inlining, I can try single-stepping it and see what's going on

[andres-erbsen]

There you go: andres-erbsen@811460b Thank you!

[andres-erbsen]

See also #1601 (comment)

[JasonGross]

I've tracked down the issue, and indeed it is what I originally suspected: DCE cannot handle code branching that contains lambdas, so it's the if-statements that are causing trouble. The code at

fiat-crypto/src/MiscCompilerPasses.v

Lines 93 to 94 in 1cce238

	| expr.Abs s d f
	=> (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx))))

and

fiat-crypto/src/MiscCompilerPasses.v

Lines 58 to 60 in 1cce238

	| expr.Abs s d f
	=> let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in
	(cur_idx, live)

does not propagate the index update from underneath the lambda, and so indices end up being incorrectly reused.

I can think of two solutions:

1. Thread a boolean of "is in head position", so that we recurse under the initial lambdas, but not under lambdas in the arguments to any App, nor under lambdas in the variable-bindings of let-in
2. Adjust subst0n' to recurse over the PHOAS expression at two different var arguments, one for tracking the current index, and the other for tracking the returned expression.

Thoughts? (And do you feel confident implementing either of these fixes?)