In another question Initializing non-deterministic variables in QBF, I was interested about translating assertion-based pseudocode to QBF in order to have an exponentially more compact encoding compared to unrolling deeply nested loops into SAT.

While some misunderstandings in the pseudocode for that question ultimately led to several answers adding in 'cheating' simplifications not in the spirit of the original question, D.W. clarified that a full answer depends on the relationship between PSPACE and #PSPACE.

Formally PSPACE and #PSPACE are "incompatible" for comparison in a sense of being a decision problem versus a counting problem, but this artifact can be made consistent in analogy to PH versus #P. Decision classes such as PP and ⊕P find the most-significant bit of the #P counting problem and least-significant bit respectively. Reductions filling in the rest of the bits of #P output should be rather straightforward given a powerful PSPACE-complete oracle, since P^#P ⊂ PH ⊂ PSPACE.

Looking at the following assertion pseudocode, it's obvious that counting solutions to either SAT (#SAT) or QBF (#QBF) is trivially possible using polynomial-space. For example, the following pseudocode would naively run in exponential time, but never uses more than a linear O(n) amount of memory. This renders, via abuse of notation, #PSPACE ⊂ PSPACE.

counter = 0
for loop_aux_0 in {0,1}:
  for loop_aux_1 in {0,1}:
    for loop_aux_2 in {0,1}:
      .
        .
          .
            for loop_aux_n in {0,1}: 
              counter += f(loop_aux_0, loop_aux_1, .., loop_aux_n)
assert(counter != UINT_MAX)

Here f is an arbitrary PSPACE function that outputs 0 or 1.

If there are no objections that #PSPACE ⊂ PSPACE, how can I actually encode #QBF as part of a QBF instance?

I suggested a QBF implementation (although missing initialization) utilizing an adder circuit for counter with its output fed back in as input alongside f_ouput being the carry-in of the LSB:

∃ counter[n] ∀ loop_aux[n] ∃ f_output[1] (counter += f_output) & (f_output == f(loop_aux_0, loop_aux_1, .., loop_aux_n))

The problem with this encoding is that the counter is incremented non-deterministically without initialization, rendering any value of counter satisfiable. Can this encoding be saved with additional clauses or auxiliary variables to initialize the counter? Or is there a better way to encode #QBF in QBF?