Binary counter

DefinitionBinary counter increment#✓fully proved

A \(k\)-bit counter is a vector \(b = (b_0, \dots, b_{k-1})\) of bits stored lowest bit first. Incrementing \(b\) changes the initial run of \(1\) bits \(b_0, \dots, b_{t-1}\) to \(0\) and then changes the first \(0\) bit \(b_t\), if there is one, to \(1\); if every bit is \(1\), all bits become \(0\) and no new bit is added. The result is again a \(k\)-bit counter, and the cost of the increment is the number of bits changed, one unit per changed bit.

public def increment {k : Nat} (bits : Vector Bool k) : TimeM Nat (Vector Bool k) :=
  let result := carry bits.toList
  ⟨⟨result.ret.toArray, by
      change (carry bits.toList).ret.toArray.size = k
      simp only [List.size_toArray, carry_length, Vector.length_toList]⟩, result.time⟩

Used by 11

Used byExact cost of an increment · Increment costs at most the width · Incrementing the all-ones counter costs the full width · Increment adds one with wraparound · Running the binary counter · One more increment · Exact cost of increments from zero · Lower bound on the cost of increments from zero · Aggregate cost bound for the binary counter · Cost recurrence for the binary counter run · Counter value after successive increments

TheoremIncrement adds one with wraparound#✓fully proved

Let \(b = (b_0, \dots, b_{k-1})\) be a \(k\)-bit counter stored lowest bit first, with bits \(b_i \in \{0, 1\}\) and unsigned value \(v(b) = \sum_{i < k} b_i 2^i\). If \(b'\) is the counter returned by incrementing \(b\), then \(v(b') = (v(b) + 1) \bmod 2^k\).

public theorem increment_value {k : Nat} (bits : Vector Bool k) :
    (BitVec.ofBoolListLE (increment bits).ret.toList).toNat =
      ((BitVec.ofBoolListLE bits.toList).toNat + 1) % 2 ^ k

Uses 1 · Used by 1

Statement usesBinary counter increment

Used byCounter value after successive increments

TheoremExact cost of an increment#✓fully proved

Let \(b = (b_0, \dots, b_{k-1})\) be a \(k\)-bit counter stored lowest bit first, and let \(t\) be the length of its initial run of \(1\) bits, that is, the largest \(t \le k\) with \(b_0 = \dots = b_{t-1} = 1\). The cost of incrementing \(b\) is \(t + 1\) if \(t < k\), and \(t\) if \(t = k\).

public theorem increment_time {k : Nat} (bits : Vector Bool k) :
    (increment bits).time = (bits.toList.takeWhile id).length +
      if (bits.toList.takeWhile id).length < k then 1 else 0

Uses 1

Statement usesBinary counter increment

TheoremIncrement costs at most the width#✓fully proved

For every \(k\)-bit counter \(b\) (a vector of \(k\) bits, lowest bit first), the cost of incrementing \(b\) is at most \(k\).

public theorem increment_time_le {k : Nat} (bits : Vector Bool k) :
    (increment bits).time ≤ k

Uses 1

Statement usesBinary counter increment

DefinitionRunning the binary counter#✓fully proved

For a width \(k\), a \(k\)-bit counter \(b\) and \(n \in \mathbb{N}\), the run of \(n\) increments from \(b\) is defined recursively. The run of \(0\) increments returns \(b\) at cost zero. The run of \(n + 1\) increments performs the run of \(n\) increments, then increments the counter it returned and returns the result; its cost is the cost of the \(n\)-step run plus the cost of that increment.

public def run {k : Nat} (bits : Vector Bool k) : Nat → TimeM Nat (Vector Bool k)
  | 0 => pure bits
  | n + 1 => do
      let previous ← run bits n
      increment previous

Uses 1 · Used by 8

Statement usesBinary counter increment

Used byFlip counts of the individual bits · One more increment · Exact cost of increments from zero · Lower bound on the cost of increments from zero · Aggregate cost bound for the binary counter · Cost recurrence for the binary counter run · Counter value after successive increments · Running zero increments

TheoremRunning zero increments#✓fully proved

For every width \(k\) and every \(k\)-bit counter \(b\), running zero increments from \(b\) returns \(b\) unchanged at cost zero.

public theorem run_zero {k : Nat} (bits : Vector Bool k) :
    run bits 0 = pure bits

Uses 1

Statement usesRunning the binary counter

TheoremOne more increment#✓fully proved

For every bit vector \(b\) and every natural number \(n\), the bit vector returned by running \(n + 1\) increments from \(b\) is the increment of the bit vector returned by running \(n\) increments from \(b\).

public theorem run_ret_succ {k : Nat} (bits : Vector Bool k) (n : Nat) :
    (run bits (n + 1)).ret = (increment (run bits n).ret).ret

Uses 2 · Used by 1

Statement usesBinary counter increment · Running the binary counter

Used byCounter value after successive increments

TheoremCost recurrence for the binary counter run#✓fully proved

For every width \(k\), every \(k\)-bit counter \(b\) and every \(n\), the cost of running \(n + 1\) successive increments from \(b\) equals the cost of running \(n\) increments from \(b\) plus the cost of incrementing the counter that the \(n\)-step run returns.

public theorem run_time_succ {k : Nat} (bits : Vector Bool k) (n : Nat) :
    (run bits (n + 1)).time =
      (run bits n).time + (increment (run bits n).ret).time

Uses 2 · Used by 3

Statement usesBinary counter increment · Running the binary counter

Used byExact cost of increments from zero · Lower bound on the cost of increments from zero · Aggregate cost bound for the binary counter

TheoremCounter value after successive increments#✓fully proved

For every width \(k\), every \(k\)-bit counter \(b\) and every \(n\), let \(v\) be the value of \(b\) read as an unsigned binary number with the least significant bit first. After \(n\) successive increments starting from \(b\), the counter read the same way has value \((v + n) \bmod 2^k\).

public theorem run_value {k : Nat} (bits : Vector Bool k) (n : Nat) :
    (BitVec.ofBoolListLE (run bits n).ret.toList).toNat =
      ((BitVec.ofBoolListLE bits.toList).toNat + n) % 2 ^ k

Uses 4 · Used by 4

Statement usesRunning the binary counter

Proof usesBinary counter increment · Increment adds one with wraparound · One more increment

Used byFlip counts of the individual bits · Exact cost of increments from zero · Lower bound on the cost of increments from zero · Aggregate cost bound for the binary counter

TheoremFlip counts of the individual bits#✓fully proved

Let \(k\), \(i\) and \(n\) be natural numbers with \(i < k\), and for each \(t\) let \(c_t\) be the bit vector returned by running \(t\) increments from the all-false bit vector of width \(k\). Then the number of \(t < n\) such that the bit at position \(i\) of \(c_t\) (counting from the low-order bit, starting at \(0\)) differs from the bit at position \(i\) of \(c_{t+1}\) is \(\lfloor n / 2^i \rfloor\).

public theorem run_bit_flips (k i n : Nat) (hi : i < k) :
    ((List.range n).map fun t =>
      if (run (Vector.replicate k false) t).ret.toList.getD i false ≠
          (run (Vector.replicate k false) (t + 1)).ret.toList.getD i false
        then 1 else 0).sum = n / 2 ^ i

Uses 2

Statement usesRunning the binary counter

Proof usesCounter value after successive increments

TheoremIncrementing the all-ones counter costs the full width#✓fully proved

For every \(k\), the cost of incrementing the \(k\)-bit counter whose \(k\) bits are all \(1\) is exactly \(k\).

public theorem increment_time_replicate_true (k : Nat) :
    (increment (Vector.replicate k true)).time = k

Uses 1

Statement usesBinary counter increment

TheoremExact cost of increments from zero#✓fully proved

For all natural numbers \(k\) and \(n\), running \(n\) increments from the all-false bit vector of width \(k\) costs exactly \(\sum_{i=0}^{k-1} \lfloor n / 2^i \rfloor\).

public theorem run_time_eq (k n : Nat) :
    (run (Vector.replicate k false) n).time =
      ((List.range k).map fun i => n / 2 ^ i).sum

Uses 4

Statement usesRunning the binary counter

Proof usesBinary counter increment · Cost recurrence for the binary counter run · Counter value after successive increments

TheoremAggregate cost bound for the binary counter#✓fully proved

For every width \(k\) and every \(n > 0\), performing \(n\) successive increments on the \(k\)-bit counter that starts with all bits zero costs strictly fewer than \(2n\) bit changes in total.

public theorem run_time_lt (k n : Nat) (hn : 0 < n) :
    (run (Vector.replicate k false) n).time < 2 * n

Uses 4

Statement usesRunning the binary counter

Proof usesBinary counter increment · Cost recurrence for the binary counter run · Counter value after successive increments

TheoremLower bound on the cost of increments from zero#✓fully proved

For all natural numbers \(k\) and \(n\) with \(k > 0\), running \(n\) increments from the all-false bit vector of width \(k\) costs at least \(n\).

public theorem run_time_ge (k n : Nat) (hk : 0 < k) :
    n ≤ (run (Vector.replicate k false) n).time

Uses 4

Statement usesRunning the binary counter

Proof usesBinary counter increment · Cost recurrence for the binary counter run · Counter value after successive increments

DefinitionResetting a binary counter#✓fully proved

Resetting a bit vector \(b\) of width \(k\) returns the all-false bit vector of width \(k\) and charges cost \(1\) for each position of \(b\) that holds true, that is, for each bit it changes from true to false.

public def reset {k : Nat} (bits : Vector Bool k) : TimeM Nat (Vector Bool k) :=
  let result := resetBits bits.toList
  ⟨⟨result.ret.toArray, by
      change (resetBits bits.toList).ret.toArray.size = k
      simp only [List.size_toArray, resetBits_length, Vector.length_toList]⟩, result.time⟩

Used by 10

Used byPotential identity for reset · Reset is idempotent · Cost of resetting a binary counter · A second reset costs nothing · Reset cost is the Hamming distance · Reset costs at most the width · Resetting the all-false counter costs nothing · Resetting a width-zero counter costs nothing · Reset returns the all-false counter · Reset yields the value zero

TheoremReset returns the all-false counter#✓fully proved

For every bit vector \(b\) of width \(k\), the bits returned by resetting \(b\) are, in order, \(k\) copies of false.

public theorem reset_toList {k : Nat} (bits : Vector Bool k) :
    (reset bits).ret.toList = List.replicate k false

Uses 1 · Used by 4

Statement usesResetting a binary counter

Used byPotential identity for reset · Reset is idempotent · A second reset costs nothing · Reset yields the value zero

TheoremReset yields the value zero#✓fully proved

For every bit vector \(b\) of width \(k\), the bits returned by resetting \(b\), read low-order bit first as an unsigned binary numeral, have value \(0\).

public theorem reset_value {k : Nat} (bits : Vector Bool k) :
    (BitVec.ofBoolListLE (reset bits).ret.toList).toNat = 0

Uses 2

Statement usesResetting a binary counter

Proof usesReset returns the all-false counter

TheoremCost of resetting a binary counter#✓fully proved

For every bit vector \(b\) of width \(k\), the cost of resetting \(b\) equals the number of positions of \(b\) that hold true.

public theorem reset_time {k : Nat} (bits : Vector Bool k) :
    (reset bits).time = (bits.toList.map Bool.toNat).sum

Uses 1 · Used by 5

Statement usesResetting a binary counter

Used byPotential identity for reset · A second reset costs nothing · Reset costs at most the width · Resetting the all-false counter costs nothing · Resetting a width-zero counter costs nothing

TheoremReset cost is the Hamming distance#✓fully proved

Let \(b = (b_0, \dots, b_{k-1})\) be a \(k\)-bit counter and \(b' = (b'_0, \dots, b'_{k-1})\) the counter returned by resetting \(b\). The cost of resetting \(b\) equals the number of indices \(i < k\) with \(b_i \ne b'_i\).

public theorem reset_time_changes {k : Nat} (bits : Vector Bool k) :
    (reset bits).time = ((List.range k).map fun i =>
      if bits.toList.getD i false ≠ (reset bits).ret.toList.getD i false
      then 1 else 0).sum

Uses 1

Statement usesResetting a binary counter

TheoremReset costs at most the width#✓fully proved

For every \(k\)-bit counter \(b\) (a vector of \(k\) bits), the cost of resetting \(b\) is at most \(k\).

public theorem reset_time_le {k : Nat} (bits : Vector Bool k) :
    (reset bits).time ≤ k

Uses 2

Statement usesResetting a binary counter

Proof usesCost of resetting a binary counter

TheoremResetting a width-zero counter costs nothing#✓fully proved

Resetting a bit vector of width \(0\) has cost \(0\).

public theorem reset_time_zero_width (bits : Vector Bool 0) :
    (reset bits).time = 0

Uses 2

Statement usesResetting a binary counter

Proof usesCost of resetting a binary counter

TheoremResetting the all-false counter costs nothing#✓fully proved

For every width \(k\), resetting the all-false bit vector of width \(k\) has cost \(0\).

public theorem reset_time_replicate_false (k : Nat) :
    (reset (Vector.replicate k false)).time = 0

Uses 2

Statement usesResetting a binary counter

Proof usesCost of resetting a binary counter

TheoremReset is idempotent#✓fully proved

For every \(k\)-bit counter \(b\), resetting the counter returned by resetting \(b\) returns the same counter as resetting \(b\) once.

public theorem reset_ret_idempotent {k : Nat} (bits : Vector Bool k) :
    (reset (reset bits).ret).ret = (reset bits).ret

Uses 2

Statement usesResetting a binary counter

Proof usesReset returns the all-false counter

TheoremA second reset costs nothing#✓fully proved

For every \(k\)-bit counter \(b\), resetting the counter returned by resetting \(b\) has cost \(0\).

public theorem reset_time_after_reset {k : Nat} (bits : Vector Bool k) :
    (reset (reset bits).ret).time = 0

Uses 3

Statement usesResetting a binary counter

Proof usesCost of resetting a binary counter · Reset returns the all-false counter

TheoremPotential identity for reset#✓fully proved

For every \(k\)-bit counter \(b\) (a vector of \(k\) bits), the cost of resetting \(b\) plus the number of \(1\) bits in the returned counter equals the number of \(1\) bits in \(b\).

public theorem reset_potential {k : Nat} (bits : Vector Bool k) :
    (reset bits).time + ((reset bits).ret.toList.map Bool.toNat).sum =
      (bits.toList.map Bool.toNat).sum

Uses 3

Statement usesResetting a binary counter

Proof usesCost of resetting a binary counter · Reset returns the all-false counter

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.