数组一半空了就缩容，为什么反而不停搬家？

"""Research prototype: explicit unit-copy model for grow/shrink thresholds.

One unit per push/pop plus one per live element copied during resize.
Allocation/zero fill/free costs and real timing are deliberately not modeled.
Python lists store the model state; their own allocation strategy is irrelevant.
"""
import json
from pathlib import Path
import platform


class ModelArray:
    def __init__(self, shrink_denominator):
        if shrink_denominator not in (2, 4):
            raise ValueError("use either one-half or one-quarter threshold")
        self.denominator = shrink_denominator
        self.slots = [None]
        self.size = 0
        self.copies = 0
        self.operations = 0
        self.trace = []

    def resize(self, capacity):
        replacement = [None] * capacity
        for i in range(self.size):
            replacement[i] = self.slots[i]
            self.copies += 1
        self.slots = replacement

    def record(self, operation, old_capacity, old_copies):
        moved = self.copies - old_copies
        self.operations += 1
        self.trace.append({"operation": operation, "size": self.size,
                           "old_capacity": old_capacity, "capacity": len(self.slots),
                           "copied": moved, "modeled_cost": 1 + moved})
        assert 0 <= self.size <= len(self.slots)

    def push(self, value):
        old_capacity, old_copies = len(self.slots), self.copies
        if self.size == len(self.slots):
            self.resize(2 * len(self.slots))
        self.slots[self.size] = value
        self.size += 1
        self.record('push', old_capacity, old_copies)

    def pop(self):
        if self.size == 0:
            raise ValueError("cannot pop an empty model")
        old_capacity, old_copies = len(self.slots), self.copies
        self.size -= 1
        value = self.slots[self.size]
        self.slots[self.size] = None
        if len(self.slots) > 1 and self.size * self.denominator <= len(self.slots):
            self.resize(max(1, len(self.slots) // 2))
        self.record('pop', old_capacity, old_copies)
        return value


def alternating_experiment(initial_size, cycles, denominator):
    model = ModelArray(denominator)
    for i in range(initial_size):
        model.push(i)
    prefill_copies = model.copies
    start = model.operations
    for i in range(cycles):
        model.push(1000 + i)
        assert model.pop() == 1000 + i
        assert model.slots[:model.size] == list(range(initial_size))
    return {
        "initial_size": initial_size, "cycles": cycles,
        "shrink_denominator": denominator,
        "alternating_operations": model.operations - start,
        "alternating_copies": model.copies - prefill_copies,
        "alternating_cost": model.operations - start + model.copies - prefill_copies,
        "total_operations_with_prefill": model.operations,
        "total_cost_with_prefill": model.operations + model.copies,
        "trace": model.trace[start:]
    }


def legal_operation_sequences(length, prefix='', size=0):
    if len(prefix) == length:
        yield prefix
        return
    yield from legal_operation_sequences(length, prefix + '+', size + 1)
    if size:
        yield from legal_operation_sequences(length, prefix + '-', size - 1)


def main():
    small = [alternating_experiment(4, 8, d) for d in (2, 4)]
    large = [alternating_experiment(128, 16, d) for d in (2, 4)]
    # Independent arithmetic for this fixed alternating family, not a second simulation.
    for pair, initial, cycles in [(small, 4, 8), (large, 128, 16)]:
        assert pair[0]['alternating_copies'] == 2 * initial * cycles
        assert pair[1]['alternating_copies'] == initial
    sequences = 0
    for length in range(13):
        for ops in legal_operation_sequences(length):
            for denominator in (2, 4):
                model, plain = ModelArray(denominator), []
                for index, operation in enumerate(ops):
                    if operation == '+':
                        model.push(index)
                        plain.append(index)
                    else:
                        assert model.pop() == plain.pop()
                    assert model.slots[:model.size] == plain
            sequences += 1
    report = {
        "status": "PASS", "python_version": platform.python_version(),
        "small_example": small, "larger_example": large,
        "legal_operation_sequences_checked": sequences, "max_sequence_length": 12,
        "sequence_check_purpose": "State/value preservation against an ordinary stack for both policies; this finite enumeration is not an asymptotic proof.",
        "cost_model": "one per push/pop, plus one per live element copied; excludes allocation, initialization, free, garbage collection, caching and elapsed time",
        "scope": "Synthetic tail push/pop model; no claim about CPython list, Java ArrayList or real latency. General quarter-threshold amortized bound needs the cited mathematical argument."
    }
    Path(__file__).with_suffix('.report.json').write_text(
        json.dumps(report, ensure_ascii=False, indent=2) + '\n', encoding='utf-8')
    for pair in [small, large]:
        for row in pair:
            print(f"initial={row['initial_size']} cycles={row['cycles']} threshold=1/{row['shrink_denominator']} alternating_copies={row['alternating_copies']} alternating_cost={row['alternating_cost']}")
    print(f"PASS; legal_sequences={sequences}; lengths=0..12; state checks only")


if __name__ == '__main__':
    main()

"""Fraction check of the written potential proof for the quarter policy.

This checks branch algebra on finitely many valid states, including states not
reachable from an empty array. The general proof is written in amortized-proof.json.
Neither the earlier graph enumeration nor the push/pop sequence suite is rerun.
"""
from collections import Counter
from fractions import Fraction
import json
from pathlib import Path
import platform

from array_shrink_threshold import ModelArray


def potential(n, m):
    if (type(n) is not int or type(m) is not int or m < 1
            or m & (m - 1) or not 0 <= n <= m):
        raise ValueError('valid state needs power-of-two capacity >=1 and 0<=n<=m')
    return Fraction(2 * n - m) if 2 * n >= m else Fraction(m, 2) - n


def branch_formula(n, m, operation):
    """Exact one-step equations, separately derived in the companion proof."""
    if operation == 'push':
        if n == m:
            return 'push-grow', n + 1, 2 * m, m + 1, Fraction(3)
        if m == 1:
            return 'push-minimum-crossing', 1, 1, 1, Fraction(3, 2)
        if 2 * n >= m:
            return 'push-no-resize-high', n + 1, m, 1, Fraction(3)
        return 'push-no-resize-low', n + 1, m, 1, Fraction(0)
    if operation != 'pop' or n == 0:
        raise ValueError('pop requires n>=1')
    q = n - 1
    if m > 1 and 4 * q <= m:
        return 'pop-shrink', q, m // 2, 1 + q, Fraction(q + 2) - Fraction(m, 4)
    if m == 1:
        return 'pop-minimum-crossing', 0, 1, 1, Fraction(1, 2)
    if 2 * n > m:
        return 'pop-no-resize-high', q, m, 1, Fraction(-1)
    return 'pop-no-resize-low', q, m, 1, Fraction(2)


def run_transition(n, m, operation):
    model = ModelArray(4)
    model.slots = list(range(n)) + [None] * (m - n)
    model.size = n
    before = potential(n, m)
    if operation == 'push':
        model.push(-1)
        expected_values = list(range(n)) + [-1]
    else:
        assert model.pop() == n - 1
        expected_values = list(range(n - 1))
    after = potential(model.size, len(model.slots))
    assert model.slots[:model.size] == expected_values
    cost = model.trace[-1]['modeled_cost']
    amortized = Fraction(cost) + after - before
    name, nn, mm, predicted_cost, predicted_amortized = branch_formula(n, m, operation)
    assert (model.size, len(model.slots), cost) == (nn, mm, predicted_cost)
    assert amortized == predicted_amortized
    assert amortized <= (3 if operation == 'push' else 2)
    assert before >= 0 and after >= 0
    return name, {
        'operation': operation, 'before': {'n': n, 'm': m, 'phi': str(before)},
        'after': {'n': nn, 'm': mm, 'phi': str(after)}, 'copied': model.copies,
        'actual_modeled_cost': cost, 'amortized_cost': str(amortized)
    }


def check_whole_sequence(operations):
    model = ModelArray(4)
    initial_phi = potential(0, 1)
    total_amortized = Fraction(0)
    pushes = pops = 0
    for i, operation in enumerate(operations):
        before = potential(model.size, len(model.slots))
        if operation == '+':
            model.push(i)
            pushes += 1
        else:
            model.pop()
            pops += 1
        after = potential(model.size, len(model.slots))
        total_amortized += model.trace[-1]['modeled_cost'] + after - before
    actual = model.operations + model.copies
    final_phi = potential(model.size, len(model.slots))
    assert actual == total_amortized + initial_phi - final_phi
    assert actual <= 3 * pushes + 2 * pops + initial_phi
    return {'pushes': pushes, 'pops': pops, 'modeled_cost': actual,
            'summed_amortized_cost': str(total_amortized),
            'initial_phi': str(initial_phi), 'final_phi': str(final_phi),
            'upper_bound': str(3 * pushes + 2 * pops + initial_phi)}


def main():
    counts, examples, maxima = Counter(), {}, {'push': None, 'pop': None}
    states = 0
    for exponent in range(11):
        m = 1 << exponent
        for n in range(m + 1):
            states += 1
            for operation in (['push', 'pop'] if n else ['push']):
                branch, record = run_transition(n, m, operation)
                counts[branch] += 1
                examples.setdefault(branch, record)
                measured = Fraction(record['amortized_cost'])
                if maxima[operation] is None or measured > maxima[operation]:
                    maxima[operation] = measured
    # This is one additional trace to check telescoping, not another enumeration.
    sequence = '+' * 32 + '-' * 24 + '+-' * 11 + '-' * 8
    telescoping = check_whole_sequence(sequence)
    # Beginning in a nonempty state requires its initial potential, not 1/2.
    _, arbitrary_start = run_transition(1024, 1024, 'push')
    assert arbitrary_start['actual_modeled_cost'] == 1025
    assert arbitrary_start['amortized_cost'] == '3'
    report = {
        'status': 'PASS', 'python_version': platform.python_version(),
        'states_checked': states, 'transitions_checked': sum(counts.values()),
        'capacity_domain_before_transition': '1,2,4,...,1024',
        'largest_capacity_after_a_checked_transition': 2048,
        'state_domain': 'every integer n in 0..m; includes valid but unreachable states',
        'branch_counts': dict(counts), 'one_observed_example_per_branch': examples,
        'maximum_amortized_push': str(maxima['push']),
        'maximum_amortized_pop': str(maxima['pop']),
        'telescoping_trace': telescoping,
        'nonempty_initial_state_counterexample': arbitrary_start,
        'boundary': 'Finite exact-arithmetic verification of the separately written branch proof and the model implementation. This enumeration is not the general proof, not a timing benchmark, and says nothing about allocator/zero-fill/free costs.'
    }
    Path(__file__).with_suffix('.report.json').write_text(
        json.dumps(report, ensure_ascii=False, indent=2) + '\n', encoding='utf-8')
    print(f"states={states}; transitions={sum(counts.values())}; exact Fraction branch checks PASS")
    print(f"max amortized push={maxima['push']}; max amortized pop={maxima['pop']}; initial potential=1/2")
    print(f"telescoping: actual={telescoping['modeled_cost']}; amortized={telescoping['summed_amortized_cost']}; final_phi={telescoping['final_phi']}")
    print('nonempty initial state: one push from n=m=1024 costs 1025, amortized 3; initial credit must be included')


if __name__ == '__main__':
    main()