API Documentation

Main module.

z3_armor.entrypoint(argv=None)[source]

Entrypoint for command line interface.

Parameters:: argv (Sequence[str] | None) –
Return type:: None

class z3_armor.Constraint[source]

Bases: ABC

abstract __str__()[source]

Representation of the constraint.

Return type:: str

abstract apply(terms)[source]

Apply terms an BitVec Array.

Parameters:: terms (List[BitVec]) –
Return type:: BoolRef

abstract check(secret)[source]

Check the password.

Parameters:: secret (bytes) –
Return type:: bool

class z3_armor.Z3Armor(secret, random_state=None)[source]

Bases: object

Parameters:

secret (bytes) –
random_state (int | None) –

__init__(secret, random_state=None)[source]

Instantiated Z3Armor.

Parameters:

secret (bytes) –
random_state (int | None) –

Return type:

None

__str__()[source]

Represent the ConstraintGenerator.

Return type:: str

solver()[source]

Create the solver.

Return type:: Tuple[Solver, List[BitVec]]

verify(secret)[source]

Verify a password on the constraint generator.

Parameters:: secret (bytes) –
Return type:: bool

complete()[source]

Check that the solver has a valid unique solution.

Return type:: bool

solutions()[source]

Find all solution for the currents constraints.

Return type:: Iterator[bytes]

weights()[source]

Computes the weights of each index.

Return type:: List[float]

generate(rand=None)[source]

Generate a new constraint and it into the generator.

Parameters:: rand (Random | None) –
Return type:: Constraint

fit()[source]

Make solver sat.

Return type:: None

weighted_sampling(rand, k)[source]

Get index using sampling.

Parameters:

rand (Random) –
k (int) –

Return type:

List[int]

reduce()[source]

Minimize the number of constraints.

Return type:: None

format(name)[source]

Format the algorithm with the premade template.

Parameters:: name (str) –
Return type:: str

format_from_path(path)[source]

Format the algorithm with template on filesystem.

Parameters:: path (str | Path) –
Return type:: str

format_from_template(template)[source]

Format the algorithm with the provided template.

Parameters:: template (Template) –
Return type:: str