Zulip Chat Archive

Stream: general

Topic: vm overrides


view this post on Zulip Edward Ayers (Mar 08 2019 at 14:21):

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.

view this post on Zulip Mario Carneiro (Mar 08 2019 at 18:00):

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.

view this post on Zulip Mario Carneiro (Mar 08 2019 at 18:01):

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.

view this post on Zulip Edward Ayers (Mar 09 2019 at 14:34):

@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

view this post on Zulip Edward Ayers (Mar 09 2019 at 14:36):

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

view this post on Zulip Mario Carneiro (Mar 09 2019 at 18:40):

@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

view this post on Zulip Edward Ayers (Mar 10 2019 at 15:07):

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?

view this post on Zulip Mario Carneiro (Mar 10 2019 at 15:11):

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

view this post on Zulip Mario Carneiro (Mar 10 2019 at 15:15):

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

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

view this post on Zulip Mario Carneiro (Mar 10 2019 at 15:17):

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.)

view this post on Zulip Edward Ayers (Mar 10 2019 at 17:22):

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.

view this post on Zulip Edward Ayers (Mar 10 2019 at 17:35):

(deleted)

view this post on Zulip Edward Ayers (Mar 10 2019 at 18:22):

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.


Last updated: May 17 2021 at 23:14 UTC