Secrets design - optional information in `bool` and `f64`

[bvssvni]

Dyon supports putting optional secret information in bool and f64 that is unlocked with two intrinsics:

• fn why(var: sec[bool]) -> [any] { ... }
• fn where(var: sec[f64]) -> [any] { ... }

The ∀/all, ∃/any, min, max loops uses this to insert index information.

where intrinsic

A where intrinsic gives you the secret of a number. The secret is automatically derived from the composition of loops:

// Find smallest value in 2D array.
list := [[1, 0], [-1, 2]]
x := min i, j { list[i][j] }
arg := where(x)
println(arg) // prints `[1, 0]`
println(list[arg[0]][arg[1]] == x) // prints `true`

If a list is empty, the min/max loop will return NaN:

list := []
x := min i { list[i] }
println(where(x)) // ERROR: Expected `number`, found `NaN`

The secret of a number can only be unlocked if the value is not NaN.

You can use the ? operator to propagate the error message:

fn foo(list: []) -> res {
    x := min i { list[i] }
    // if list is empty, returns `err("Expected `number`, found `NaN`")`
    println(where(x?))
    return ok("success!")
}

The ? operator can also be useful in numerical calculations to check for division of zero by zero.

why intrinsic

The why intrinsic gives you a secret of a bool. The secret is derived from composition of loops:

// Find the value in 2D array that is less than zero.
list := [[1, 0], [-1, 2]]
x := ∃ i, j { list[i][j] < 0 }
arg := why(x)
println(arg) // prints `[1, 0]`
println(list[arg[0]][arg[1]] < 0) // prints `true`

If the list is empty, the ∀/all loop will return true and ∃/any will return false.

list := []
x := ∃ i { list[i] > 0 }
println(why(x)) // ERROR: This does not make sense, perhaps an array is empty?

You can use the ? operator to propagate the error message:

fn foo(list: []) -> res {
    x := ∃ i { list[i] > 0 }
    // If list is empty,
    // returns `err("This does not make sense, perhaps an array is empty?")`
    println(why(x?))
    return ok("success!")
}

The why intrinsics only unlocks the secret if the value is true. When using a ∀/all loop you must ask "why not":

x := ∀ i { list[i] > 0 }
println(why(!x))

The ? operator is evaluated after !:

x := ∀ i { list[i] > 0 }
println(why(!x?)) // works because `x` is inverted before `?`

When combining ∀/all loops with ∃/any loops, the secret will only propagate for true values, such that the meaning is preserved:

// Find the list where all values are positive.
list := [[1, 2], [-1, 2]]
x := ∃ i { ∀ j { list[i][j] > 0 } }
println(why(x)) // prints `[0]` because that's the list.

By inverting the result of a ∀/all loop the secret is propagated:

// Find the list where not all values are positive.
list := [[1, 2], [-1, 2]]
x := ∃ i { !∀ j { list[i][j] > 0 } }
println(why(x)) // prints `[1, 0]` because that's where we find `-1`.

Binary operators

A secret propagates from the left argument in binary operators:

// Find the list where the minimum value is less than zero.
list := [[1, 0], [-1, 2]]
x := ∃ i { min j { list[i][j] } < 0 }
println(why(x)) // prints `[1, 0]` because that's where -1 is, which is the minimum value.

If we swap sides, the secret is lost from the inner min loop:

// Find the list where zero is greater or equal to the minimum value of the list.
list := [[1, 0], [-1, 2]]
x := ∃ i { 0 >= min j { list[i][j] } }
println(why(x)) // prints `[1]` because that's where the list is

Unary operator

• !x inverts the value of bool, but keeps the secret
• -x changes sign of f64, but keeps the secret

explain_why intrinsic

Puts a secret with a bool:

reason := "just because"
x := explain_why((1+1)==2, reason)
println(why(x)) // prints `["just because"]`

explain_where intrinsic

Puts a secret with a f64:

reason := "the number is 2"
x := explain_where(2, reason)
println(where(x)) // prints `["the number is 2"]`

Returning values

Secrets are leaked when assigned to return. A function calling another can inspect what the other function was doing, which makes it easier to debug and write custom search/solvers.

Motivation

These rules are designed for:

• Unifying ∀/all, ∃/any with min/max
• Simplifies algorithms for problem solving
• Improved performance for these loops
• Easy to read
• Reduce bugs
• Reduce typing
• Make debugging easier
• Optional safety for edge cases
• Automatically derive meaningful answers