Equal.md - Open-CP/OCP GitHub Wiki

Test of Equal Operator

Below is an example demonstrating how to generate and test the Equal operator.


To instantiate Equal operator, run

import operators.operators as op
import variables.variables as var
import solving.solving as solving

# Create input and output variables for the Equal operation
my_input, my_output = [var.Variable(2, ID=f"in{i}") for i in range(1)], [var.Variable(2, ID=f"out{i}") for i in range(1)]
# Instantiate the Equal operation
equal = op.Equal(my_input, my_output, ID='Equal')
equal.display()

To generate Python code, run

# Generate and print Python code
code = operator.generate_implementation(implementation_type="python", unroll=True)
print(f"python code: \n", "\n".join(code))    

To generate C code, run

# Generate and print C code
code = operator.generate_implementation(implementation_type="c", unroll=True)
print(f"c code: \n", "\n".join(code))

To generate and solve corresponding MILP models for differential cryptanalysis, run

# Generate and solve MILP models under different model versions
for model_v in ["diff_0", "truncated_diff"]:
    filename = f'files/milp_{operator.ID}_{model_v}.lp' 
    # Set model_version of the operator
    operator.model_version = model_v
    
    # Generate milp_constraints
    milp_constraints = operator.generate_model(model_type='milp', unroll=True)
    
    # Define objective function if weight exists
    obj_fun = operator.weight if hasattr(operator, "weight") else []print(f"MILP constraints with model_version={model_v}: \n", "\n".join(milp_constraints))
    
    # Generate MILP model
    model = solving.gen_milp_model(constraints=milp_constraints, obj_fun=obj_fun, filename=filename) 
    
    # Solve MILP model for the optimal solution
    sol, obj = solving.solve_milp(filename, solving_goal="optimize")  
    print(f"Optimal solutions:\n{sol}\nObjective function:\n{obj}")
    
    # Solve MILP model for all solutions
    sol_list, obj_list = solving.solve_milp(filename, solving_goal="all_solutions")
    print(f"All solutions:\n{sol_list}\nObjective function:\n{obj_list}\nnumber of solutions: {len(sol_list)}")

To generate and solve corresponding SAT models for differential cryptanalysis, run

# Generate and solve SAT models under different model versions
for model_v in ["diff_0", "truncated_diff"]:
    filename = f'files/sat_{operator.ID}_{model_v}.cnf'
    # Set model_version of the operator
    operator.model_version = model_v

    # Generate sat constraints
    sat_constraints = operator.generate_model(model_type='sat', unroll=True)
            
    # Define objective function if weight exists
    obj_var = operator.weight if hasattr(operator, "weight") else []
            
    # Generate SAT model
    model, variable_map = solving.gen_sat_model(constraints=sat_constraints, obj_var=obj_var, filename=filename) 
    print("variable_map in sat:\n", variable_map)
            
    # Solve SAT model for the optimal solution
    sol = solving.solve_sat(filename, variable_map, solving_goal="optimize")  
    print(f"Optimal solutions:\n{sol}")
            
    # Solve SAT model for all solutions
    sol_list = solving.solve_sat(filename, variable_map, solving_goal="all_solutions")
    print(f"All solutions:\n{sol_list}")