TAny should be a proper function type

[ssyram]

As the title, the function analyze_function_type, in Structs.ml, currently accepts only TArrow as proper function types. But TAny should also be a proper function type? E.g., for Haskell-like codes: undefined x y should also work.

A potential problem happens here that some usage of analyze_function_type will need the length of the arguments, but TAny has no information about the potential application length. Is this a simple problem to fix?

[msprotz]

how did you end up triggering this? can you send a repro?

(it's ok if the repro is with eurydice)

[ssyram]

Thanks. It was when I want to experiment if I can add the support for FnOpMove... My solution is that I translate f(x) into app(f, x), like in Haskell. But the type of app is a bit hard to work with, so I want TAny. But then encountered this problem.

[msprotz]

Why don't you translate it into an EApp node, even if the head is an EBound? You should be able to provide correct type information for it, which means the rest of the translation should go smoothly.

Are you attempting to translate closures? If so, @Nadrieril has some improvements in the pipeline.

[msprotz]

Overall, I'm quite interested in your use-case, so if you could say a little more about what you are trying to achieve, possibly with a complete repro, I might be able to provide more useful suggestions.

[ssyram]

Thanks for your advice! Actually, I'm just trying to understand the codes better rather than working in some specific use case.

I think Fn (closure) is a bit harder that it essentially involves deciding the associated types, which I thought is a bit troublesome even in Charon?

So, I want to add support for fn to just have a try, which seems to be just a millimeter away that FnOpMove is not supported. And yes, I used EApp, but I just wanted to introduce a unique marker function (app) for it and then remove the marker in the generated C codes.

And there are additional difficulties when I want to introduce different types for different apply functions. If the fn type involves generic or even const generics...

[ssyram]

Further, despite the cases, I wanted to implement a function for each stuff with type attached, and I believe have implemented correctly, but was then stopped by the Krml check...

I have the use case:

fn multiple_ptr(f : fn(&i32, &i32) -> i32) -> i32 {
    f(&1,&2)
}

So, the translated Low* is the following, as shown in the log:

  external $$apply$2 <0>:<cg: 0>
    ( int32_t* ->  int32_t* -> int32_t) ->

      int32_t* ->

        int32_t* ->
        int32_t
...
    let
    mutable
    uu____190(Mark.MaybeAbsent,(Mark.AtMost 4611686018427387903), ):

      int32_t* ->

        int32_t* ->
        int32_t
    = $any
...
    let
    mutable
    uu____191(Mark.MaybeAbsent,(Mark.AtMost 4611686018427387903), ):  int32_t*
    = $any
    in
...
    let
    mutable
    uu____194(Mark.MaybeAbsent,(Mark.AtMost 4611686018427387903), ):  int32_t*
    = $any
    in
...
    uu____189@7 := $$apply$2 uu____190@6 uu____191@5 uu____194@2;

I guess this perfectly aligns with my intention.

But the "checker" log from Krml then shows a strange error of subtype mismatch for "int32_t (a.k.a. int32_t) vs: int32_t* -> int32_t (a.k.a. int32_t* -> int32_t)".

I printed out the log, which is strange:

[check] t=int32_t for e=$$apply$2 @6 @5 @2
[check] annot= int32_t* -> int32_t for e=$$apply$2 @6 @5 @2
[infer] $$apply$2 @6 @5 @2
[infer] $$apply$2
[infer, got] ( int32_t* ->  int32_t* -> int32_t) ->  int32_t* ->  int32_t* -> int32_t
( int32_t* ->  int32_t* -> int32_t) ->  int32_t* ->  int32_t* -> int32_t <=? ( int32_t* ->  int32_t* -> int32_t) ->  int32_t* ->  int32_t* -> int32_t
 int32_t* ->  int32_t* -> int32_t <=?  int32_t* ->  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
 int32_t* -> int32_t <=?  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
int32_t <=? int32_t
 int32_t* ->  int32_t* -> int32_t <=?  int32_t* ->  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
 int32_t* -> int32_t <=?  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
int32_t <=? int32_t
[infer, now] ( int32_t* ->  int32_t* -> int32_t) ->  int32_t* ->  int32_t* -> int32_t
[check] t= int32_t* ->  int32_t* -> int32_t for e=@6
[check] annot= int32_t* ->  int32_t* -> int32_t for e=@6
[infer] @6
[infer, got]  int32_t* ->  int32_t* -> int32_t
 int32_t* ->  int32_t* -> int32_t <=?  int32_t* ->  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
 int32_t* -> int32_t <=?  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
int32_t <=? int32_t
[infer, now]  int32_t* ->  int32_t* -> int32_t
 int32_t* ->  int32_t* -> int32_t <=?  int32_t* ->  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
 int32_t* -> int32_t <=?  int32_t* -> int32_t
 int32_t* <=?  int32_t*
int32_t <=? int32_t
int32_t <=? int32_t
[check] t= int32_t* for e=@5
[check] annot= int32_t* for e=@5
[infer] @5
[infer, got]  int32_t*
 int32_t* <=?  int32_t*
int32_t <=? int32_t
[infer, now]  int32_t*
 int32_t* <=?  int32_t*
int32_t <=? int32_t
[check] t= int32_t* for e=@2
[check] annot= int32_t* for e=@2
[infer] @2
[infer, got]  int32_t*
 int32_t* <=?  int32_t*
int32_t <=? int32_t
[infer, now]  int32_t*
 int32_t* <=?  int32_t*
int32_t <=? int32_t
[infer, got] int32_t
int32_t <=?  int32_t* -> int32_t

Note that, everything works fine but suddenly in the final line, the error occurs. I guess there is a bug within the Krml checking procedure.

[msprotz]

Two possibilities.

1. Perhaps there's an issue in AstOfLlbc, see https://github.com/AeneasVerif/eurydice/blob/main/lib/AstOfLlbc.ml#L1402-L1426

Sometimes, the closure type requires passing an extra "address-of" for the captured state.

Could this be what you're experiencing? (I have not debugged this further since I did not work on closures very much.)

2. You are adding an incorrect type annotation on your AST node, which then results in an inconsistency, which the internal Checker module detects.

Is this normal? [check] annot= int32_t* -> int32_t for e=$$apply$2 @6 @5 @2 -- is an arrow type the result you expect for your application of $$apply2$$?

[ssyram]

Thanks for spotting 2! Yes, you're right and it works now!

[msprotz]

Great! I assume you'll submit a PR?

[ssyram]

I'll have a try.

[msprotz]

Thanks! Looking forward to it this seems like a generally useful addition