An attribute for making partial evaluator inline Boogie(Strata Core) functions

[aqjune-aws]

Boogie (Strata Core) functions are not inlined by default but rather translated to the define-fun SMT-LIB command because they may be used in axioms.

If the DDM of Boogie (Strata Core) has a way of attaching inline attribute & letting them eagerly inlined during partial evaluation or through a dedicated inlining pass, it will be useful for performance.

[andrewmwells-amazon]

Concretely, we'd like to inline a function like this:

#strata
program Boogie;

datatype Any () {
  Any_str(Any_str_val: string),
  Any_int(Any_int_val: int)
};

function isStr(v: Any): bool {
  Any..isAny_str(v)
}

function isInt(v: Any): bool {
  Any..isAny_int(v)
}

procedure main() returns ()
{
  var short_bucket_name_inner: string;
  var short_bucket_name: Any;

  short_bucket_name_inner := "abcdefg";
  short_bucket_name := Any_str(short_bucket_name_inner);

  assert [short_bucket_nameIsStr]: isStr(short_bucket_name);
};
#end 

By writing:

{inline} function isStr(v: Any): bool {
  Any..isAny_str(v)
}

{inline} function isInt(v: Any): bool {
  Any..isAny_int(v)
}

With the result that the final line becomes:

  assert [short_bucket_nameIsStr]: Any..isAny_str(short_bucket_name);

Which can be discharged by PE.