Bolt does not support three valued logic (3VL)

[mm-gmbd]

Apologies for the crappy title. Maybe after some thinking I'll come up with something more specific. Anyways, onto the question/issue.

I think this is really an issue for Firebase rules in general, but since I came across it while using Bolt, I figured I'd at least jot it down here to start. And again, onto the issue :)

I have a Firebase that includes users and devices, and users can be either type admin or standard. An admin user can access data from all devices, whereas a standard user can only access the devices that claim him/her as the owner (devices/$device/owner).

A small (but necessary) wrinkle in my data structure is that a single device can have multiple identities, or rather, one day, it's identifier could be "$device1" and the next day it could be "$device4" (although it can have multiple identifies, it can only be one identity at one time).

There is also a never-changing, always-unique identifier that represents that device, let's call it "$uniqueDevice1", and it has it's own tree, and it's value represents the current changeable identity of the device.

So, for example:

• user1 owns device1
• user2 owns device4
• user0 is admin, and has access to all devices
• device1 and device4 are actually both representations of uniqueDevice1
• uniqueDevice1 is currently being represented by device4

users: {
  user0: {
    userType: 'admin'
  },
  user1: {
    userType: 'standard`
    devices: {
      device1: true,
    }
  },
  user2: {
    userType: 'standard'
    devices: {
      device4: true
    }
  }
}

devices: {
  device1: {
    owner: user1
    data: "I'm device 1!",
    uniqueDevice: "uniqueDevice1"
  },
  device4: {
    owner: user2
    data: "I'm device 4!",
    uniqueDevice: "uniqueDevice1"
  }
}

uniqueInformation: {
  uniqueDevice1: {
    information: "some information 1"
  },
  otherUniqueDevice: {
    information: "some other information"
  }
}

uniqueDevices: {
  uniqueDevice1: device4
}

Here are my read rules for accessing devices/$device/data:

path /devices/$device/data: {
  read() = readRules($device);
}

//Allows an owner of the device or an admin to read device data
function readRules(device) {
   return (auth != null && root.users[auth.uid].userType == 'standard' && root.devices[device].owner == auth.uid) ||
             (auth != null && root.users[auth.uid].userType == 'admin');
}

You can see that, regardless of which "non-unique" device the "unique" device is representing, user1 can access device1/data, and user2 can access device4/data. Also, the admin can access data from both devices.

Now, here are my read rules for accessing uniqueInformation/$uniqueDevice/information:

path /uniqueInformation/$uniqueDevice/information: {
  read() = uniqueReadRules($uniqueDevice);
}

//Allows an owner of the device to read information, IF ANY ONLY IF the device they own is currently being represented by the unique device. Also allows admin to read information
function uniqueReadRules(uniqueDevice){
  return (auth != null && root.users[auth.uid].userType == 'standard' && root.devices[root.uniqueDevices[uniqueDevice]].owner == auth.uid) ||
             (auth != null && root.users[auth.uid].userType == 'admin');
}

This is almost the exact same as readRules, but with the difference that the value passed to root.devices[//here//] is root.unqiueDevices[uniqueDevice], rather than just device.

So, here is the issue. If the value of uniqueDevices/$uniqueDevice is not set in Firebase, the admin is rejected from reading /uniqueInformation/$uniqueDevice/information, even though the rule is OR'd with root.users[auth.uid].userType == 'admin.

I presume because this is the equivalent of the following:

root.devices[null].owner == auth.uid || root.users[auth.uid].userType == 'admin'

And because null is passed into root.devices, then the rule totally bombs out. I'm pretty sure I'm correct on this, because if I simply arrange my rules so that the admin check comes first, then even if the value for uniqueDevices/$uniqueDevice is null in Firebase, the admin can still read uniqueInformation/$uniqueDevice/information.

So, I guess the question is, in what cases do Firebase rules totally bomb out and ignore the rest of the rules, even if there is still AND'ing and OR'ing to be done?

[mckoss]

See https://en.wikipedia.org/wiki/Three-valued_logic

Bolt (and Firebase) will fail any rule that dereferences a null value. You're correct - it would be nicer to support 3VL - but at some expense of blowing up some rules. It's something we can investigate, or perhaps make an option to the compiler.

You can fix it by writing compound expressions yourself.

[mm-gmbd]

@mckoss, thanks for the explanation, wasn't aware of three-valued logic. Learn something every day :)

As for the compound expressions, I presume you mean (in this case), checking the value of the the key before using it to dereference?

path /uniqueInformation/$uniqueDevice/information: {
  read() = uniqueReadRules($uniqueDevice);
}

//Allows an owner of the device to read information, IF ANY ONLY IF the device they own is currently being represented by the unique device. Also allows admin to read information
function uniqueReadRules(uniqueDevice){
  return (auth != null && 
          root.users[auth.uid].userType == 'standard' && 
          root.uniqueDevices[uniqueDevice] !== null && //ADDED THIS RULE
          root.devices[root.uniqueDevices[uniqueDevice]].owner == auth.uid) ||
          (
            auth != null && 
            root.users[auth.uid].userType == 'admin'
          );
}

In this case, will it automatically fall past the next statement (that originally failed) and into the OR?

[mckoss]

Yes. Our rules are "short circuiting":

a && b => if !a, then b never evaluated. a || b => if a, then b never evaluated.

Bolt preserves the ordering of expressions when generating expressions, so you can depend on the order of evaluation to use short-circuiting to avoid dereferencing null values.

If you example above, you might also need to add the check:

root.devices[root.uniqueDevices[uniqueDevice]] != null

before referencing the owner field.

This is kind of a pain to do, I know - which is one reason we've considering applying 3VL to allow you to use "undefined" values in expressions.