Soundness Bug in Function Substitution

[joscoh]

This assertion succeeds:

def functionAssertPgm : Program :=
#strata
program Core;

inline function foo(x : int, $__y0 : int) : int { x + $__y0 }

procedure TestFoo() returns ()
{
  var y : int;
  assert [fooEq]: (foo(y, 2) == 4);
};

#end

#eval verify functionAssertPgm

The reason is that in the evaluation of Factory functions, arguments are substituted for the free variables sequentially, so one can be captured by a future substitution. Here we first substitute x -> $__y0 and then substitute $__y0 -> 2. This particular example relies on giving an "illegal" variable name, but since functions and expressions can be constructed via an API, name clashes are possible.

The most straightforward fix is to do simultaneous substitution rather than sequential substitution when evaluating Factory functions.

[aqjune-aws]

I can see multiple options for resolving this bug. Indeed, $__ is a preserved prefix according to a comment at https://github.com/strata-org/Strata/blob/main/Strata/DL/Lambda/LState.lean#L30-L32 . This wasn't being checked, however. Another option for fixing this is to update FuncWF to state that argument names don't start with $__. I think either solution is fine.

[joscoh]

Fixing the names is not enough, since we provide an API which could still allow someone to generate such ill-formed terms:

-- foo: inline function foo(x : int, y : int) : int { x + y }
private def fooFunc : LFunc CoreLParams :=
  { name := "foo",
    inputs := [("x", .int), ("y", .int)],
    output := .int,
    body := some (.app () (.app () intAddOp (.fvar () ⟨"x", ()⟩ none)) (.fvar () ⟨"y", ()⟩ none)),
    attr := #[.inline] }

-- Factory = Core.Factory (has Int.Add etc.) + foo
private def testState : LState CoreLParams :=
  match LState.init.addFactory (Core.Factory.push fooFunc) with
  | .ok s => s
  | .error e => panic! s!"{e}"

-- foo(y, 2) where y is a free variable
private def expr : LExpr CoreLParams.mono :=
  .app () (.app () fooFunc.opExpr (.fvar () ⟨"y", ()⟩ (some .int))) (.intConst () 2)

#eval do
  let result := LExpr.eval testState.config.fuel testState expr
  IO.println s!"{result}"

We need to fix the substitution mechanism instead (and this will make things easier to prove).

[aqjune-aws]

Makes sense... Indeed, using the parallel substitution alternative seems to be a better choice!