Commit 03ba29cf authored by Luc Libralesso's avatar Luc Libralesso
Browse files

add model shaving

parent 56704c5d
......@@ -13,7 +13,7 @@ require "pry"
class TestWriterGraphviz < Minitest::Unit::TestCase
def test_a()
dag = Midori128_Dag.new(nb_rounds=4)
dag = Midori128_Dag.new(nb_rounds=3)
model = get_abstract_constraint_model(dag)
file = File.open("test.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
......
......@@ -7,8 +7,17 @@ require_relative './graphviz_atomic.rb'
def get_abstract_constraint_model(dag)
atoms = dag.atoms()
operators = dag.operators()
# atoms2,operators2 = *[atoms,operators]
# shave dag to remove useless inputs and outputs
atoms2,operators2 = *shave_dag(atoms, operators)
# atoms2,operators2 = *shave_dag(atoms, operators)
atoms2,operators2 =
*shave_simple_input_xor(
*shave_constants_dag(
*shave_end_dag(
atoms, operators
)
)
)
writefile_graphviz(atoms2, operators2, "test.dot")
# create model
model = create_abstract_model(atoms2, operators2)
......@@ -16,6 +25,117 @@ def get_abstract_constraint_model(dag)
end
##
# removes operators and atoms to be shaved and returns a new dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def get_dag_subset(atoms, operators, to_shave)
# create new dag with shaved nodes
atom_map = {}
new_atoms = []
# create new set of atoms
atoms.each do |atom|
if !to_shave.include?(atom)
new_atom = Variable.new(atom.name, 0..1, value=atom.value)
atom_map[atom] = new_atom
new_atoms.push(new_atom)
end
end
# create new set of operators
new_operators = []
operators.each do |op|
if !to_shave.include?(op)
new_inputs = op.inputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_outputs = op.outputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_op = op.dup
# p "#{op.class <= XorOperator}\t#{new_inputs.length}"
if (op.class <= XorOperator) && (new_inputs.length == 1)
# p "###"
raise "get_dag_subset: node with multiple outputs detected #{op}" unless new_outputs.length == 1
new_op = EqualityOperator.new(new_inputs[0], new_outputs[0])
else
new_op.inputs = new_inputs
new_op.outputs = new_outputs
end
new_operators.push(new_op)
end
end
return [new_atoms, new_operators]
end
##
# simplifies the dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_simple_input_xor(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes with 1 output which is a xor
inputs = atoms.filter do |n|
preds.fetch(n, []).length == 0 &&
succs.fetch(n, []).length == 1 &&
succs.fetch(n, [])[0].class <= XorOperator
end
# for each input, replace the xor by
to_shave = Set.new()
inputs.each do |atom|
to_shave.add(atom)
to_shave.add(succs[atom][0])
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes constants from the input nodes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_constants_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
constants = atoms.filter{ |n| n.value != nil }
to_shave = Set.new() # nodes to remove in the shaved model
constants.each do |c|
to_shave.add(c)
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes end operators and atoms before S-boxes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_end_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
outputs = atoms.filter{ |n| succs.fetch(n, []).empty? }
to_shave = Set.new() # nodes to remove in the shaved model
outputs.each do |output_atom|
if preds[output_atom].length == 0
to_shave.add(output_atom)
elsif preds[output_atom].length == 1
op = preds[output_atom][0]
# if op is not a SOperator and has only one output, the atom (and operator) can be shaved
if !(op.class <= SOperator) && (succs[op].length == 1)
to_shave.add(output_atom)
to_shave.add(op)
end
else
raise "shave_end_dag: output #{output_atom.name.name} has too many preds (#{preds[output_atom]} should be <= 1)"
end
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes operators and atoms before the initial S-box
# this function is used to simplify as possible step1 models (less equivalent solutions)
......@@ -71,9 +191,17 @@ def shave_dag(atoms, operators)
new_atoms.push(new_input)
new_op.inputs = [new_input]
else
new_op.inputs = op.inputs
.filter{|ivar| !to_shave.include?(ivar)}
.map{|ivar| atom_map[ivar]}
# if xor operator with only one input, change it to equality
if op.class <= XorOperator && op.inputs.filter{|ivar| !to_shave.include?(ivar)}.length == 1
new_op = EqualityOperator.new(
op.inputs.filter{|ivar| !to_shave.include?(ivar)}.map{|ivar| atom_map[ivar]}[0],
new_op.outputs[0]
)
else
new_op.inputs = op.inputs
.filter{|ivar| !to_shave.include?(ivar)}
.map{|ivar| atom_map[ivar]}
end
end
new_operators.push(new_op)
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment