md5.pl

%% TODO
% - put simplificatin in the loop for bitlist_add
% - get per-step test cases
% - make the top level tests pass

%%%%
%%%% test cases
%%%%

%test(top_driver,[[var(a),var(b),1,0,1,0,0,1,0,0,0,1,0,1,0,1,0,1,0,0,0,1,1,0,1,0,0,0,0,0,1,1,0,0,0,1,1,0,1,1,1,0,0,1,1,1,1,1,1,0,0,1,1,0,0,1,0,1,1,1,0,1,0,1,1,1,0,0,0,1,0,0,1,0,1,1,1,0,0,1,1,1,0,1,1,0,0,0,0,0,0,0,1,0,1,1,1,0,0,0,1,0,1,0,1,0,0,0,0,0,1,1,1,1,1,1,1,0,1,0,0,1,1,1,0,1,0,1]], cats).
test(top_driver,[[0,0,1,0,1,0,0,1,0,0,0,1,0,1,0,1,0,1,0,0,0,1,1,0,1,0,0,0,0,0,1,1,0,0,0,1,1,0,1,1,1,0,0,1,1,1,1,1,1,0,0,1,1,0,0,1,0,1,1,1,0,1,0,1,1,1,0,0,0,1,0,0,1,0,1,1,1,0,0,1,1,1,0,1,1,0,0,0,0,0,0,0,1,0,1,1,1,0,0,0,1,0,1,0,1,0,0,0,0,0,1,1,1,1,1,1,1,0,1,0,0,1,1,1,0,1,0,1]], [0,1,1,0,0,1,1,0,0,0,1,0,0,1,0,1,1,0,0,0,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,1,0,1,1,1,0,1,1,0,1,1,1,0,1,0,1,0,0,0,1,1,1,0,0,1,1,0,1,0,0,0,1,0,1,0,1,0,1,1,1,1,1,1,1,0,1,0,0,1,0,1,1,0,0,1,1,1,1,1,1,1,0,1,1,1,0,1,0,0,1,1,0,1,1,1,1,0,1,0,0]).
%test(top_driver,[[1,0,1,1,1,0,0,1,0,1,0,1,1,0,0,1,1,1,1,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,1,1,0,1,0,0,0,1,1,1,1,0,1,0,1,0,0,0,1,0,1,1,0,0,1,1,0,1,0,1,0,0,1,1,0,0,1,0,0,1,1,0,0,0,0,1,0,0,0,1,0,1,0,1,1,0,0,1,0,1,0,1,1,0,1,1,1,0,1,0,0,0,0,1,1,1,1,1,1,0,0,0,1,0,0,1,0,1,0,1,1,0]], [1,0,1,0,1,1,0,1,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,1,1,0,1,0,1,0,0,1,0,1,1,0,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,1,0,1,0,0,0,1,0,0,1,1,1,1,0,1,1,0,1,1,0,1,0,1,1,1,0,1,1,1,0,0,1,1,1,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,0,0,1,0,1,0,1,1,0,1,0,1,0,1,0,0,0,1,1,0,1,1,0,0,0,1,1]).
%test(top_driver,[[1,1,1,0,1,1,0,0,0,1,1,0,1,0,0,1,0,1,1,0,1,0,1,0,1,1,0,0,1,1,0,0,1,1,1,0,0,1,1,0,1,1,1,1,1,1,0,0,1,0,0,1,1,0,1,0,0,1,0,1,0,1,1,1,1,0,1,1,1,1,0,0,1,1,0,0,1,0,1,1,0,1,0,0,1,0,1,1,1,1,0,1,0,0,0,0,0,1,1,1,0,0,0,0,1,0,1,1,1,0,1,1,0,0,1,1,1,0,1,0,1,0,1,1,0,0,0,0]], [1,0,0,1,1,1,0,0,0,0,0,1,0,1,0,1,0,0,1,1,1,1,1,1,0,1,1,0,0,1,1,0,1,0,1,1,0,1,0,1,0,1,0,1,1,0,0,0,1,0,0,0,0,1,0,0,0,0,0,1,0,0,0,0,0,1,0,0,1,0,0,1,1,1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1,1,1,0,1,0,0,1,0,0,0,0,0,1,1,1,0,0,1,0,0,0,1,1,1,0,1,0,1,0,1,1,0,0,0,0,1,1,0]).
%test(top_driver,[[1,1,1,1,0,1,0,1,1,1,0,1,0,1,1,0,1,0,0,1,1,1,0,1,0,1,1,0,0,1,1,0,1,0,1,1,0,1,1,1,0,1,0,0,1,0,1,0,0,1,0,0,1,0,1,1,1,1,0,0,0,1,0,0,0,1,0,0,0,1,0,0,0,0,1,1,0,1,0,1,1,1,1,0,0,0,1,1,1,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,1,1,0,0,1,0,0,1,1,1,1,1,0,0,1,0,0,0,0,1,1,0,1,1]], [1,1,1,1,0,1,1,0,1,1,0,0,0,1,1,0,1,1,0,0,0,1,1,1,0,1,1,1,1,1,0,0,1,0,1,0,1,0,0,1,1,1,1,0,1,1,0,1,1,1,1,0,0,0,0,0,0,1,1,0,1,1,1,0,1,1,0,1,1,1,1,1,0,0,0,1,1,1,1,1,0,1,0,0,1,0,0,1,0,1,1,0,0,1,0,0,0,0,0,0,0,1,0,1,0,1,0,0,1,0,1,0,1,0,0,0,0,0,0,0,1,1,1,1,0,1,0,0]).
%test(top_driver,[[0,0,0,1,0,0,1,0,1,0,1,0,0,0,1,1,0,0,1,1,1,1,1,1,0,1,1,1,1,0,1,1,0,1,0,1,0,1,1,1,0,0,1,0,1,0,1,1,1,1,0,1,0,1,1,1,1,1,0,0,0,0,0,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,1,0,1,1,0,0,1,1,1,1,0,1,1,1,0,1,0,0,1,0,1,1,0,0,0,0,1,0,0,1,1,1,1,0,1,0,0,1,0,0,1,1,0,1,0,0,1,1,0,0]], [1,0,1,0,1,0,1,1,1,0,1,1,1,0,1,0,0,0,0,0,1,0,0,1,1,1,0,0,1,0,1,0,0,1,0,1,1,0,1,0,1,1,0,0,1,1,1,1,0,1,0,0,1,1,0,0,0,0,1,0,0,1,1,0,1,0,0,1,0,1,1,1,0,0,0,1,0,1,0,0,0,1,1,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,1,1,1,1,1,0,1,0,1,0,0,0,1,1,1,0,1,0,1,0,1,0,0,1,1,1,0]).
%test(top_driver,[[0,1,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0,1,1,0,0,0,0,0,1,1,1,1,1,0,0,1,1,1,0,0,0,1,1,1,0,1,1,0,0,1,0,1,1,0,1,0,0,0,1,0,1,1,0,1,1,0,0,0,0,0,0,1,1,0,0,1,0,0,1,1,1,0,1,1,1,1,0,1,0,1,1,1,1,0,1,1,1,0,1,1,1,0,1,1,0,0,1,0,1,1,1,1,1,1,0,0,0,1,0,1,1,0,0,1,0,1,0,0,1]], [0,1,1,0,0,1,0,0,1,0,0,0,1,1,0,1,1,1,0,1,0,1,0,1,1,0,0,1,0,0,1,0,0,0,1,0,1,1,0,0,1,0,1,1,0,1,0,1,0,0,1,1,0,0,0,1,1,0,0,1,1,0,0,1,0,0,1,1,0,0,1,0,1,1,1,0,1,0,1,0,1,1,1,1,0,0,0,0,0,0,1,0,1,0,0,0,0,0,0,1,1,0,1,0,0,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0,1,1,1,0,1,1,1]).
%test(top_driver,[[1,1,0,1,0,0,1,1,1,0,0,1,1,1,1,0,1,0,1,1,1,1,0,0,0,0,0,0,1,0,1,1,0,0,1,1,1,1,1,1,1,0,1,0,0,1,1,1,1,1,1,0,0,1,1,0,1,1,0,1,1,1,0,1,1,1,0,1,0,0,0,1,0,0,0,1,1,1,0,1,0,0,1,0,1,1,1,0,1,0,1,0,1,1,0,0,1,0,1,0,1,0,1,1,0,0,1,1,1,0,1,0,1,1,0,0,0,0,0,1,1,1,1,1,1,1,0,0]], [0,0,1,1,0,1,0,1,1,1,1,0,0,0,0,0,1,1,1,0,0,0,1,0,0,0,1,1,0,0,1,1,0,0,0,0,0,0,1,0,0,0,0,0,1,0,1,1,1,1,0,0,0,0,0,0,1,0,1,1,0,1,0,1,1,1,1,1,0,0,1,0,1,0,0,0,1,0,1,1,0,0,1,1,1,0,1,1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,1,1,0,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,1,1,0,1,0,1,1]).
%test(top_driver,[[1,0,0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,1,1,1,1,0,1,0,0,0,0,0,1,1,0,0,1,0,0,1,1,1,0,0,0,1,1,0,0,0,1,1,0,0,0,1,1,0,0,0,1,0,1,0,1,1,0,0,0,0,1,0,1,1,1,0,1,1,1,1,0,0,0,1,1,1,1,0,0,1,0,1,0,1,1,1,0,0,0,0,0,0,1,0,0,0,1,1,0,0,1,1,1,1,1,0,1,0,0,0,0,1,0,0,1,0,1,0,0,1,1,1]], [0,1,1,0,1,1,1,0,0,0,1,1,1,1,1,1,1,0,1,0,0,1,0,1,0,1,0,0,1,1,1,0,1,1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,1,1,1,0,0,0,1,1,0,0,0,1,1,1,1,1,0,1,1,0,0,0,1,1,0,1,0,1,1,0,1,1,0,1,0,0,0,0,0,1,1,0,0,1,0,1,1,0,1,0,0,1,0,1,0,0,1,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,0,1,1,0,1,0,1,1]).
%test(top_driver,[[0,0,0,1,1,1,0,1,1,0,0,1,0,0,0,1,0,0,1,0,0,0,0,1,1,1,0,1,1,1,0,0,1,1,0,0,0,1,1,1,0,1,1,0,1,1,1,1,0,0,0,0,0,0,1,0,0,0,1,1,0,1,0,0,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,1,1,1,0,1,0,1,1,1,0,0,0,1,0,1,1,0,0,0,1,0,0,0,0,0,0,0,0,1,1,1,0,1,1,0,1,0,1,1,0,1,1,0,0,0,1,1,0,0]], [0,0,0,0,0,0,1,0,1,0,1,1,1,1,0,1,1,1,1,0,1,1,0,0,1,0,0,0,1,1,1,0,1,0,0,1,0,0,0,1,0,1,1,1,0,0,1,1,1,0,0,0,0,0,1,1,0,1,1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,1,1,0,0,0,1,0,0,0,1,0,1,1,0,1,1,0,1,1,0,1,1,1,1,0,0,1,0,0,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,1,1,1,0,1,1]).
%test(top_driver,[[0,0,0,1,1,1,1,0,0,1,1,0,1,1,1,1,1,0,1,0,0,0,0,0,1,0,0,0,0,0,1,1,1,0,1,1,0,1,1,1,1,1,0,1,0,0,0,0,1,0,0,1,1,1,1,1,1,0,0,1,1,0,1,1,1,0,0,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,0,0,1,1,0,0,1,1,1,0,1,1,0,1,1,1,1,1,0,0,1,0,0,1,0,1,0,0,0,0,1,1,0,0,1,0,0,0,0,1,0,1,1,1,1,1]], [1,0,0,0,0,1,0,1,0,1,0,0,0,1,1,0,1,0,0,0,0,1,0,0,0,0,1,1,0,1,1,0,1,0,0,1,0,1,0,0,1,0,0,0,0,1,1,1,0,0,1,1,1,0,1,0,0,0,1,1,1,0,1,1,1,0,1,0,1,0,1,1,0,0,0,1,1,0,0,1,0,1,0,0,0,1,0,1,1,0,0,0,1,1,1,0,0,0,0,1,0,0,0,1,0,1,1,0,1,0,1,0,1,0,0,1,0,1,0,0,0,1,0,0,1,0,0,0]).

%% test framework

run_tests :-
  test(Pred,Args,Expected),
  run_one_test(Pred,Args,Expected),
  fail.

run_tests :- writeln('testing completed.').

run_one_test(Pred,Args,Expected) :-
  append(Args,[Actual],FullArgs),
  Goal =.. [Pred|FullArgs],
  call(Goal), !,
  (Actual = Expected -> true ;
    write('*'), write(Pred), write('* expected:'), write(Expected),
    write(' but got: '), write(Actual), nl).

run_one_test(Pred,Args,_) :-
  write('*'), write(Pred), write('* unprovable with args: '), write(Args), nl.


%% test drivers

top_driver(FlatIn,FlatOut) :-
  length(Ai,32),
  length(Bi,32),
  length(Ci,32),
  length(Di,32),
  flatten([Ai,Bi,Ci,Di],FlatIn),
  main(input(Ai,Bi,Ci,Di),output(Ao,Bo,Co,Do)),
  length(Ao,32),
  length(Bo,32),
  length(Co,32),
  length(Do,32),
  flatten([Ao,Bo,Co,Do],FlatOut).


%%%%
%%%% the full MD5 algorithm
%%%%

%% word contructors


variable_word(Prefix,L) :-
  variable_word(0,Prefix,[],L).

variable_word(32,_,L,L) :- !.
variable_word(N,Prefix,T,L) :-
  atom_concat(Prefix,N,Label),
  N1 is N+1,
  variable_word(N1,Prefix,[var(Label)|T],L).  

constant_word(D,L) :-
  integer_to_bitlist_word(D,32,L).

initial_word(Which,L) :-
  initial_integer(Which,D),
  constant_word(D,L).

shift_word(I,L) :-
  shift_integer(I,D),
  constant_word(D,L).

%% main

main :-
  variable_word(x0_,X0),
  variable_word(x1_,X1),
  variable_word(x2_,X2),
  variable_word(x3_,X3),
  main(input(X0,X1,X2,X3),_).

main(input(X0,X1,X2,X3),output(AFinal,BFinal,CFinal,DFinal)) :-
  initial_word(a,A0),
  initial_word(b,B0),
  initial_word(c,C0),
  initial_word(d,D0),


  constant_word(2147483648,Tick),
  constant_word(0,Zero),
  constant_word(128,Size),

  X = [
    X0,   X1,   X2,   X3,
    Tick, Zero, Zero, Zero,
    Zero, Zero, Zero, Zero,
    Zero, Zero, Zero, Size],

  writeln('about to run the 64 steps'),
  step_src(Steps),
  run_steps(
    Steps,
    X,
    registers(A0,B0,C0,D0),
    registers(A,B,C,D)),
  
  writeln('steps completed'),
  writeln('adding results'),

  bitlist_add(A0,A,AAlmost),
  simplify_nicely(a,AAlmost,AFinal),
  bitlist_add(B0,B,BAlmost),
  simplify_nicely(b,BAlmost,BFinal),
  bitlist_add(C0,C,CAlmost),
  simplify_nicely(c,CAlmost,CFinal),
  bitlist_add(D0,D,DAlmost),
  simplify_nicely(d,DAlmost,DFinal),

  writeln('done!').

%% step execution

run_steps([],_,Regs,Regs).
run_steps([Step|Steps],X,Regs0,Regs) :-
  run_step(Step,X,Regs0,Regs1),
  run_steps(Steps,X,Regs1,Regs).

run_step(Step,X,InRegs,OutRegs) :-
  Step = step(Alg,Swizzle,K,S,I),
  Swizzle = [AName,BName,CName,DName],

  select_register(AName,InRegs,Ai),
  select_register(BName,InRegs,Bi),
  select_register(CName,InRegs,Ci),
  select_register(DName,InRegs,Di),

  select_register(AName,OutRegs,Ao),

  nth0(K,X,Xk),
  shift_word(I,Ti),

  writeln(Step),

  writeln('constructing expressions...'), 

  md5_apply(Alg,Bi,Ci,Di,Applied),
  simplify_nicely(applied,Applied,Applied_),

  bitlist_add(Ai,Applied_,Data),
  simplify_nicely(data,Data,Data_),

  bitlist_add(Xk,Ti,Consts),
  simplify_nicely(consts,Consts,Consts_),

  bitlist_add(Data_,Consts_,PreShift),
  simplify_nicely(preshift,PreShift,PreShift_),

  bitlist_rotate(PreShift_,S,PostShift),
  bitlist_add(Bi,PostShift,Hairy),
  simplify_nicely(hairy,Hairy,Ao),
  nl.

simplify_nicely(Tag,In,Out) :-
  write('simplifying '), write(Tag), nl,
  bitlist_complexity(In,Cin),
  write(' * initial complexity: '), write(Cin), nl,
  bitlist_simplify(In,Out),
  bitlist_complexity(Out,Cout),
  write(' * final complexity:   '), write(Cout), nl.

select_register(a,registers(A,_,_,_),A).  
select_register(b,registers(_,B,_,_),B).  
select_register(c,registers(_,_,C,_),C).  
select_register(d,registers(_,_,_,D),D).  

%%%%
%%%% helper functions (ff,gg,hh,ii)
%%%%

md5_apply(ff,X,Y,Z,Res) :- md5_ff(X,Y,Z,Res).
md5_apply(gg,X,Y,Z,Res) :- md5_gg(X,Y,Z,Res).
md5_apply(hh,X,Y,Z,Res) :- md5_hh(X,Y,Z,Res).
md5_apply(ii,X,Y,Z,Res) :- md5_ii(X,Y,Z,Res).

md5_ff(X,Y,Z,Res) :-
  bitlist_and(X,Y,XandY),
  bitlist_not(X,NotX),
  bitlist_and(NotX,Z,NotXandZ),
  bitlist_or(XandY,NotXandZ,Res).

md5_gg(X,Y,Z,Res) :-
  bitlist_and(X,Z,XandZ),
  bitlist_not(Z,NotZ),
  bitlist_and(Y,NotZ,YandNotZ),
  bitlist_or(XandZ,YandNotZ,Res).

md5_hh(X,Y,Z,Res) :-
  bitlist_xor(X,Y,XxorY),
  bitlist_xor(XxorY,Z,Res).

md5_ii(X,Y,Z,Res) :-
  bitlist_not(Z,NotZ),
  bitlist_or(X,NotZ,XorNotZ),
  bitlist_xor(Y,XorNotZ,Res).


%%%%
%%%% initial registers
%%%%

initial_integer(a,1732584193).
initial_integer(b,4023233417).
initial_integer(c,2562383102).
initial_integer(d,271733878).

%%%%
%%%% shift constants
%%%%

shift_integer(I,D) :-
  D is truncate(4294967296*abs(sin(I))).


%%%%
%%%% algorithm steps
%%%%

% read like this: [abcd k s i]
% a = b + ((a + F(b,c,d) + X[k] + T[i]) <<< s)

step_src([

  %% round 1

  step(ff,[a,b,c,d],0,7,1),
  step(ff,[d,a,b,c],1,12,2),
  step(ff,[c,d,a,b],2,17,3),
  step(ff,[b,c,d,a],3,22,4),
  
  step(ff,[a,b,c,d],4,7,5),
  step(ff,[d,a,b,c],5,12,6),
  step(ff,[c,d,a,b],6,17,7),
  step(ff,[b,c,d,a],7,22,8),
  
  step(ff,[a,b,c,d],8,7,9),
  step(ff,[d,a,b,c],9,12,10),
  step(ff,[c,d,a,b],10,17,11),
  step(ff,[b,c,d,a],11,22,12),
  
  step(ff,[a,b,c,d],12,7,13),
  step(ff,[d,a,b,c],13,12,14),
  step(ff,[c,d,a,b],14,17,15),
  step(ff,[b,c,d,a],15,22,16),
  
  %% round 2

  step(gg,[a,b,c,d],1,5,17),
  step(gg,[d,a,b,c],6,9,18),
  step(gg,[c,d,a,b],11,14,19),
  step(gg,[b,c,d,a],0,20,20),
  
  step(gg,[a,b,c,d],5,5,21),
  step(gg,[d,a,b,c],10,9,22),
  step(gg,[c,d,a,b],15,14,23),
  step(gg,[b,c,d,a],4,20,24),
  
  step(gg,[a,b,c,d],9,5,25),
  step(gg,[d,a,b,c],14,9,26),
  step(gg,[c,d,a,b],3,14,27),
  step(gg,[b,c,d,a],8,20,28),
  
  step(gg,[a,b,c,d],13,5,29),
  step(gg,[d,a,b,c],2,9,30),
  step(gg,[c,d,a,b],7,14,31),
  step(gg,[b,c,d,a],12,20,32),
  
  %% round 3

  step(hh,[a,b,c,d],5,4,33),
  step(hh,[d,a,b,c],8,11,34),
  step(hh,[c,d,a,b],11,16,35),
  step(hh,[b,c,d,a],14,23,36),
  
  step(hh,[a,b,c,d],1,4,37),
  step(hh,[d,a,b,c],4,11,38),
  step(hh,[c,d,a,b],7,16,39),
  step(hh,[b,c,d,a],10,23,40),
  
  step(hh,[a,b,c,d],13,4,41),
  step(hh,[d,a,b,c],0,11,42),
  step(hh,[c,d,a,b],3,16,43),
  step(hh,[b,c,d,a],6,23,44),
  
  step(hh,[a,b,c,d],9,4,45),
  step(hh,[d,a,b,c],12,11,46),
  step(hh,[c,d,a,b],15,16,47),
  step(hh,[b,c,d,a],2,23,48),
  
  %% round 4

  step(ii,[a,b,c,d],0,6,49),
  step(ii,[d,a,b,c],7,10,50),
  step(ii,[c,d,a,b],14,15,51),
  step(ii,[b,c,d,a],5,21,52),
  
  step(ii,[a,b,c,d],12,6,53),
  step(ii,[d,a,b,c],3,10,54),
  step(ii,[c,d,a,b],10,15,55),
  step(ii,[b,c,d,a],1,21,56),
  
  step(ii,[a,b,c,d],8,6,57),
  step(ii,[d,a,b,c],15,10,58),
  step(ii,[c,d,a,b],6,15,59),
  step(ii,[b,c,d,a],13,21,60),
  
  step(ii,[a,b,c,d],4,6,61),
  step(ii,[d,a,b,c],11,10,62),
  step(ii,[c,d,a,b],2,15,63),
  step(ii,[b,c,d,a],9,21,64)

]).

%%%%
%%%% bitlist utilities
%%%%

integer_to_bitlist_word(Var,Width,L) :-
  var(Var), !,
  length(L,Width).

integer_to_bitlist_word(Int,Width,L) :-
  integer_to_bitlist(Width,Int,[],L).

integer_to_bitlist(0,_,RL,RL) :- !.
integer_to_bitlist(N,Int,Sofar,RL) :-
  H is Int mod 2,
  Rest is Int // 2,
  N1 is N-1,
  integer_to_bitlist(N1,Rest,[H|Sofar],RL).

bitlist_rotate(In,0,In) :- !.
bitlist_rotate(In,Times,Out) :-
  rotate(Times,In,Out).

rotate(0,L,L) :- !.
rotate(N,[H|T],L) :-
  N1 is N-1,
  append(T,[H],L1),
  rotate(N1,L1,L).

bit_add(A, B, Ci, Co, S) :-
  Co = or(and(A,B),and(Ci,xor(A,B))),
  S = xor(Ci,xor(A,B)).


bitlist_add(A,B,S) :-
  reverse(A,RA),
  reverse(B,RB),
  bitlist_add(RA,RB,0,RS),
  reverse(RS,S).

bitlist_add([],[],_,[]).
bitlist_add([A0|A],[B0|B],Ci,[S0|S]) :-
  bit_add(A0,B0,Ci,Co,S0),
  bitlist_add(A,B,Co,S).

bit_xorize(A,B,xor(A,B)).
bitlist_xor(A,B,C) :- maplist(bit_xorize,A,B,C).

bit_orize(A,B,or(A,B)).
bitlist_or(A,B,C) :- maplist(bit_orize,A,B,C).

bit_andize(A,B,and(A,B)).
bitlist_and(A,B,C) :- maplist(bit_andize,A,B,C).

bit_notize(A,not(A)).
bitlist_not(A,B) :- maplist(bit_notize,A,B).


%% assignment to labeled variables

bitlist_assign([],L,L).
bitlist_assign([P|T],L,R) :-
  maplist(bit_assign_prime(P),L,L1),
  bitlist_assign(T,L1,R).

bit_assign_prime(Pair,Term,Result) :-
  bit_assign(Term,Pair,Result).

bit_assign(0,_,0).
bit_assign(1,_,1).
bit_assign(var(Label),Label-V,V) :- !.
bit_assign(var(Label),_,var(Label)) :- !.
bit_assign(not(T),P,R) :-
  bit_assign(T,P,RT),
  bit_simplify(not(RT),R).
bit_assign(xor(A,B),P,R) :-
  bit_assign(A,P,RA),
  bit_assign(B,P,RB),
  bit_simplify(xor(RA,RB),R).
bit_assign(and(A,B),P,R) :-
  bit_assign(A,P,RA),
  bit_assign(B,P,RB),
  bit_simplify(and(RA,RB),R).
bit_assign(or(A,B),P,R) :-
  bit_assign(A,P,RA),
  bit_assign(B,P,RB),
  bit_simplify(or(RA,RB),R).


%% algebraic simplifications

bitlist_simplify(L,R) :- maplist(bit_simplify,L,R).

bit_simplify(0,0).
bit_simplify(1,1).

bit_simplify(var(A),var(A)).
bit_simplify(not(A),R) :-
  bit_simplify(A,RA),
  bit_simplify_not(RA,R).

bit_simplify(xor(A,B),R) :-
  bit_simplify(A,RA),
  bit_simplify(B,RB),
  msort([RA,RB],[SRA,SRB]),
  bit_simplify_xor(SRA,SRB,R).

bit_simplify(or(A,B),R) :-
  bit_simplify(A,RA),
  bit_simplify(B,RB),
  msort([RA,RB],[SRA,SRB]),
  bit_simplify_or(SRA,SRB,R).

bit_simplify(and(A,B),R) :-
  bit_simplify(A,RA),
  bit_simplify(B,RB),
  msort([RA,RB],[SRA,SRB]),
  bit_simplify_and(SRA,SRB,R).

bit_simplify_not(not(A),A) :- !.
bit_simplify_not(0,1) :- !.
bit_simplify_not(1,0) :- !.
bit_simplify_not(A,not(A)).

bit_simplify_xor(0,B,B) :- !.
bit_simplify_xor(1,B,R) :- !, bit_simplify(not(B),R).
bit_simplify_xor(A,A,0) :- !.
bit_simplify_xor(not(A),A,1) :- !.
bit_simplify_xor(A,B,xor(A,B)).

bit_simplify_and(0,_,0) :- !.
bit_simplify_and(1,B,B) :- !.
bit_simplify_and(not(A),A,0) :- !.
bit_simplify_and(A,A,A) :- !.
bit_simplify_and(A,B,and(A,B)).

bit_simplify_or(0,B,B) :- !.
bit_simplify_or(1,_,1) :- !.
bit_simplify_or(not(A),A,1) :- !.
bit_simplify_or(A,A,A) :- !.
bit_simplify_or(A,B,or(A,B)).

%% complexity?

bitlist_complexity(L,C) :-
  maplist(bit_complexity,L,Complexities),
  sumlist(Complexities,C).

bit_complexity(0,1).
bit_complexity(1,1).
bit_complexity(var(_),1).
bit_complexity(not(A),C) :-
  bit_complexity(A,C0),
  C is C0+1.
bit_complexity(xor(A,B),C) :-
  bit_complexity(A,CA),
  bit_complexity(B,CB),
  C is CA+CB+1.
bit_complexity(and(A,B),C) :-
  bit_complexity(A,CA),
  bit_complexity(B,CB),
  C is CA+CB+1.
bit_complexity(or(A,B),C) :-
  bit_complexity(A,CA),
  bit_complexity(B,CB),
  C is CA+CB+1.