Rahul/finite fields

frame/configs/ff_generate_interestingness_funsearch.yaml

@@ -30,11 +30,13 @@ initial_state:
   concepts:
     - "create_finite_field_zero_concept"
     - "create_finite_field_one_concept"
-    - "create_finite_field_three_concept"
-    - "create_finite_field_nine_concept"
+    - "create_finite_field_alpha_concept"
+    - "create_finite_field_alpha_squared_concept"
     - "create_finite_field_addition_concept"
     - "create_finite_field_multiplication_concept"
-    - "create_finite_field_equality_concept" 
+    - "create_finite_field_equality_concept"
+    - "create_finite_field_additive_inverse_concept"
+    - "create_finite_field_multiplicative_inverse_concept"
 
 # Experiment settings override
 experiment:

frame/configs/theory_building/initial_state/finite_field_basic.yaml

@@ -9,8 +9,10 @@ import_from: "frame.knowledge_base.initial_concepts"
 concepts:
   - "create_finite_field_zero_concept"
   - "create_finite_field_one_concept"
-  - "create_finite_field_three_concept"
-  - "create_finite_field_nine_concept"
+  - "create_finite_field_alpha_concept"
+  - "create_finite_field_alpha_squared_concept"
   - "create_finite_field_addition_concept"
   - "create_finite_field_multiplication_concept"
-  - "create_finite_field_equality_concept" 
+  - "create_finite_field_equality_concept" 
+  - "create_finite_field_additive_inverse_concept"
+  - "create_finite_field_multiplicative_inverse_concept"

frame/environments/FF/calculations.py

@@ -1,60 +1,84 @@
 from typing import Dict
 from frame.environments.ground_truth_types import GroundTruthEntity, EntityType
-from frame.knowledge_base.entities import FiniteFieldElement
+from frame.knowledge_base.entities import FiniteFieldElement, DEFAULT_FINITE_FIELD
 from frame.tools.z3_template import Z3Template
 import galois
 
-DEFAULT_FIELD = galois.GF(27)
-
-def get_order(a: FiniteFieldElement) -> int:
-    """Computes the multiplicative order of a finite field element."""
-    if a.value == 0:
-        return 1  # By convention for this context
-    if a.value == 1:
-        return 1
-
-    # The galois library stores elements as numpy arrays, so we extract the int
-    element_val = int(a.value)
-    one_val = int(DEFAULT_FIELD(1))
-
-    count = 1
-    val = element_val
-    while val != one_val:
-        val = (val * element_val) % DEFAULT_FIELD.order
-        count += 1
-    return count
 
 FF_CALCULATIONS: Dict[str, GroundTruthEntity] = {
     # TODO: Add discovered_names for these concepts
+    "ff_add_zero": GroundTruthEntity(
+        canonical_name="ff_add_zero",
+        entity_type=EntityType.CONCEPT,
+        description="Addition of finite field element with zero",
+        computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)),
+        z3_translation=lambda a: Z3Template(f"", a), 
+        discovered_names={"specialized_(ff_add_at_0_to_ff_zero)", "specialized_(ff_add_at_1_to_ff_zero)" }
+    ),
+    "ff_add_one": GroundTruthEntity(
+        canonical_name="ff_add_one",
+        entity_type=EntityType.CONCEPT,
+        description="Addition of finite field element with one",
+        computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)),
+        z3_translation=lambda a: Z3Template(f"", a), 
+        discovered_names={"specialized_(ff_add_at_0_to_ff_one)", "specialized_(ff_add_at_1_to_ff_one)" }
+    ),
+    "ff_add_alpha": GroundTruthEntity(
+        canonical_name="ff_add_alpha",
+        entity_type=EntityType.CONCEPT,
+        description="Addition of finite field element with alpha",
+        computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)),
+        z3_translation=lambda a: Z3Template(f"", a), 
+        discovered_names={"specialized_(ff_add_at_0_to_ff_alpha)", "specialized_(ff_add_at_1_to_ff_alpha)" }
+    ),
+    "ff_add_alpha_squared": GroundTruthEntity(
+        canonical_name="ff_add_alpha_squared",
+        entity_type=EntityType.CONCEPT,
+        description="Addition of finite field element with alpha squared",
+        computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(9)),
+        z3_translation=lambda a: Z3Template(f"", a), 
+        discovered_names={"specialized_(ff_add_at_0_to_ff_alpha_squared)", "specialized_(ff_add_at_1_to_ff_alpha_squared)" }
+    ),
     "ff_power": GroundTruthEntity(
         canonical_name="ff_power",
         entity_type=EntityType.CONCEPT,
         description="Exponentiation of finite field elements",
         computational_implementation=lambda a, n: a ** n,
+        discovered_names={"iterate_(ff_multiply_with_ff_one)"},
     ),
     "ff_subtract": GroundTruthEntity(
         canonical_name="ff_subtract",
         entity_type=EntityType.CONCEPT,
         description="Subtraction of finite field elements",
+        discovered_names={"compose_(ff_additive_inverse_with_ff_add_output_to_input_map={0: 1})"},
         computational_implementation=lambda a, b: a - b,
     ),
-    "ff_inverse": GroundTruthEntity(
-        canonical_name="ff_inverse",
+    "ff_division": GroundTruthEntity(
+        canonical_name="ff_division",
+        entity_type=EntityType.CONCEPT,
+        description="Division of finite field elements",
+        discovered_names={"compose_(ff_multiplicative_inverse_with_ff_multiply_output_to_input_map={0: 1})"},
+        computational_implementation=lambda a, b: a / b,
+    ),
+    "ff_square": GroundTruthEntity(
+        canonical_name="ff_square",
         entity_type=EntityType.CONCEPT,
-        description="Multiplicative inverse of a finite field element",
-        computational_implementation=lambda a: a.inverse() if int(a.value) != 0 else FiniteFieldElement(0),
+        description="Square of a finite field element",
+        computational_implementation=lambda a: a * a,
+        discovered_names={"matched_(ff_multiply_indices_[0, 1])", "specialized_(ff_power_at_1_to_two)"}
     ),
     "ff_frobenius_map": GroundTruthEntity(
         canonical_name="ff_frobenius_map",
         entity_type=EntityType.CONCEPT,
         description="The Frobenius automorphism x -> x^3",
         computational_implementation=lambda a: a ** 3,
+        discovered_names={"specialized_(ff_power_at_1_to_three)"}
     ),
     "ff_element_order": GroundTruthEntity(
         canonical_name="ff_element_order",
         entity_type=EntityType.CONCEPT,
         description="The multiplicative order of a finite field element",
-        computational_implementation=get_order,
+        computational_implementation=lambda a: DEFAULT_FINITE_FIELD.multiplicative_order(a.value),
     ),
 }
 
@@ -64,19 +88,21 @@ def get_order(a: FiniteFieldElement) -> int:
         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,
+        computational_implementation=lambda a: DEFAULT_FINITE_FIELD.multiplicative_order(a.value) == DEFAULT_FINITE_FIELD.order - 1,
     ),
     "ff_is_square": GroundTruthEntity(
         canonical_name="ff_is_square",
         entity_type=EntityType.CONCEPT,
         description="True if the element is a square",
-        computational_implementation=lambda a: a.is_square(),
+        computational_implementation=lambda a: DEFAULT_FINITE_FIELD.is_square(a.value),
+        discovered_names={"exists_(ff_square_indices_[0])"}
     ),
     "ff_is_cube": GroundTruthEntity(
         canonical_name="ff_is_cube",
         entity_type=EntityType.CONCEPT,
         description="True if the element is a cube",
-        computational_implementation=lambda a: a in {e*e*e for e in DEFAULT_FIELD.elements},
+        computational_implementation=lambda a: a in {e*e*e for e in DEFAULT_FINITE_FIELD.elements},
+        discovered_names={"exists_(ff_frobenius_map_indices_[0])"}
     ),
 }
 

frame/environments/FF/operations.py

@@ -1,6 +1,6 @@
 from typing import Dict
 from frame.environments.ground_truth_types import GroundTruthEntity, EntityType
-from frame.knowledge_base.entities import FiniteFieldElement
+from frame.knowledge_base.entities import FiniteFieldElement, DEFAULT_FINITE_FIELD
 from frame.tools.z3_template import Z3Template
 
 FF_FUNCTIONS: Dict[str, GroundTruthEntity] = {
@@ -9,26 +9,28 @@
         entity_type=EntityType.CONCEPT,
         description="Addition of finite field elements",
         computational_implementation=lambda a, b: a + b,
-        z3_translation=lambda a, b: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field addition
-            params 2;
-            bounded params 0;
-            ReturnExpr x_0 + x_1;
-            ReturnPred None;
-        """, a, b)
+        z3_translation=lambda a, b: Z3Template(f"", a, b)
     ),
     "ff_multiply": GroundTruthEntity(
         canonical_name="ff_multiply",
         entity_type=EntityType.CONCEPT,
         description="Multiplication of finite field elements",
         computational_implementation=lambda a, b: a * b,
-        z3_translation=lambda a, b: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field multiplication
-            params 2;
-            bounded params 0;
-            ReturnExpr x_0 * x_1;
-            ReturnPred None;
-        """, a, b)
+        z3_translation=lambda a, b: Z3Template(f"", a, b)
+    ),
+    "ff_additive_inverse": GroundTruthEntity(
+        canonical_name="ff_additive_inverse",
+        entity_type=EntityType.CONCEPT,
+        description="Additive inverse of a finite field element",
+        computational_implementation=lambda a: -a,
+        z3_translation=lambda a: Z3Template(f"", a)
+    ),
+    "ff_multiplicative_inverse": GroundTruthEntity(
+        canonical_name="ff_multiplicative_inverse",
+        entity_type=EntityType.CONCEPT,
+        description="Multiplicative inverse of a finite field element",
+        computational_implementation=lambda a: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) / a,
+        z3_translation=lambda a: Z3Template(f"", a)
     ),
 }
 
@@ -38,13 +40,7 @@
         entity_type=EntityType.CONCEPT,
         description="Equality of finite field elements",
         computational_implementation=lambda a, b: a == b,
-        z3_translation=lambda a, b: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field equality
-            params 2;
-            bounded params 0;
-            ReturnExpr None;
-            ReturnPred x_0 == x_1;
-        """, a, b)
+        z3_translation=lambda a, b: Z3Template(f"", a, b)
     ),
 }
 
@@ -53,52 +49,28 @@
         canonical_name="ff_zero",
         entity_type=EntityType.CONCEPT,
         description="The zero element in the finite field",
-        computational_implementation=lambda: FiniteFieldElement(0),
-        z3_translation=lambda: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field zero
-            params 0;
-            bounded params 0;
-            ReturnExpr 0;
-            ReturnPred None;
-        """)
+        computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)),
+        z3_translation=lambda: Z3Template(f"")
     ),
     "ff_one": GroundTruthEntity(
         canonical_name="ff_one",
         entity_type=EntityType.CONCEPT,
         description="The one element in the finite field",
-        computational_implementation=lambda: FiniteFieldElement(1),
-        z3_translation=lambda: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field one
-            params 0;
-            bounded params 0;
-            ReturnExpr 1;
-            ReturnPred None;
-        """)
+        computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)),
+        z3_translation=lambda: Z3Template(f"")
     ),
-    "ff_three": GroundTruthEntity(
-        canonical_name="ff_three",
+    "ff_alpha": GroundTruthEntity(
+        canonical_name="ff_alpha",
         entity_type=EntityType.CONCEPT,
-        description="The three element in the finite field",
-        computational_implementation=lambda: FiniteFieldElement(3),
-        z3_translation=lambda: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field three
-            params 0;
-            bounded params 0;
-            ReturnExpr 3;
-            ReturnPred None;
-        """)
+        description="The alpha element in the finite field",
+        computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)),
+        z3_translation=lambda: Z3Template(f"")
     ),
-    "ff_nine": GroundTruthEntity(
-        canonical_name="ff_nine",
+    "ff_alpha_squared": GroundTruthEntity(
+        canonical_name="ff_alpha_squared",
         entity_type=EntityType.CONCEPT,
-        description="The nine element in the finite field",
-        computational_implementation=lambda: FiniteFieldElement(9),
-        z3_translation=lambda: Z3Template(f"""
-            # TODO: Implement Z3 translation for finite field nine
-            params 0;
-            bounded params 0;
-            ReturnExpr 9;
-            ReturnPred None;
-        """)
+        description="The alpha squared element in the finite field",
+        computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(9)),
+        z3_translation=lambda: Z3Template(f"")
     ),
 } 

frame/environments/FF/repl_commands.txt

@@ -0,0 +1,50 @@
+apply iter successor
+apply iter add zero
+apply match add indices_to_match=[0,1]
+apply match multiply indices_to_match=[0,1]
+apply specialize successor zero index_to_specialize=0
+apply specialize successor one index_to_specialize=0
+apply specialize successor two index_to_specialize=0
+apply specialize successor three index_to_specialize=0
+apply specialize successor four index_to_specialize=0
+apply specialize successor five index_to_specialize=0
+apply specialize successor six index_to_specialize=0
+apply specialize successor seven index_to_specialize=0
+apply specialize successor eight index_to_specialize=0
+apply specialize successor nine index_to_specialize=0
+apply specialize successor ten index_to_specialize=0
+apply specialize successor eleven index_to_specialize=0
+apply specialize successor twelve index_to_specialize=0
+apply specialize successor thirteen index_to_specialize=0
+apply specialize successor fourteen index_to_specialize=0
+apply specialize successor fifteen index_to_specialize=0
+apply specialize successor sixteen index_to_specialize=0
+apply specialize successor seventeen index_to_specialize=0
+apply specialize successor eighteen index_to_specialize=0
+apply specialize successor nineteen index_to_specialize=0
+apply specialize successor twenty index_to_specialize=0
+apply specialize successor twenty_one index_to_specialize=0
+apply specialize successor twenty_two index_to_specialize=0
+apply specialize successor twenty_three index_to_specialize=0
+apply specialize successor twenty_four index_to_specialize=0
+apply specialize successor twenty_five index_to_specialize=0
+apply specialize successor twenty_six index_to_specialize=0
+apply iter multiply one
+
+
+apply specialize ff_add ff_zero index_to_specialize=0
+apply specialize ff_add ff_one index_to_specialize=0
+apply specialize ff_add ff_alpha index_to_specialize=0
+apply specialize ff_add ff_alpha_squared index_to_specialize=0
+apply iter ff_multiply ff_one
+apply compose ff_additive_inverse ff_add output_to_input_map={0:1}
+apply compose ff_multiplicative_inverse ff_multiply output_to_input_map={0:1}
+apply specialize ff_power two index_to_specialize=1
+apply specialize ff_power three index_to_specialize=1
+apply specialize ff_power twenty_seven index_to_specialize=1
+apply exists ff_square indices_to_quantify=[0]
+apply exists ff_frobenius_map indices_to_quantify=[0]
+
+
+
+