OKlibrary  0.2.1.6
ConstraintTemplateGlobalPropagation.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 6.12.2010 (Swansea) */
00002 /* Copyright 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00023 /* TODO : Update specification below */
00024 
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteSystem.mac")$
00031 
00032 /* A propagation function takes a list of constraints and a list of variables
00033    (in most cases, the variable list for the list of constraints) and
00034    then propagates the effects of certain constraints in the constraint list
00035    across the list, returning a new constraint list after the effects
00036    have been propagated along with the new variable list for the
00037    constraint list.
00038 
00039    For example, prop_eq_csttl takes a constraint list and variable list
00040    and removes equivalence constraints by replacing the variables
00041    made equivalent (a=b) by a new variable veq(a,b) and removing the
00042    constraint.
00043 */
00044 
00045 
00046 /********************************
00047  * Propagation functions        *
00048  ********************************
00049 */
00050 
00051 /* Given a list of constraint templates, a variable list, and a list of
00052    propagation functions returns a new list of constraint templates and a new
00053    variable list after applying each propagation function to both. */
00054 prop_all_csttl(csttl, old_var_l, prop_l) :=
00055   lreduce(lambda([csttl_new,csttpb], csttpb(csttl_new[1],csttl_new[2])),
00056     prop_l,[csttl,old_var_l])$
00057 
00058 
00059 /**************************************************
00060  * Standard propagation bundles                   *
00061  **************************************************
00062 */
00063 
00064 /* Equivalence propagation */
00065 
00066 declare(veq, noun)$
00067 declare(veq, posfun)$
00068 new_veq([a]) := apply(veq, a)$
00069 
00070 /* Given a constraint template list, returns the list of new variables
00071    introduced by prop_eq_csttl.
00072 */
00073 prop_eq_vars_l(csttl) := block([cstt_eq_l,new_var_l : []],
00074   cstt_eq_l : sublist(csttl, lambda([a], cstt_named_p(a, "eq_cst"))),
00075   while cstt_eq_l # [] do block([cstt_eq_vars_l],
00076     cstt_eq : first(cstt_eq_l),
00077     cstt_eq_l : rest(cstt_eq_l),
00078     cstt_eq_var_l : cstt_vars_l(cstt_eq),
00079     eq_var_l : 
00080       partition_elements(cstt_eq_var_l, ceiling(length(cstt_eq_var_l)/2)),
00081     new_var_l : remove_elements(eq_var_l[1], new_var_l),
00082     new_var_l : remove_elements(eq_var_l[2], new_var_l),
00083     new_var_temp_l : map(new_veq, eq_var_l[1], eq_var_l[2]),
00084     new_var_l : append(new_var_l, new_var_temp_l),
00085     cstt_eq_l : csttl_rename_vars(cstt_eq_l, eq_var_l[1], new_var_temp_l),
00086     cstt_eq_l : csttl_rename_vars(cstt_eq_l, eq_var_l[2], new_var_temp_l)),
00087   return(new_var_l))$
00088 
00089 /* Given a constraint template list, returns the list of constraint templates
00090    where equality constraints (named "eq_cst") have been removed and the pairs
00091    of equivalent variables in each "eq_cst" constraint replaced with new
00092    variables (see prop_eq_csttl_vars_l).
00093 
00094    XXX
00095 */
00096 prop_eq_csttl(csttl, old_var_l) := block(
00097   [eq_csttl, var_mappings, var_map : sm2hm({}), pre_map : sm2hm({}), new_var_l, count],
00098   eq_csttl : sublist(csttl, lambda([cstt], cstt_named_p(cstt,"eq_cst"))),
00099   var_mappings :
00100     lappend(map(lambda([a], map("[",a[1],a[2])),
00101       map(lambda([a],partition_elements(a,ceiling(length(a)/2))),
00102         map(cstt_vars_l, eq_csttl)))),
00103   if oklib_monitor then print("Starting equivalence mapping!"),
00104   count : 0,
00105   for M in var_mappings do block(
00106       [M1_mapped, M2_mapped, new_var_, preexisting_maps],
00107     if oklib_monitor then print("Mapping [",count : count + 1, "/", length(var_mappings),"]"),
00108     M1_mapped : ev_hm_d(var_map,M[1], M[1]),
00109     M2_mapped : ev_hm_d(var_map,M[2], M[2]),
00110     new_var_ : new_veq(M1_mapped, M2_mapped),
00111     set_hm(var_map, M[1], new_var_),
00112     set_hm(var_map, M[2], new_var_),
00113     preexisting_maps : append(
00114       ev_hm_d(pre_map, M1_mapped, []),ev_hm_d(pre_map, M2_mapped, [])),
00115     for old_map in preexisting_maps do (
00116       set_hm(var_map, old_map, new_var_)),
00117     set_hm(pre_map, new_var_, append(preexisting_maps, [M1_mapped,M2_mapped])),
00118     del_hm(pre_map, M1_mapped), del_hm(pre_map, M2_mapped)),
00119   new_var_l : map(lambda([a], ev_hm_d(var_map,a,a)), old_var_l),
00120   csttl : csttl_rename_vars(
00121     sublist(csttl, lambda([cstt], not(cstt_named_p(cstt,"eq_cst")))),
00122       old_var_l, new_var_l),
00123   return([csttl, stable_unique(new_var_l)]))$
00124 
00125