JAR: Join-Accumulate Refine

11.9. Cap Table Operations🔗

🔗def
Jar.JAVM.Kernel.handleSplit (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleSplit
  (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) :
  KernelState × DispatchResult

SPLIT a DATA cap. φ[7]=page_offset. Subject=DATA, object=dst slot for hi half.

🔗def
Jar.JAVM.Kernel.handleDrop (state : KernelState) (vmIdx slot : Nat) :
  KernelState × DispatchResult
Jar.JAVM.Kernel.handleDrop
  (state : KernelState)
  (vmIdx slot : Nat) :
  KernelState × DispatchResult

DROP a cap. Auto-unmaps DATA.

🔗def
Jar.JAVM.Kernel.handleMove (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleMove
  (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) :
  KernelState × DispatchResult

MOVE a cap between CNodes. Auto-unmaps DATA on CNode change.

🔗def
Jar.JAVM.Kernel.handleCopy (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleCopy
  (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) :
  KernelState × DispatchResult

COPY a cap between CNodes (copyable types only).

🔗def
Jar.JAVM.Kernel.handleDowngrade (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleDowngrade
  (state : KernelState)
  (sVm sSlot oVm oSlot : Nat) :
  KernelState × DispatchResult

DOWNGRADE HANDLE → CALLABLE. Subject=HANDLE, object=dst slot.

🔗def
Jar.JAVM.Kernel.handleSetMaxGas (state : KernelState)
  (vmIdx slot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleSetMaxGas
  (state : KernelState)
  (vmIdx slot : Nat) :
  KernelState × DispatchResult

SET_MAX_GAS on a HANDLE. φ[7]=gas_limit.