chore: merge origin master & update p/spl-token.md (#897)

- #893 
- #892 
- #894 
- #896 
- [update spl/p-token.md to use
#execTerminatorCall](39ce2a6)
- #898

Author: jberthold

deps/pyproject-build-systems

@@ -1 +1 @@
-795a980d25301e5133eca37adae37283ec3c8e66
+042904167604c681a090c07eb6967b4dd4dae88c

deps/stable-mir-json

@@ -1 +1 @@
-20a1bbdfc1fb36fb19539d0d4d91f5a437be7de6
+626e8fed0470078c4d980b6b5b503a3aceb355ec

deps/stable-mir-json_release

@@ -1 +1 @@
-c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c
+4cca323a547a1aaa9b94929c4901bed5343eafe8

deps/uv2nix

@@ -1 +1 @@
-0.9.9
+0.9.14

deps/uv_release

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/20a1bbdfc1fb36fb19539d0d4d91f5a437be7de6";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/626e8fed0470078c4d980b6b5b503a3aceb355ec";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";
@@ -18,7 +18,7 @@
       inputs.nixpkgs.follows = "nixpkgs";
     };
 
-    uv2nix.url = "github:pyproject-nix/uv2nix/c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c";
+    uv2nix.url = "github:pyproject-nix/uv2nix/4cca323a547a1aaa9b94929c4901bed5343eafe8";
     # uv2nix requires a newer version of nixpkgs
     # therefore, we pin uv2nix specifically to a newer version of nixpkgs
     # until we replaced our stale version of nixpkgs with an upstream one as well
@@ -27,7 +27,7 @@
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
     uv2nix.inputs.nixpkgs.follows = "nixpkgs-unstable";
     # uv2nix.inputs.nixpkgs.follows = "nixpkgs";
-    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/795a980d25301e5133eca37adae37283ec3c8e66";
+    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/042904167604c681a090c07eb6967b4dd4dae88c";
     pyproject-build-systems = {
       inputs.nixpkgs.follows = "uv2nix/nixpkgs";
       inputs.uv2nix.follows = "uv2nix";

flake.lock

@@ -308,21 +308,33 @@ The call stack is not necessarily empty at this point so it is left untouched.
 `Call` is calling another function, setting up its stack frame and
 where the returned result should go.
 
-
 ```k
-  // Intrinsic function call - execute directly without state switching
-  rule [termCallIntrinsic]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
-         =>
-           #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET)
+  syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction)
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND)
+        ...
        </k>
-    requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), _SPAN))
+        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND)
+        ...
+       </k>
+      <locals> LOCALS </locals>
+
+  // Intrinsic function call - execute directly without state switching
+  rule [termCallIntrinsic]:
+        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND) ~> _
+         => #execIntrinsic(FUNC, ARGS, DEST) ~> #continueAt(TARGET)
+        </k>
+    requires isIntrinsicFunction(FUNC)
 
   // Regular function call - full state switching and stack setup
-  rule [termCallFunction]: <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
-         =>
-           #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
+  rule [termCallFunction]:
+       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND) ~> _
+        => #setUpCalleeData(FUNC, ARGS)
        </k>
-       <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
+       <currentFunc> CALLER => FTY </currentFunc>
        <currentFrame>
          <currentBody> _ </currentBody>
          <caller> OLDCALLER => CALLER </caller>
@@ -332,7 +344,7 @@ where the returned result should go.
          <locals> LOCALS </locals>
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
-    requires notBool isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
+    requires notBool isIntrinsicFunction(FUNC)
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
   rule isIntrinsicFunction(IntrinsicFunction(_)) => true
@@ -341,11 +353,6 @@ where the returned result should go.
   syntax KItem ::= #continueAt(MaybeBasicBlockIdx)
   rule <k> #continueAt(someBasicBlockIdx(TARGET)) => #execBlockIdx(TARGET) ... </k>
   rule <k> #continueAt(noBasicBlockIdx) => .K ... </k>
-
-  syntax Ty ::= #tyOfCall( Operand ) [function, total]
-
-  rule #tyOfCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _)))) => Ty
-  rule #tyOfCall(_) => ty(-1) [owise] // copy, move, non-zero size: not supported
 ```
 
 The local data has to be set up for the call, which requires information about the local variables of a call. This step is separate from the above call stack setup because it needs to retrieve the locals declaration from the body. Arguments to the call are `Operands` which refer to the old locals (`OLDLOCALS` below), and the data is either _copied_ into the new locals using `#setArgs`, or it needs to be _shared_ via references.
@@ -415,7 +422,8 @@ An operand may be a `Reference` (the only way a function could access another fu
      andBool isTypedValue(CALLERLOCALS[I])
     [preserves-definedness] // valid list indexing checked
 
-  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems)))
+  // TODO: This is not safe, need to add more checks to this.
+  rule <k> #setArgFromStack(IDX, operandMove(place(local(I), _)))
         =>
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
         ...

flake.nix

@@ -130,6 +130,17 @@ Constant operands are simply decoded according to their type.
     requires typeInfoVoidType =/=K lookupTy(TY)
 ```
 
+Function pointers are zero-sized constants whose `Ty` is a key in the function table instaed of the type table.
+
+```k
+  rule <k> operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, ty(ID) #as TY, _)))
+        => FunPtr(TY)
+       ...
+       </k>
+    requires typeInfoVoidType ==K lookupTy(TY) // not a valid type info
+     andBool lookupFunction(TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty
+```
+
 ### Copying and Moving
 
 When an operand is `Copied` by a read, the original remains valid (see `false` passed to `#readProjection`).

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -51,6 +51,8 @@ The special `Moved` value represents values that have been used and should not b
                                                           [symbol(Value::PtrLocal)]
                    // pointer to a local TypedValue (on the stack)
                    // fields are the same as in Reference
+                 | FunPtr ( Ty )
+                   // function pointer, created by operandConstant only. Ty is a key in the function table
                  | AllocRef ( AllocId , ProjectionElems , Metadata )
                                                           [symbol(Value::AllocRef)]
                    // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable