Secrets design - optional information in `bool` and `f64`
bvssvni opened this issue · 0 comments
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 ofbool
, but keeps the secret-x
changes sign off64
, 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
withmin
/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