nada_dsl.audit.abstract module

Abstract interpreter and type definitions for the Nada DSL auditing component.

class Metaclass

Bases: type

Metaclass for the Constant, Public, and Secret classes, enabling comparison of derived classes and conversions between them.

shape(cls_: type = None) → type

Return the shape of a class that is an instance of this metaclass.

>>> PublicInteger.shape().__name__
'Public'
>>> AbstractInteger.shape(Constant).__name__
'Integer'

__lt__(other: type) → bool

Return self<value.

__le__(other: type) → bool

Return self<=value.

class Constant

Bases: object

Class from which classes for constants are derived.

>>> Constant <= Constant
True
>>> Constant < Secret
True
>>> Constant < Secret
True
>>> Secret <= Constant
False
>>> min(Constant, Public).__name__
'Constant'

class Public

Bases: object

Class from which classes for public values are derived.

>>> Public < Secret
True
>>> Public <= Constant
False
>>> Public < Public
False
>>> min(Secret, Public).__name__
'Public'

class Secret

Bases: object

Class from which classes for constants are derived.

>>> Constant < Secret
True
>>> Public < Secret
True
>>> Secret < Secret
False
>>> max([Secret, Public, Constant]).__name__
'Secret'

class Abstract(cls: type = None)

Bases: object

Base class for abstract interpreter values. All more specific abstract value types are derived from this class.

The attributes of this class are also used as global aggregators of the signature components (parties, inputs, and outputs) during abstract execution.

>>> Abstract.initialize()
>>> party = Party("party")
>>> input = Input("input", party)
>>> output = Output(PublicInteger(input), "output", party)
>>> [
...     list(map(lambda entry: type(entry).__name__, component))
...     for component in Abstract.signature()
... ]
[['Party'], ['Input'], ['Output']]

parties = None

inputs = None

outputs = None

context = None

analysis = None

static initialize(context=None)

static party(party: Party)

static input(input: Input)

static output(output: Output)

static signature() → Tuple[list[Party], list[Input], list[Output]]

class Party(name: str)

Bases: Abstract

Abstract interpreter values corresponding to parties.

>>> isinstance(Party("party"), Party)
True

If arguments having incorrect types are supplied to the constructor, an exception is raised.

>>> Party(123)
Traceback (most recent call last):
  ...
TypeError: name parameter must be a string

class Input(name: str, party: Party)

Bases: Abstract

Abstract interpreter values corresponding to inputs.

>>> isinstance(Input("input", Party("party")), Input)
True

If arguments having incorrect types are supplied to the constructor, an exception is raised.

>>> Input(123, Party("party"))
Traceback (most recent call last):
  ...
TypeError: name parameter must be a string
>>> Input("input", 456)
Traceback (most recent call last):
  ...
TypeError: party parameter must be a Party object

class Output(value: PublicInteger | SecretInteger, name: str, party: Party)

Bases: Abstract

Abstract interpreter values corresponding to outputs.

>>> party = Party("party")
>>> input = Input("input", party)
>>> isinstance(Output(PublicInteger(input), "output", party), Output)
True

If arguments having incorrect types are supplied to the constructor, an exception is raised.

>>> Output(123, "output", party)
Traceback (most recent call last):
  ...
TypeError: output value must be a PublicInteger or a SecretInteger
>>> Output(PublicInteger(input), 123, party)
Traceback (most recent call last):
  ...
TypeError: name parameter must be a string
>>> Output(PublicInteger(input), "output", 123)
Traceback (most recent call last):
  ...
TypeError: party parameter must be a Party object

class AbstractInteger(input: Input = None, value: int = None)

Bases: Abstract

Abstract interpreter values corresponding to all integers types. This class is only used by derived classes and is not exported.

__add__(other: int | AbstractInteger) → AbstractInteger

Addition of abstract values that are instances of integer classes. The table below presents the output type for each combination of argument types.

self	other	result
Integer	Integer	Integer
Integer	PublicInteger	PublicInteger
Integer	SecretInteger	SecretInteger
PublicInteger	Integer	PublicInteger
PublicInteger	PublicInteger	PublicInteger
PublicInteger	SecretInteger	SecretInteger
SecretInteger	Integer	SecretInteger
SecretInteger	PublicInteger	SecretInteger
SecretInteger	SecretInteger	SecretInteger

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(PublicInteger(x) + PublicInteger(y)).__name__
'PublicInteger'
>>> type(PublicInteger(x) + SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + PublicInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + SecretInteger(y)).__name__
'SecretInteger'

The addition operator supports 0 as a base case in order to accommodate the built-in sum function.

>>> type(sum([PublicInteger(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([SecretInteger(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([PublicInteger(x), PublicInteger(y)])).__name__
'PublicInteger'

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> PublicInteger(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

__radd__(other: int | AbstractInteger) → AbstractInteger

Addition for cases in which the left-hand argument is not an instance of a class derived from this class.

__sub__(other: AbstractInteger) → AbstractInteger

Subtraction of abstract values that are instances of integer classes.

__rsub__(other: AbstractInteger) → AbstractInteger

Subtraction for cases in which the left-hand argument is not an instance of a class derived from this class.

__neg__() → AbstractInteger

Negation of abstract values that are instances of integer classes.

>>> x = Input("x", Party("a"))
>>> type(-Integer(x)).__name__
'Integer'
>>> type(-PublicInteger(x)).__name__
'PublicInteger'
>>> type(-SecretInteger(x)).__name__
'SecretInteger'

__mul__(other: AbstractInteger) → AbstractInteger

Multipliaction of abstract values that are instances of integer classes. The table below presents the output type for each combination of argument types.

self	other	result
Integer	Integer	Integer
Integer	PublicInteger	PublicInteger
Integer	SecretInteger	SecretInteger
PublicInteger	Integer	PublicInteger
PublicInteger	PublicInteger	PublicInteger
PublicInteger	SecretInteger	SecretInteger
SecretInteger	Integer	SecretInteger
SecretInteger	PublicInteger	SecretInteger
SecretInteger	SecretInteger	SecretInteger

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(PublicInteger(x) + PublicInteger(y)).__name__
'PublicInteger'
>>> type(PublicInteger(x) + SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + PublicInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + SecretInteger(y)).__name__
'SecretInteger'

The addition operator supports 0 as a base case in order to accommodate the built-in sum function.

>>> type(sum([PublicInteger(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([SecretInteger(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([PublicInteger(x), PublicInteger(y)])).__name__
'PublicInteger'

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> PublicInteger(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

__rmul__(other: AbstractInteger) → AbstractInteger

Addition for cases in which the left-hand argument is not an instance of a class derived from this class.

__lt__(other: AbstractInteger) → AbstractInteger

Comparison of abstract values that are instances of integer classes. The table below presents the output type for each combination of argument types.

self	other	result
Integer	Integer	Boolean
Integer	PublicInteger	PublicBoolean
Integer	SecretInteger	SecretBoolean
PublicInteger	Integer	PublicBoolean
PublicInteger	PublicInteger	PublicBoolean
PublicInteger	SecretInteger	SecretBoolean
SecretInteger	Integer	SecretBoolean
SecretInteger	PublicInteger	SecretBoolean
SecretInteger	SecretInteger	SecretBoolean

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(PublicInteger(x) < PublicInteger(y)).__name__
'PublicBoolean'
>>> type(PublicInteger(x) < SecretInteger(y)).__name__
'SecretBoolean'
>>> type(Integer(x) < Integer(y)).__name__
'Boolean'
>>> type(SecretInteger(x) < Integer(y)).__name__
'SecretBoolean'
>>> type(Integer(x) < PublicInteger(y)).__name__
'PublicBoolean'

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> PublicInteger(x) < 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

__le__(other: AbstractInteger) → AbstractBoolean

Comparison of abstract values that are instances of integer classes. See AbstractInteger.__lt__ for details and examples.

__gt__(other: AbstractInteger) → AbstractBoolean

Comparison of abstract values that are instances of integer classes. See AbstractInteger.__lt__ for details and examples.

__ge__(other: AbstractInteger) → AbstractBoolean

Comparison of abstract values that are instances of integer classes. See AbstractInteger.__lt__ for details and examples.

__eq__(other: AbstractInteger) → AbstractBoolean

Comparison of abstract values that are instances of integer classes. See AbstractInteger.__lt__ for details and examples.

__ne__(other: AbstractInteger) → AbstractBoolean

Comparison of abstract values that are instances of integer classes. See AbstractInteger.__lt__ for details and examples.

class Integer(input: Input = None, value: int = None)

Bases: AbstractInteger, Constant

Abstract values corresponding to constant integers.

>>> Integer < PublicInteger
True
>>> Integer < SecretInteger
True
>>> Integer.shape().__name__
'Constant'

Instances of this class support the use of some built-in operators.

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(Integer(x) + Integer(y)).__name__
'Integer'
>>> type(Integer(x) * Integer(y)).__name__
'Integer'
>>> type(Integer(y) + PublicInteger(x)).__name__
'PublicInteger'
>>> type(SecretInteger(x) + Integer(y)).__name__
'SecretInteger'
>>> type(PublicInteger(x) * Integer(y)).__name__
'PublicInteger'
>>> type(Integer(y) * SecretInteger(x)).__name__
'SecretInteger'

The addition operator supports 0 as a base case in order to accommodate the built-in sum function.

>>> type(sum([Integer(x), Integer(y)])).__name__
'Integer'
>>> type(sum([Integer(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([PublicInteger(x), Integer(y)])).__name__
'PublicInteger'

Concrete interpretation (with explicit values) is also supported if those values are present in the aggregate context being maintained using the static class attributes.

>>> Abstract.context = {'x': 123, 'y': 456}
>>> r = Integer(x, 123) + SecretInteger(y, 456)
>>> r.value
579
>>> r = PublicInteger(x, 123) + Integer(y, 456)
>>> r.value
579
>>> r = SecretInteger(x, 123) * Integer(y, 456)
>>> r.value
56088
>>> r = Integer(x, 123) * PublicInteger(y, 456)
>>> r.value
56088

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> Integer(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> Integer(x) * 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> 123 * Integer(x)
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

class PublicInteger(input: Input = None, value: int = None)

Bases: AbstractInteger, Public

Abstract values corresponding to public integers.

>>> Integer < PublicInteger
True
>>> PublicInteger < SecretInteger
True
>>> PublicInteger.shape().__name__
'Public'

Instances of this class support the use of some built-in operators.

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(PublicInteger(x) + PublicInteger(y)).__name__
'PublicInteger'
>>> type(PublicInteger(x) + SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + PublicInteger(y)).__name__
'SecretInteger'
>>> type(PublicInteger(x) * PublicInteger(y)).__name__
'PublicInteger'
>>> type(PublicInteger(x) * SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) * PublicInteger(y)).__name__
'SecretInteger'

The addition operator supports 0 as a base case in order to accommodate the built-in sum function.

>>> type(sum([PublicInteger(x), SecretInteger(y)])).__name__
'SecretInteger'
>>> type(sum([PublicInteger(x), PublicInteger(y)])).__name__
'PublicInteger'

Concrete interpretation (with explicit values) is also supported if those values are present in the aggregate context being maintained using the static class attributes.

>>> Abstract.context = {'x': 123, 'y': 456}
>>> r = PublicInteger(x, 123) + SecretInteger(y, 456)
>>> r.value
579
>>> r = PublicInteger(x, 123) + PublicInteger(y, 456)
>>> r.value
579
>>> r = PublicInteger(x, 123) * SecretInteger(y, 456)
>>> r.value
56088
>>> r = PublicInteger(x, 123) * PublicInteger(y, 456)
>>> r.value
56088

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> PublicInteger(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> PublicInteger(x) * 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> 123 * PublicInteger(x)
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

class SecretInteger(input: Input = None, value: int = None)

Bases: AbstractInteger, Secret

Abstract interpreter values corresponding to secret integers.

>>> SecretInteger < Integer
False
>>> PublicInteger < SecretInteger
True
>>> SecretInteger.shape().__name__
'Secret'

Instances of this class support the use of some built-in operators.

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> type(Integer(x) + SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + PublicInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) + SecretInteger(y)).__name__
'SecretInteger'
>>> type(PublicInteger(x) * SecretInteger(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) * Integer(y)).__name__
'SecretInteger'
>>> type(SecretInteger(x) * SecretInteger(y)).__name__
'SecretInteger'

Concrete interpretation (with explicit values) is also supported if those values are present in the aggregate context being maintained using the static class attributes.

>>> Abstract.context = {'x': 123, 'y': 456}
>>> r = SecretInteger(x, 123) * SecretInteger(y, 456)
>>> r.value
56088

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> SecretInteger(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> SecretInteger(x) * 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger
>>> 123 * SecretInteger(x)
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

class AbstractBoolean(input: Input = None, value: int = None)

Bases: Abstract

Abstract interpreter values corresponding to all boolean types. This class is only used by derived classes and is not exported.

if_else(true: AbstractInteger, false: AbstractInteger) → AbstractInteger

Ternary (i.e., conditional) operator. The table below presents the output type for each combination of argument types.

self	true and false	result
Boolean	Integer	Integer
Boolean	PublicInteger	PublicInteger
Boolean	SecretInteger	SecretInteger
PublicBoolean	Integer	PublicInteger
PublicBoolean	PublicInteger	PublicInteger
PublicBoolean	SecretInteger	SecretInteger
SecretBoolean	Integer	SecretInteger
SecretBoolean	PublicInteger	SecretInteger
SecretBoolean	SecretInteger	SecretInteger

>>> x = Input("x", Party("a"))
>>> y = Input("y", Party("b"))
>>> z = Input("z", Party("c"))
>>> type(PublicBoolean(x).if_else(PublicInteger(y), PublicInteger(z))).__name__
'PublicInteger'

If a value of an incompatible type is supplied to an overloaded operator, an exception is raised.

>>> PublicInteger(x) + 123
Traceback (most recent call last):
  ...
TypeError: expecting Integer, PublicInteger, or SecretInteger

class Boolean(input: Input = None, value: int = None)

Bases: AbstractBoolean, Constant

Abstract values corresponding to constant boolean values.

class PublicBoolean(input: Input = None, value: int = None)

Bases: AbstractBoolean, Public

Abstract values corresponding to public boolean values.

class SecretBoolean(input: Input = None, value: int = None)

Bases: AbstractBoolean, Secret

Abstract values corresponding to secret boolean values.

signature(source: str) → Tuple[list[Party], list[Input], list[Output]]

Return the signature of the supplied Nada program (represented as a string). The signature consists of three lists: the program’s (1) parties, (2) inputs, and (3) outputs.

>>> source = '\n'.join([
...     'from nada_dsl import *',
...     '',
...     'def nada_main():',
...     '    party1 = Party(name="Party1")',
...     '    a = SecretInteger(Input(name="a", party=party1))',
...     '    b = SecretInteger(Input(name="b", party=party1))',
...     '',
...     '    c = a * b',
...     '',
...     '    return [Output(c, "c", party1), Output(c, "d", party1)]'
... ])
>>> (ps, ins, outs) = signature(source)
>>> [p.name for p in ps]
['Party1']
>>> [i.name for i in ins]
['a', 'b']
>>> [o.name for o in outs]
['c', 'd']

If the supplied strign is not a valid Nada program, an exception is raised.

>>> source = '\n'.join([
...     'from nada_dsl import *',
...     'def nada_main():',
...     '    pass'
... ])
>>> signature(source)
Traceback (most recent call last):
  ...
ValueError: nada_main must return a sequence of outputs
>>> source = '\n'.join([
...     'def nada_main():',
...     '    pass'
... ])
>>> signature(source)
Traceback (most recent call last):
  ...
ValueError: first statement must be: from nada_dsl import *
>>> source = '\n'.join([
...     'from nada_dsl import *',
...     'def foo():',
...     '    pass'
... ])
>>> signature(source)
Traceback (most recent call last):
  ...
ValueError: nada_main must be defined