Formal: Python/native classifier + per-line malloc attribution - #1082
Merged
Conversation
Closes two more HANDOFF gaps. PythonNativeClassifier.lean (scalene_cpu_profiler.py:251-341): the 4-way Python-vs-native time classifier. Separates the theorem from the heuristic: - charge_total / classified_conserves: EVERY branch conserves the sample's CPU budget (python_time + c_time) across (line, python|native) buckets -- the classification only moves a fixed budget, never invents/loses time. - split_atCall / split_together / split_splitToCall: the native/Python split each branch decides. - charge_nonneg: every bucket charge >= 0 (from python_time,c_time >= 0). - classify_total: the branch selector is total (exactly one branch fires). - branchA_exact_if_in_call: conditional correctness -- IF the sample truly landed in native, branch A is exact. Which branch is right (the CALL-opcode heuristic) stays an engineering hypothesis, stated not hidden. PerLineMallocAttribution.lean (scalene_memory_profiler.py:336-360): the Python reader's per-line bookkeeping, distinct from the footprint total. - perline_conserves: Sum of memory_malloc_samples[line] = total_memory_malloc_ samples, so malloc[line]/total is a genuine fraction. - python_le_malloc: memory_python_samples[line] <= memory_malloc_samples[line] (python_fraction in [0,1]) -- DERIVES the bound Attribution.lean assumed and scalene_json.py's n_python_fraction relies on. - highwater_ge_current / highwater_monotone: the per-line peak dominates the running footprint and never decreases. No sorry; standard axioms only. Full lake build green (8575 jobs). 16 modules / 133 theorems. STATUS.md, README (§15/§16 + roundup), HANDOFF updated.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes two more open gaps from the correctness map. Two new Lean modules (
sorry-free, standard axioms only; fulllake buildgreen — 8575 jobs; now 16 modules / 133 theorems).Python/native classifier —
PythonNativeClassifier.leanModels the 4-way heuristic that splits each CPU sample's time between Python and native (
scalene_cpu_profiler.py:251-341). Separates the theorem from the heuristic:charge_total/classified_conserves— every branch conserves the sample's CPU budget (python_time + c_time) across all(line, python|native)buckets. The classification only moves a fixed budget; it never invents or drops time.split_atCall/split_together/split_splitToCall— the native/Python split each branch decides.charge_nonneg— every bucket charge ≥ 0.classify_total— the branch selector is a total function (exactly one branch fires for any input).branchA_exact_if_in_call— conditional correctness: if the sample truly landed in native code, branch A is exact. Which branch is right per sample (the CALL-opcode/deferral heuristic) stays an engineering hypothesis — stated, not hidden.Per-line malloc attribution —
PerLineMallocAttribution.leanThe Python reader's per-line bookkeeping (
scalene_memory_profiler.py:336-360), distinct from the footprint total in #1080.perline_conserves— Σ over lines ofmemory_malloc_samples[line]=total_memory_malloc_samples, somalloc[line]/total(the renderer'sn_usage_fraction) is a genuine fraction.python_le_malloc— per line0 ≤ memory_python_samples ≤ memory_malloc_samples(frompython_fraction ∈ [0,1]). This derives the boundAttribution.leanassumed and thatscalene_json.py'sn_python_fraction = python/malloc ∈ [0,1]relies on.highwater_ge_current/highwater_monotone— the per-line high-water peak dominates the running footprint and never decreases.Docs
STATUS.md updated (CPU classifier row ❌→✅ for conservation /⚠️ for branch-choice; new per-line attribution row), README gains §15 + §16 and the top roundup reflects both, HANDOFF module table + next-steps updated.
Formal-only; no production code touched.