Add support for finite fields #90
Conversation
| from frame.tools.z3_template import Z3Template | ||
| import galois | ||
|
|
||
| DEFAULT_FIELD = galois.GF(27) |
There was a problem hiding this comment.
can we import this from one file, so we don't have to change it every time in the future when we generalize?
|
|
||
| DEFAULT_FIELD = galois.GF(27) | ||
|
|
||
| def get_order(a: FiniteFieldElement) -> int: |
There was a problem hiding this comment.
this would just be DEFAULT_FIELD.multiplicative_order(a.value) using the library's in-built function
| canonical_name="ff_is_primitive_element", | ||
| entity_type=EntityType.CONCEPT, | ||
| description="True if the element is a generator of the multiplicative group", | ||
| computational_implementation=lambda a: get_order(a) == (DEFAULT_FIELD.order - 1) if int(a.value) != 0 else False, |
There was a problem hiding this comment.
alternatively, return a in DEFAULT_FIELD.primitive_elements
| ff_one_concept = create_finite_field_one_concept() | ||
| ff_addition_concept = create_finite_field_addition_concept() | ||
| ff_multiplication_concept = create_finite_field_multiplication_concept() | ||
| ff_equality_concept = create_finite_field_equality_concept() |
There was a problem hiding this comment.
we also need the concept of generators. The way to get all the generators is the following.
generator = DEFAULT_FIELD.primitive_element
generators_list = [generator**i for i in range(DEFAULT_FIELD.order)]
Then you need to make a concept out of each of these generators.
There was a problem hiding this comment.
I agree this makes sense, if we can specify the field somewhere we can add a set of the generators here. Probably better to do this generally, but we can also just hardcode it if that takes too much work
No description provided.