vm overrides

Stream: general

[Edward Ayers]

I was thinking about VM overrides a little this week. I hacked around with the Lean source code a little and I got the VM to swap out vm_declarations when one attaches a vm_override attribute to a declaration.
https://github.com/EdAyers/lean/tree/vm_override
The branch is not usable and crashes lean all of the time, it's just an experiment.
The conclusions of my experiment are:

I get stack mismanagement errors if the VM overridden type has a different size to the original type. So just swapping out declarations isn't good enough. The VM needs to keep a registry of what is overridden.
My proposal for VM overrides is to use typeclasses or similar to give a pseudo-bijection between the original data and the override data:

inductive float := ...IEEE definition of float goes here

meta instance : has_vm_override float native.float :=  ⟨to_native, from_native⟩

  -- now the VM is aware that all floats should be converted to native.floats.

  @[vm_override native.float.add]
  def add : float → float → float :=   ... IEEE definition
  instance : has_add float := ⟨add⟩

The VM will use the given to_native and from_native functions to convert between the formats. This means that if you define some operation on floats but you forget to give the VM override, then it won't completely break the VM because the VM can convert between the native and nonnative versions of the data as necessary.

[Mario Carneiro]

It shouldn't be possible to forget to give the VM override once the basics are set up. In particular, all core operations that reference the overridden type (of which there are O(1) of them) must be overridden. In your example that means all the float constructors and float.rec. In practice I would instead define a separate inductive type inductive IEEE_float := ... like you are envisioning, and then structure float := (to_IEEE: IEEE_float) is a newtype that gets overridden. Now you only need a few overrides: to_IEEE is overriden to from_native, mk is overridden to to_native, and float.rec is overridden to a function that uses from_native.

[Mario Carneiro]

Could you elaborate on the stack mismanagement errors? It is possible that we need to hint to lean that the type itself is being overridden (and it's also good documentation), but I didn't think this would be necessary.

[Edward Ayers]

@Mario Carneiro Is this the kind of thing you have in mind?

inductive IEEE_float := ...

def IEEE_float.add := ...
-- plus other defininitions

@[vm_override native.float]
structure float := (to_IEEE : IEEE_float)

@[vm_override native.float.add]
def float.add : float -> float - > float := \lam (mk x) (mk y), mk $ IEEE_float.add x y

-- Errors because no VM override attribute
def float.neg : float -> float  := \lam (mk x) , mk $ IEEE_float.neg x

-- This does not error because only composed of vm_overridden functions.
def float.double := \lam x , float.add x x

[Edward Ayers]

I'll get back to you with details of VM stack errors. Most likely a function of my misprogramming than with Lean.

[Mario Carneiro]

@Edward Ayers Here's how you override the core functions:

meta constant native.float : Type
meta constant native.float.add : native.float → native.float → native.float

inductive IEEE_float := ...

def IEEE_float.add := ...
-- plus other defininitions

meta constant native.float.to_IEEE : native.float → IEEE_float
meta constant native.float.of_IEEE : IEEE_float → native.float

-- No vm implementation needed
@[inline] meta def native.float.rec {C : Sort*}
  (H : IEEE_float → C) (f : native.float) : C :=
H f.to_IEEE

@[vm_override native.float] -- optional?
structure float := (to_IEEE : IEEE_float)

-- Override the core functions
attribute [vm_override native.float.rec] float.rec
attribute [vm_override native.float.of_IEEE] float.mk
attribute [vm_override native.float.to_IEEE] float.to_IEEE

@[vm_override native.float.add]
def float.add : float -> float - > float := \lam (mk x) (mk y), mk $ IEEE_float.add x y

-- No error because the equation compiler defines this function in terms of
-- float.rec and float.mk
def float.neg : float -> float  := \lam (mk x) , mk $ IEEE_float.neg x

-- This does not error because only composed of vm_overridden functions.
def float.double := \lam x , float.add x x

[Edward Ayers]

I get a only attribute [class] accepted for structures error for adding vm_override attribute to float. Should I turn off in C++ or is it there for a reason?

[Mario Carneiro]

I would guess that there is no good reason for the restriction

[Mario Carneiro]

But I can't replicate the error. This works, for example:

@[norm] structure T := (n : nat)

[Mario Carneiro]

but actually, like I say in the comment I'm not sure that it is required to vm_override the type itself, since the type is erased. (It might make good documentation but I don't see how the VM would make use of the info.)

[Edward Ayers]

My VM error was coming from Lean doing some optimisation on declarations which use projection.

@[vm_override native.float.to_repr]
def to_repr : float → string := λ x, IEEE_float.to_repr $ float.to_IEEE $ x

@[vm_override native.float.to_repr]
def to_repr2 : float → string := λ ⟨x⟩, IEEE_float.to_repr $  x

-- this one works
#eval (to_repr $ float.one)

-- this one gives a VM stack error.
#eval (to_repr2 $ float.one)

If I am interpreting the C++ correctly, when Lean makes the bytecode for to_repr2 $ float.one, it has written down somewhere that to_repr2 uses destructors and then inlines the destructor step in the bytecode. Therefore the native vm_declaration and the non-native vm_declaration alter the stack inconsistently.

[Edward Ayers]

(deleted)

[Edward Ayers]

After more digging, when bytecode for to_repr2 $ float.one is made, the bytecode compiler doesn't even see the constant to_repr2, the optimisation is occurring before it is fed to bytecode generator. I can't figure out which part of Lean is doing the optimising though.