Commit c99b494f authored by Luc Libralesso's avatar Luc Libralesso
Browse files

add equality dag shaving + add diff constraint generation

parent 206b15f0
source 'https://rubygems.org'
gem 'slop'
gem 'pry'
gem 'rgl'
\ No newline at end of file
gem 'rgl'
gem 'union_find'
......@@ -2,18 +2,28 @@ GEM
remote: https://rubygems.org/
specs:
coderay (1.1.3)
generator (0.0.1)
lazy_priority_queue (0.1.1)
method_source (1.0.0)
pry (0.13.1)
coderay (~> 1.1)
method_source (~> 1.0)
rgl (0.5.7)
lazy_priority_queue (~> 0.1.0)
stream (~> 0.5.3)
slop (4.8.2)
stream (0.5.3)
generator
union_find (0.0.2)
PLATFORMS
ruby
DEPENDENCIES
pry
rgl
slop
union_find
BUNDLED WITH
2.1.4
require 'union_find'
require_relative '../cryptodag.rb'
require_relative '../operators/elementary.rb'
require_relative '../constraints/all.rb'
require_relative './graphviz_atomic.rb'
### DIRTY HACK (modify union_find datastructure)
class UnionFind::UnionFind
public :find_root
end
##############
def get_abstract_constraint_model(dag)
atoms = dag.atoms()
operators = dag.operators()
......@@ -11,6 +20,7 @@ def get_abstract_constraint_model(dag)
# shave dag to remove useless inputs and outputs
# atoms2,operators2 = *shave_dag(atoms, operators)
atoms2,operators2 =
*shave_equalities(
*shave_simple_input_xor(
*shave_constants_dag(
*shave_end_dag(
......@@ -18,12 +28,114 @@ def get_abstract_constraint_model(dag)
)
)
)
)
writefile_graphviz(atoms2, operators2, "test.dot")
puts "DOT FILE WRITEN"
# create model
model = create_abstract_model(atoms2, operators2)
return model
end
##
# simplifies the dag by removing equalities
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_equalities(atoms, operators)
union_find = UnionFind::UnionFind.new(Set.new(atoms))
untouched_atoms = Set.new(atoms)
operators.filter{|op| op.class <= EqualityOperator}.each do |op|
union_find.union(op.inputs[0], op.outputs[0])
untouched_atoms.delete(op.inputs[0])
untouched_atoms.delete(op.outputs[0])
end
old_to_root = {}
root_set = Set.new()
atoms.each do |a|
root_set.add(union_find.find_root(a))
old_to_root[a] = union_find.find_root(a)
end
raise "union find: inconsistent results" unless root_set.length == union_find.count_isolated_components
root_to_new = {}
new_atoms = []
root_set.each do |a|
new_a = Variable.new(a.name, 0..1, value=a.value)
root_to_new[a] = new_a
new_atoms.push(new_a)
end
puts "ELIMINATE EQUALITIES (vars: #{atoms.length} -> #{new_atoms.length})"
# define operators
new_operators = []
operators.filter{|op| !(op.class <= EqualityOperator)}.each do |op|
res = op.dup
res.inputs = op.inputs.map{|a| root_to_new[old_to_root[a]]}
res.outputs = op.outputs.map{|a| root_to_new[old_to_root[a]]}
raise "shave_equalities: different size between new and old input op #{res.inputs.length} should be #{op.inputs.length}" unless res.inputs.length == op.inputs.length
raise "shave_equalities: different size between new and old outputs op" unless res.outputs.length == op.outputs.length
res.inputs.each do |a|
raise "atom non existing in new_atoms set (input of #{res}, #{a})" unless Set.new(new_atoms).include?(a)
end
new_operators.push(res)
end
return [new_atoms, new_operators]
end
##
# returns new xors that can be used to improve the relaxations
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def generate_xors(atoms, operators, custom_xors, max_size=4)
new_xors = Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)}+custom_xors)
# new_xors.each do |x|
# p x.map{|e| e.name.name}
# end
variables = Set.new()
new_xors.each do |op|
op.each do |v|
variables.add(v)
end
end
puts "GENERATE_XORS(limit=#{max_size}): found #{new_xors.length} initial xors"
puts "\t#{variables.length} variables"
initial_xors = Set.new()
while new_xors.length > initial_xors.length
initial_xors = new_xors
variable_adj = {}
nb_links = 0
new_xors.each do |op|
op.each do |v|
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(op)
nb_links += 1
end
end
puts "\tnb links: #{nb_links}"
new_xors = initial_xors.dup
variables.each do |v|
variable_adj[v].each do |a|
variable_adj[v].each do |b|
if a != b
c = (a+b)-(a&b)
# check that c does not contain more than 2 diff variables
nb_diffs = c.filter{|v| v.name.name.start_with?("diff_")}.length
if nb_diffs <= 1
if c.length >= 1 && c.length <= max_size
# p c.map{|v|v.name.name}
new_xors.add(c)
end
end
end
end
end
end
puts "\tround finished: #{new_xors.length-initial_xors.length} added"
end
result = new_xors - (Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)})+custom_xors)
return result
end
##
# removes operators and atoms to be shaved and returns a new dag
......@@ -198,6 +310,7 @@ def create_abstract_model(atoms, operators)
raise "gen_abstract_constraint_model: unknown operator: #{op.class.name}"
end
end
# generate xors
# add objective function
s_operators = operators.filter {|op| op.class <= SOperator}
obj = Variable.new("obj", 1..20)
......@@ -209,9 +322,128 @@ def create_abstract_model(atoms, operators)
)
)
model.add_instructions(Instruction.new("solve minimize obj"))
diff_xors = add_diff_variables_mixcolumn_lines(model, atoms, operators, variable_dict)
new_xors = generate_xors(atoms, operators, diff_xors)
new_xors.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
return model
end
# def add_diff_variables()
# end
\ No newline at end of file
##
#
#
def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable)
res_xors = []
mc_operators = operators.filter{|op| op.class <= MixColumnsOperator}
op_to_ids = {}
ids_to_op = {}
id = 0
mc_operators.each do |op|
op_to_ids[op] = id
ids_to_op[id] = op
id += 1
end
puts "ADD_DIFF (MIXCOLUMN LINES)"
puts "\t#{mc_operators.length} mixColumns operators found"
diffs = []
mc_operators.each do |o1|
mc_operators.each do |o2|
if op_to_ids[o1] != op_to_ids[o2]
4.times do |row|
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"I"])
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"O"])
end
end
end
end
diffs_to_var = {}
puts "\tadding #{diffs.length} diff variables"
diffs.each do |d|
o1,o2,row,t = d[0],d[1],d[2],d[3],d[4]
diffs_to_var[d] = Variable.new("diff_m#{o1}_m#{o2}_l#{row}_#{t}", 0..1)
model.add_variables(diffs_to_var[d])
end
# add linking to original variables
diffs.each do |d|
o1,o2,row,t = d[0],d[1],d[2],d[3]
if t == "I"
model.add_constraints(Diff1.new(*[
atom_to_variable[ids_to_op[o1].inputs[row]],
atom_to_variable[ids_to_op[o2].inputs[row]],
diffs_to_var[d]
]))
res_xors.push(Set.new([
ids_to_op[o1].inputs[row],
ids_to_op[o2].inputs[row],
diffs_to_var[d]
]))
else
model.add_constraints(Diff1.new(*[
atom_to_variable[ids_to_op[o1].outputs[row]],
atom_to_variable[ids_to_op[o2].outputs[row]],
diffs_to_var[d]
]))
res_xors.push(Set.new([
ids_to_op[o1].outputs[row],
ids_to_op[o2].outputs[row],
diffs_to_var[d]
]))
end
end
# add symmetry
diffs.each do |d1|
diffs.each do |d2|
if d1[0] == d2[1] && d1[1] == d2[0] && d1[3] == d2[3] && d1[2] == d2[2] && d1[0] != d2[0]
model.add_constraints(Equality.new(
diffs_to_var[d1],
diffs_to_var[d2]
))
end
end
end
# add transitivity
mc_operators.each do |o1|
mc_operators.each do |o2|
mc_operators.each do |o3|
if o1 != o2 && o2 != o3 && o1 != o3
id1, id2, id3 = op_to_ids[o1], op_to_ids[o2], op_to_ids[o3]
4.times do |row|
["I","O"].each do |t|
vars = [
diffs_to_var[[id1,id2,row,t]],
diffs_to_var[[id1,id3,row,t]],
diffs_to_var[[id2,id3,row,t]]
]
model.add_constraints(Diff1.new(*vars))
res_xors.push(Set.new(vars))
end
end
end
end
end
end
# add mix columns property (sum diffs input + diffs output) for each couple of operators
mc_operators.each do |o1|
mc_operators.each do |o2|
id1, id2 = op_to_ids[o1], op_to_ids[o2]
if id1 < id2
model.add_constraints(IncludedIn.new(
Sum.new(
*( 4.times.map{|row| diffs_to_var[[id1,id2,row,"I"]]} + 4.times.map{|row| diffs_to_var[[id1,id2,row,"O"]]} )
), Set[0,4,5,6,7,8]
))
model.add_constraints(Equivalence.new(
Equals.new(Sum.new(*4.times.map{|row| diffs_to_var[[id1,id2,row,"I"]]}), 0),
Equals.new(Sum.new(*4.times.map{|row| diffs_to_var[[id1,id2,row,"O"]]}), 0)
))
end
end
end
# XOR(DIFFZ[i1, j, k, i2], X[i1 + 1, j, k], X[i2 + 1, j, k])
return res_xors
end
\ No newline at end of file
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