Generate function definitions

[tothtamas28]

Closes #4727

Generate a function definition for each (interpreted) function symbol and each function rule.

The definition for a function symbols applies its rule functions in an order respecting priorities:

def «#lookup(_,_)_IMP_KItem_Id_Map» (x0 : SortId) (x1 : SortMap) : Option SortKItem :=
  [_acfc941, _0e4f65f].findSome? (· x0 x1)

A function rule evaluates to none if

• the LHS pattern doesn't match;
• a function application is the requires clause or the RHS is undefined;
• the requires clause does not hold;

and to some otherwise:

def _acfc941 : SortId → SortMap → Option SortKItem
  | X, M => do
    let _Val0 <- «_in_keys(_)_MAP_Bool_KItem_Map» ((@inj SortId SortKItem) X) M
    let _Val1 <- «Map:lookup» M ((@inj SortId SortKItem) X)
    guard _Val0
    return _Val1

def _0e4f65f : SortId → SortMap → Option SortKItem
  | X, M => some (SortKItem.«Error(_,_)_IMP_KItem_Id_Map» X M)

Function definitions depending on an uninterpreted function are marked noncomputable.

[tothtamas28]

Known limitations

Restricting an argument to a subsort on the LHS

This fails to capture the case where a subsort of the subsort is injected directly.

def _f4c2469 : SortK → Option SortBool
  | SortK.kseq (SortKItem.inj_SortKResult KResult) SortK.dotk => some true
  | _ => none

Solution: unroll the pattern for each subsort (that has no further subsorts):

def _f4c2469 : SortK → Option SortBool
  | SortK.kseq (SortKItem.inj_SortBool KResult) SortK.dotk
  | SortK.kseq (SortKItem.inj_SortInt KResult) SortK.dotk => some true
  | _ => none

Collection patterns on the LHS

Collection "constructors" are mapped as functions, thus cannot be used in patterns.

def _2ede380 : SortList → Option SortInt
  | _List_ _Gen0 (ListItem (SortKItem.inj_SortInt I)) => do
    let _Val0 <- «_+Int_» I 1
    return _Val0
  | _ => none

Solution: add a de-structuring function for each supported pattern to the correspoinding hook implementation, then:

def _2ede380 (x0 : SortList) : Option SortInt :=
  match list_pat_init_last x0
  | some (_Gen0 (SortKItem.inj_SortInt I)) => do
    let _Val0 <- «_+Int_» I 1
    return _Val0
  | _ => none

[JuanCoRo]

Shouldn't other functions be added? Such as «_modInt_»? We could also add hooked functions such as _List_. They would be noncomputable rather than the current axioms, and we have the above hooks to link to them.

[JuanCoRo]

This could very well be a follow up PR tho!

[tothtamas28]

Yes, these few functions are just to demonstrate how to define functions that have no associated function rules:

• Add function definition to Preulde.
• Add KORE symbol name to _PRELUDE_FUNCS in k2lean4.py.

[JuanCoRo]

I'm getting the following error when trying to build the Func.lean file:

fail to show termination for
  _432555e
  sizeWordStackAux
with errors
failed to infer structural recursion:
Cannot use parameters #1 of _432555e and x0 of sizeWordStackAux:
  unexpected occurrence of recursive application
    _432555e
Cannot use parameters #2 of _432555e and x1 of sizeWordStackAux:
  the type Int does not have a `.brecOn` recursor

This is for the following mutual block, but the larger one is also showing a similar error:

mutual
  def _432555e : SortWordStack → SortInt → Option SortInt
    | SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Gen0 WS, SIZE => do
      let _Val0 <- «_+Int_» SIZE 1
      let _Val1 <- sizeWordStackAux WS _Val0
      return _Val1
    | _, _ => none

  def sizeWordStackAux (x0 : SortWordStack) (x1 : SortInt) : Option SortInt := [_432555e, _75897fa].findSome? (· x0 x1)
end

Somehow Lean is failing to see that the block is decreasing on the SortWordStack argument

[JuanCoRo]

The _432555e termination proof seems a bit tricky, since Lean it's not finding it by structural recursion, and the other path we have is by some size function on SortWordStack, but that's precisely _432555e if I understood right.
We could define another size function for SortWordStack that is obviously terminating to Lean, and then use that decreasing measure here, but perhaps there's a more straight-forward solution?

[tothtamas28]

Regarding the termination proof issue.

I did a few experiments, and I think it might actually be a bug in Lean. In particular, as defined, Lean is unable to show that in sizeWordStackAux, function _432555e is invoked with x0, x1, and instead introduces fresh variables in the goal. This practically makes it impossible to finish the proof.

If however the definition is modified to

  def sizeWordStackAux (x0 : SortWordStack) (x1 : SortInt) : Option SortInt := (_432555e x0 x1) <|> (75897fa x0 x1)

the goal is as expected, and in fact no manual proof is necessary.

I'll look into this a bit more, push a hotfix for the generator, and open an issue on Lean if necessary.