lzero[N: posnat, logN: posnat]: THEORY
BEGIN
   ASSUMING
	  l: VAR nat;
	  logN_is_logN: ASSUMPTION 2^(logN-1) < N+1 AND N+1 <= 2^logN;
		%%%% we have to code the numbers 0...N with logN bits
   ENDASSUMING
   IMPORTING basics_import


   b: VAR bvec[N];
   lzero_TCC: LEMMA  FORALL (b):
	    is_finite[nat]({i: nat | i = 0 OR 
 			(i <= N AND b ^ (N - 1, N - i) = fill[i](FALSE))})
     AND NOT empty?[nat]({i: nat | i = 0 OR 
 			(i <= N AND b ^ (N - 1, N - i) = fill[i](FALSE))});

   lzero(b): nat = max({ i: nat | i=0 OR 
 			(i<=N AND b^(N-1, N-i)=fill[i](FALSE)) });

   lzero_bound: LEMMA lzero(b)<=N;

   lzero_lem1: LEMMA 
      N > 2 IMPLIES
         FORALL (i: subrange(1, N-2)):
            lzero(b) = i IFF b = fill[i](FALSE) o fill[1](TRUE) o b^(N-i-2, 0);

   lzero_lem2: LEMMA 
      N > 1 IMPLIES
         (lzero(b) = 0 IFF b = fill[1](TRUE) o b^(N-2, 0));
   
   lzero_lem3: LEMMA
      N > 1 IMPLIES
         (lzero(b) = N-1 IFF b = fill[N-1](FALSE) o fill[1](TRUE));
   
   lzero_lem4: LEMMA lzero(b) = N IFF b = fill[N](FALSE);

   lzero_bvnat: LEMMA
      N > 1 IMPLIES
         b/=fill[N](FALSE) IMPLIES
            (bv2nat(b) = bv2nat(b^(N-1-lzero(b), 0)));

   lzero_bit: Lemma
      N > 1 Implies
         b /= fill[N](False) Implies
           b(N-1-lzero(b)) = true;

End lzero
  

lzero_concat[N1,N2: above(2), logN1, logN12: posnat]: Theory
Begin
   Assuming
	  l: Var nat;
	  logN_is_logN: Assumption
                   (2^(logN1-1) < N1+1 And N1+1 <= 2^logN1
                And 2^(logN12-1) < N1+N2+1 And N1+N2+1 <= 2^logN12);
   Endassuming

   Importing lzero

   b1: Var bvec[N1];
   b2: Var bvec[N2];

   lzero_concat1: Lemma (N1 > 2 and N2 > 2 ) Implies
      b1/=fill[N1](False) Implies
	 lzero[N1, logN1](b1) = lzero[N1+N2,logN12](b1 o b2);

   lzero_concat4: Lemma
      Forall (b1,b2: bvec[2]): b1 /= fill[2](False) Implies
         lzero[2,2](b1) = lzero[4,3](b1 o b2);

End lzero_concat


lzero_log[N: above(2), logN: posnat]: THEORY
BEGIN
   ASSUMING
	  l: VAR nat;
	  logN_is_logN: ASSUMPTION 2^(logN-1) < N+1 AND N+1 <= 2^logN;
   ENDASSUMING
   lib: LIBRARY = "../lib";
   IMPORTING lzero[N, logN]

   a: VAR bvec[N];

   lzero_computes_log: THEOREM  a/=fill[N](FALSE) 
      IMPLIES log2(bv2nat(a)) = N - 1 - lzero(a);

   lzero_computes_log_vv: THEOREM  a/=fill[N](FALSE) IMPLIES
      lzero(a) = N - 1 - log2(bv2nat(a));
END lzero_log



% a second lzero concat theory is necessary because inserting logN2
% as theory actual causes the proof of lzero_concat.lzero_concat1 to fail.
% additionally lzero_log is used in the proof
lzero_concat2[N1,N2: above(2), logN1, logN2, logN12: posnat]: Theory
Begin
   Assuming
	  l: Var nat;
	  logN_is_logN: Assumption %(N1 > 2 and N2 > 2) Implies
                   (2^(logN1-1) < N1+1 And N1+1 <= 2^logN1
                And 2^(logN2-1) < N2+1 And N2+1 <= 2^logN2
                And 2^(logN12-1) < N1+N2+1 And N1+N2+1 <= 2^logN12);
   Endassuming

   Importing  lzero_log

   b1: Var bvec[N1];
   b2: Var bvec[N2];

   lzero_concat0: Lemma
      b1 = fill[N1](False) Implies
         lzero[N1 + N2, logN12](b1 o b2) = N1 + lzero[N2, logN2](b2);

End lzero_concat2



lzero_exp2_impl: Theory
Begin

  Importing lzero, lzero_concat, lzero_concat2

  lzero_plus_exp2: Lemma
    Forall (m: above(1), b: bvec[m]):
      bv2nat( ( b(m-1) o (Not b(m-1)) ) o b^(m-2,0) ) = bv2nat(b) + 2^(m-1);

  lzero_exp2_impl(m: nat, b: bvec[2^m]): Recursive bvec[m+1] =
    If m = 0 Then
      Not b(0)
    Elsif m = 1 Then
      Let lz_l = Not b(0),
          lz_h = Not b(1)
      In
        If lz_h Then
          lz_l o Not lz_l
        Else
          fill[1](false) o lz_h
        Endif
    Else
      Let lz_h = lzero_exp2_impl(m-1, b^(2^m - 1, 2^(m-1))),
          lz_l = lzero_exp2_impl(m-1, b^(2^(m-1) - 1, 0))
      In
        If lz_h(m-1) Then
          lz_l(m-1) o (Not lz_l(m-1)) o lz_l^(m-2, 0)
        Else
          fill[1](false) o lz_h
        Endif
    Endif
    Measure m;

  lzero_exp2_impl_correct: Lemma 
    Forall (m: nat, b: bvec[2^m]):
      bv2nat(lzero_exp2_impl(m, b)) = lzero[2^m,m+1](b);

End lzero_exp2_impl


lzero_impl[N: above(2), logN: posnat]: Theory
Begin
  Assuming
	  l: Var nat;
	  logN_is_logN: Assumption 2^(logN-1) < N+1 And N+1 <= 2^logN;
          %%%% we have to code the numbers 0...N with logN bits
  Endassuming

  Importing lzero_exp2_impl

  b: Var bvec[N];

  lzero_impl(b): bvec[logN] =
%    Let NN = 2^logN In
    If 2^(logN-1) = N Then
      lzero_exp2_impl(logN-1, b)
    Else
      lzero_exp2_impl(logN, b o fill[2^logN - N](True))^(logN-1,0)
    Endif;

  lzero_impl_correct: Lemma
    bv2nat(lzero_impl(b)) = lzero[N, logN](b);

End lzero_impl