diff --git a/research/factored-code-tape/PROOF.md b/research/factored-code-tape/PROOF.md new file mode 100644 index 0000000000..79a66772cc --- /dev/null +++ b/research/factored-code-tape/PROOF.md @@ -0,0 +1,128 @@ +# A complete local tariff for the factored mode code + +This is a conditional arithmetic construction on a fixed classical multitape +machine. It does not establish common-coordinate access in a Gaussian caller. +The source matrix, rounding rule and original tape contract are the inputs in +SOURCES.json. The scalar factorization was first recorded in +[Discussion #5314](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314). +This package adds a fixed-word instruction table, temporary allocation and a +complete local tariff. + +## Domain and schedule + +Use the same integer grid, input bound H>=0 and word width +W=bit_length(56H+2)+1 as the source kernel. Each of 112 owner tapes contains N +signed W-bit words, with one delimiter per word and a final end marker. +Real and imaginary components are separate records. The source mode matrix +is fixed in the finite control. The emitter checks its fourteen sign cubes; +it is a certificate generator, not a variable-matrix machine oracle. + +There are eight mode tapes, eight temporary tapes, one division tape and one +readonly bound tape: 130 tapes in total. The 17 owned words start with arbitrary +bits. Initialize them once. On each coordinate validate all 112 owner values, +run the 308-instruction gather, run the eight source ROUND52 transducers, +run the 280-instruction scatter, clear the 16 mode/temporary words and advance +all owner heads. The division word is already zero after each source range or +division operation. Rewind all owner tapes at the end. For N=0, initialization +and final framing still run. + +All gathers finish before the first owner update. The emitted gather and +scatter programs use separate temporary identifiers. The allocator computes +last uses, then reuses a last-used input slot for an output when possible. +It rejects a read before definition, an allocation above eight words and +any live temporary at the end. It emits literal tape indices 0,...,127 for +signed sums. Division uses tape 128 and the readonly bound is tape 129. +No arbitrary native helper tape appears. + +The actual matrix has fourteen four-mode supports, each with the eight +projective sign patterns. For one group, signed source views identify the +rows with (1,+/-1,+/-1,+/-1). Four pair sums and four pair differences cost 8. +The sum of differences costs 3. Three selected transforms of the four sums +cost 7. Four updates to global modes cost 4. Thus gather costs14*22=308. +For scatter, form a+b,a-b,c+d,c-d in 4 sums, form each of the eight corrections +in one sum, and perform eight owner updates:14*20=280. Source signs are part +of each signed binary instruction. Copies or sign maps are not extra hidden +instructions: the next section gives a direct two-input signed primitive. + +## Finite signed primitive and range + +An instruction is z=a*x+b*y, with a,b in {-1,1}. Read the two source bits +before writing the destination bit. Start carry at [a=-1]+[b=-1]. At bit j, +add (x_j xor [a=-1]), (y_j xor [b=-1]) and the carry; write the low bit and +retain the remaining carry. Carry is in {0,1,2}. This is the usual two's +complement identity for the sum of two signed words. The destination may +be a last-used source word: the current bits are read first, and later bits +are not changed. A forward scan and a return sweep cost at most 2W+4 +transitions. All addressed heads move together; unaddressed heads stay put. +The destination is written in full, so its prior contents do not matter. + +Each temporary gather sum has magnitude at most8H; each partial mode has +magnitude at most56H. The source division returns q with +|q|<=14H/13+1/2. A scatter temporary is a signed sum of at most four such +values. Its magnitude is at most56H/13+2. An updated owner has magnitude at +most69H/13+2. All are at most56H+2. Hence every mathematical signed result +fits W bits and the modular carry loop equals that result. Division and +range validation are the authenticated source bit loops. Rounding occurs +at exactly the same eight mode values as before. The final owner words +therefore agree for every valid input, including signed ties. + +The allocator attains eight temporary words. One can also see this directly: +form the four sums and differences; reduce the differences first; form each +sum-pair's sum before its difference releases the old pair; then form the +three required coefficients and consume all four outputs. Scatter needs +only four pair values and one current correction. The runtime representation +is a reference interpreter of these fixed words. It is not a measured +physical TM or a benchmark of the full Gaussian caller. + +## Complete tariff + +Reuse the source primitive bounds: validation 8W+16, ROUND52 at most 24W+64, +and CLEAR/INIT at most 2W+4. Signed binary sums have the bound proved above. +All primitives return their participating heads to the current word start. +Owner advance costs W+1 with all 112 heads moving together. Final rewind +costs N(W+1)+2. Include 62 further framing transitions. + +```text +T <= 17(2W+4) + + N[112(8W+16) + 588(2W+4) + 8(24W+64) + + 16(2W+4) + (W+1)] + + N(W+1) + 64 + = N(2298W+4722) + 34W+132. +``` + +At most 130T individual head moves, symbol reads and symbol writes suffice. +The storage bound is 112[N(W+1)+1] owner cells, 17(W+1) owned scratch cells, +and W+1 readonly bound cells, plus fixed framing. There are 144N+17 complete +zero-writing scans: 112 range clears, 16 internal division clears and 16 final +mode/temporary clears per coordinate, plus 17 initial clears. This cleanup +is paid classical writing, not reversible uncomputation. + +The old bound is N(2898W+5922)+18W+100. Old minus new equals +N(600W+1200)-16W-32, which is positive for every N>=1 and W>=3. This compares +constructive upper bounds in two stated fixed-tape models. The new machine +has130 tapes rather than122 and uses eight more temporary words. It is not +an optimality or measured speed claim. The rounded map, two-grid-unit local +error and noninjectivity are unchanged. + +## Evidence and remaining obligations + +The verifier checks all 112 gather and eight scatter basis columns with the +emitted finite-word instructions. It compares 48 mixed/extreme coordinate +vectors in 36 batches, including N=0,1,3 and H=0,1,6,26,51,250, against the +actual source kernel. It starts every owned scratch bit dirty and requires +all 17 words clean. An independent primitive invoice sums to the displayed +formula. A changed numerical sign and owner alias are rejected. Hash pins +bind every external input; source modules load from their authenticated +source bytes, without a bytecode-cache import. + +The written range, carry, schedule and sweep arguments give the quantified +local result. Finite replay does not establish the full physical caller, +common-coordinate field access, native Gaussian accuracy, compiler reserve, +reversible ownership, a new supplier or a new kappa. Extra wrappers and +field movement remain charged caller obligations. + +Credit JoyboyBrian's PR #5035 for the source divider, validation, rounding and +classical sweep contract; Dillon's PR #4933 for the physical mode factorization; +Dugongue and retained native/precision/compiler authors for their source work. +The Walsh transform is standard. New emitted schedule, allocation, tariff, +proof and checks: Ali Romman with OpenAI Codex assistance. Apache-2.0. diff --git a/research/factored-code-tape/README.md b/research/factored-code-tape/README.md new file mode 100644 index 0000000000..88236f0065 --- /dev/null +++ b/research/factored-code-tape/README.md @@ -0,0 +1,63 @@ +# A smaller local tape bound for inverse recoding + +This conditional arithmetic construction lowers the actual source mode code +to a 130-tape classical machine. Its complete local bound is +`N(2298W+4722)+34W+132`, compared with the source bound +`N(2898W+5922)+18W+100`. The new bound is smaller for every N>=1. +The machine uses eight extra temporary words. Its rounded numerical map, +eight division calls and two-grid-unit local error are unchanged. + +[PROOF.md](PROOF.md) gives the fixed-word schedule, range and sweep proof. +[kernel.py](kernel.py) emits 308 gather and 280 scatter instructions and +allocates at most eight temporary words. [RESULT.json](RESULT.json) records +the exact replay. [SOURCES.json](SOURCES.json) pins all consumed input bytes +at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority 7. + +This adds the physical arithmetic bill left open by +[Discussion #5314](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314), +whose scalar factorization is reused with credit. The +[scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314#discussioncomment-19150518) +excludes the complete coded caller. All112 owner tapes are distinct and +provided at common coordinates. All17 owned scratch words return zero; +this is paid classical overwriting, not reversible cleanup. + +## Reproduce + +Use CPython 3.12 and the standard library from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/factored-code-tape +python3.12 -I -O -W error -B research/factored-code-tape/verify.py +``` + +Expected marker: PASS_FACTORED_CODE_TAPE. Both registered modes check all 112 +and eight basis columns, 36 batches, 48 mixed/extreme source comparisons, +N=0/1/3, dirty scratch return, independent tariff addition and numerical-sign +and alias controls. Source imports use authenticated bytes. The emitted bit +instructions execute; the complete target TM is specified by a sweep proof, +not measured as a full physical caller. + +No native Gaussian, compiler, outer ledger, Lean or selected replay ran. +The Gaussian paid profile and complete kappa calculation are unchanged. +Common-coordinate access, wrappers, field movement and full error funding +remain caller obligations. This is author-checked evidence; independent +human or proof-kernel acceptance is not claimed. + +## Open next questions + +Bind the tariff and 17-word workspace to one affordable complete caller with +legal common-coordinate access. First charge its wrappers and physical +movement and retain its error budget. Those missing caller contracts block +admission; they are not zero-cost operations. The structured question is in +TASK.json. + +## Credit + +[PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035) by JoyboyBrian +supplies the finite divider, rounding, validation and original sweep tariff. +[PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933) by Dillon +supplies the source physical mode factorization. Dugongue and retained +native, ownership, precision and compiler authors keep their source credit. +Standard Walsh butterflies are not claimed as new. New lowering, allocation, +tariff and checks: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. Frozen sources and notices remain unchanged. diff --git a/research/factored-code-tape/RESULT.json b/research/factored-code-tape/RESULT.json new file mode 100644 index 0000000000..f68e178203 --- /dev/null +++ b/research/factored-code-tape/RESULT.json @@ -0,0 +1,18 @@ +{ + "status": "PASS_FACTORED_CODE_TAPE", + "gather_columns": 112, + "scatter_columns": 8, + "mixed_and_extreme_vectors": 48, + "batch_cases": 36, + "signed_sums": 588, + "temporary_words": 8, + "tapes": 130, + "scratch_words": 17, + "transition_upper": "N(2298W+4722)+34W+132", + "zero_scans": "144N+17", + "controls": [ + "wrong_sign", + "owner_alias" + ], + "physical_caller_run": false +} diff --git a/research/factored-code-tape/SOURCES.json b/research/factored-code-tape/SOURCES.json new file mode 100644 index 0000000000..cc3f264134 --- /dev/null +++ b/research/factored-code-tape/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coded-inverse-fixed-grid/PROOF.md", + "usage": "input", + "git_blob": "a465ed5ce6b0bd7ac03bc79e72003380a839d7f4", + "sha256": "2bf523cf4f4b3e6bd90805e86f2cbf5d1d85142c16e751e72f09480bcdbee5cd" + }, + { + "path": "research/coded-inverse-fixed-grid/kernel.py", + "usage": "input", + "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b", + "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + } + ] +} diff --git a/research/factored-code-tape/TASK.json b/research/factored-code-tape/TASK.json new file mode 100644 index 0000000000..740ddce86d --- /dev/null +++ b/research/factored-code-tape/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "A fixed-word lowering and complete classical 130-tape tariff for the actual 588-sum inverse-code schedule.", + "scope_change_reason": "The live inverse-code caller needs a complete local bit/tape bill. Discussion5314 gave only the scalar factorization. This result supplies emitted instructions, temporary allocation, input validation and paid cleanup.", + "bottleneck_link": "Physical coded callers need bounded finite recoding with all ordinary work and owned state charged.", + "budget_minutes": 60, + "stop_rule": "Stop after the source-bound local fixed-tape bound and exact numerical-map comparison; do not change Gaussian jobs or selected kappa.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json: complete basis checks, 36 bounded batches, 48 source-kernel coordinate comparisons, dirty scratch return, independent invoice and sign/alias controls.", + "author": "Ali Romman with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.", + "open_questions": [ + { + "question": "Can an affordable complete caller supply the common-coordinate owner layout and fund all wrappers and movement?", + "why_it_matters": "The local arithmetic bound does not include physical field access or recursive Gaussian calls.", + "first_step": "Bind this tariff and its 17-word workspace to one named caller layout and its error budget.", + "blocked_by": "Complete physical caller and common-coordinate ownership contracts." + } + ] +} diff --git a/research/factored-code-tape/VERIFY.json b/research/factored-code-tape/VERIFY.json new file mode 100644 index 0000000000..f6256936ef --- /dev/null +++ b/research/factored-code-tape/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-inverse-fixed-grid/PROOF.md", + "research/coded-inverse-fixed-grid/kernel.py", + "research/coded-native-caller/NORMALIZERS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source pins, all linear basis columns, complete bounded batches, source word equality, paid scratch return, independent tariff and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source pins, all linear basis columns, complete bounded batches, source word equality, paid scratch return, independent tariff and semantic controls." + } + ] +} diff --git a/research/factored-code-tape/kernel.py b/research/factored-code-tape/kernel.py new file mode 100644 index 0000000000..b88165f8be --- /dev/null +++ b/research/factored-code-tape/kernel.py @@ -0,0 +1,161 @@ +"""Fixed-word lowering of the source mode map. +Ali Romman with OpenAI Codex assistance. Apache-2.0. +The source ROUND52 and range checks retain JoyboyBrian's credit. +""" +from collections import defaultdict + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def groups_for(columns): + need(len(columns) == 8 and all(len(c) == 112 and all(type(v) is int and v in (-1, 0, 1) for v in c) for c in columns), 'Mode coefficients') + groups = defaultdict(dict) + for i in range(112): + support = tuple(j for j in range(8) if columns[j][i]) + need(len(support) == 4, 'Four modes per owner') + sign = columns[support[0]][i] + mask = sum((columns[support[k+1]][i] != sign) << k for k in range(3)) + need(mask not in groups[support], 'Repeated cube vertex') + groups[support][mask] = (i, sign) + need(len(groups) == 14 and all(set(g) == set(range(8)) for g in groups.values()), 'Complete sign cubes') + return groups + + +class Builder: + def __init__(self): + self.code = [] + self.next = 0 + + def add(self, left, right, a=1, b=1, target=None): + if target is None: + target = ('t', self.next) + self.next += 1 + self.code.append((target, left, right, a, b)) + return target + + +def emit(columns): + groups = groups_for(columns) + g, s = Builder(), Builder() + for support, group in groups.items(): + sums, diffs = [], [] + for mask in range(0, 8, 2): + i, si = group[mask] + j, sj = group[mask+1] + sums.append(g.add(('o', i), ('o', j), si, sj)) + diffs.append(g.add(('o', i), ('o', j), si, -sj)) + odd = g.add(g.add(diffs[0], diffs[1]), g.add(diffs[2], diffs[3])) + t0 = g.add(sums[0], sums[1]) + t1 = g.add(sums[0], sums[1], b=-1) + t2 = g.add(sums[2], sums[3]) + t3 = g.add(sums[2], sums[3], b=-1) + out = [g.add(t0, t2), odd, g.add(t1, t3), g.add(t0, t2, b=-1)] + for k, value in zip(support, out): + g.add(('m', k), value, target=('m', k)) + a, b, c, d = [('m', k) for k in support] + u = [s.add(a, b), s.add(a, b, b=-1)] + v = [s.add(c, d), s.add(c, d, b=-1)] + for mask in range(8): + j = ((mask >> 1) ^ (mask >> 2)) & 1 + sign = 1 - 2*((mask >> 1) & 1) + value = s.add(u[mask & 1], v[j], b=sign) + i, own_sign = group[mask] + s.add(('o', i), value, b=-own_sign, target=('o', i)) + return allocate(g.code), allocate(s.code) + + +def allocate(code): + last = {} + for pos, (_, left, right, _, _) in enumerate(code): + for source in (left, right): + if source[0] == 't': + last[source] = pos + live, free, result = {}, set(range(120, 128)), [] + peak = 0 + def locate(ref): + if ref[0] == 'o': return ref[1] + if ref[0] == 'm': return 112 + ref[1] + need(ref in live, 'Read before temporary definition') + return live[ref] + for pos, (target, left, right, a, b) in enumerate(code): + li, ri = locate(left), locate(right) + for source in set((left, right)): + if source[0] == 't' and last[source] == pos: + free.add(live.pop(source)) + if target[0] == 't': + need(bool(free), 'More than eight temporary words') + dst = min(free) + free.remove(dst) + live[target] = dst + else: + dst = locate(target) + peak = max(peak, len(live)) + result.append((dst, li, ri, a, b)) + need(not live, 'Live temporary at program end') + return result, peak + + +def signed_sum(words, instruction): + dst, left, right, a, b = instruction + need(a in (-1, 1) and b in (-1, 1), 'Signed sum coefficients') + carry = int(a < 0) + int(b < 0) + for bit in range(len(words[dst])): + total = (words[left][bit] ^ int(a < 0)) + (words[right][bit] ^ int(b < 0)) + carry + words[dst][bit] = total & 1 + carry = total >> 1 + + +def invoice(width, components): + need(type(width) is int and width >= 3 and type(components) is int and components >= 0, 'Geometry') + return {'tapes': 130, 'scratch_words': 17, 'signed_sums': 588*components, + 'round52_calls': 8*components, 'range_checks': 112*components, + 'zero_scans': 144*components+17, + 'transitions_upper': components*(2298*width+4722)+34*width+132, + 'scratch_cells': 17*(width+1), + 'owner_cells': 112*(components*(width+1)+1), 'bound_cells': width+1} + + +def component(owner_words, scratch, bound, program, source): + width = source.word_width(bound) + need(len(owner_words) == 112 and len(scratch) == 17, 'Owner and scratch counts') + words = owner_words + scratch + need(len({id(w) for w in words}) == len(words), 'Word aliases') + for word in words: + source.check_word(word, width) + limit = source.encode(bound, width) + for word in owner_words: + need(source.within_bound(word, limit, words[128]), 'Input range') + (gather, gp), (scatter, sp) = program + for instruction in gather: + signed_sum(words, instruction) + for mode in words[112:120]: + source.round52_into(mode, words[128]) + for instruction in scatter: + signed_sum(words, instruction) + for word in words[112:128]: + source.clear(word) + need(not any(words[128]), 'Divider return') + return {'gather': len(gather), 'scatter': len(scatter), 'peak_temporaries': max(gp, sp)} + + +def recode_many(owner_records, scratch, bound, columns, source): + width = source.word_width(bound) + need(len(owner_records) == 112 and len(scratch) == 17, 'Record geometry') + count = len(owner_records[0]) + need(all(len(row) == count for row in owner_records), 'Aligned records') + all_words = [w for row in owner_records for w in row] + scratch + need(len({id(w) for w in all_words}) == len(all_words), 'Record aliases') + for word in all_words: + source.check_word(word, width) + for word in scratch: + source.clear(word) + program = emit(columns) + receipt = {'gather': len(program[0][0]), 'scatter': len(program[1][0]), + 'peak_temporaries': max(program[0][1], program[1][1])} + for coordinate in range(count): + got = component([row[coordinate] for row in owner_records], scratch, bound, program, source) + need(got == receipt, 'Fixed program receipt') + return {**receipt, **invoice(width, count)} diff --git a/research/factored-code-tape/verify.py b/research/factored-code-tape/verify.py new file mode 100644 index 0000000000..84ad7d11d5 --- /dev/null +++ b/research/factored-code-tape/verify.py @@ -0,0 +1,90 @@ +"""Check the complete local kernel and emitted words. Apache-2.0. +Ali Romman with OpenAI Codex assistance. +""" +from pathlib import Path +from hashlib import sha256 +from types import SimpleNamespace +import json +import argparse + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + +def need(ok, why): + if not ok: raise ValueError(why) + +def module(path): + ns={'__name__':path.stem,'__file__':str(path)} + exec(compile(path.read_bytes(),str(path),'exec'),ns) + return SimpleNamespace(**ns) + +def run(): + pins=json.loads((HERE/'SOURCES.json').read_text()) + for item in pins['files']: + if item['usage']=='input': + need(sha256((ROOT/item['path']).read_bytes()).hexdigest()==item['sha256'],'Source pin') + source=module(ROOT/'research/coded-inverse-fixed-grid/kernel.py') + new=module(HERE/'kernel.py') + modes=json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text())['mode_columns'] + (gather,gp),(scatter,sp)=new.emit(modes) + need((len(gather),len(scatter))==(308,280),'Emitted operation count') + need(max(gp,sp)<=8,'Temporary allocation') + for column in range(112): + words=[[0]*9 for _ in range(129)];words[column]=source.encode(1,9) + for instruction in gather:new.signed_sum(words,instruction) + need([source.decode(w) for w in words[112:120]]==[c[column] for c in modes],'Gather basis') + for column in range(8): + words=[[0]*9 for _ in range(129)];words[112+column]=source.encode(1,9) + for instruction in scatter:new.signed_sum(words,instruction) + need([source.decode(w) for w in words[:112]]==[-v for v in modes[column]],'Scatter basis') + vectors=0;batch_cases=0 + for H in (0,1,6,26,51,250): + W=source.word_width(H) + for N in (0,1,3): + data=[[[((i*i+17*j+13)%(2*H+1))-H for i in range(112)] for j in range(N)], + [[H if i%2 else -H for i in range(112)] for _ in range(N)]] + for columns in data: + records=[[source.encode(columns[j][i],W) for j in range(N)] for i in range(112)] + scratch=[[1]*W for _ in range(17)] + receipt=new.recode_many(records,scratch,H,modes,source) + need(all(not any(w) for w in scratch),'Owned return') + for j,x in enumerate(columns): + old=[source.encode(v,W) for v in x] + source.recode(old,modes,H,[[1]*W for _ in range(9)]) + need([row[j] for row in records]==old,'Exact source word equality') + vectors+=1 + bound=17*(2*W+4)+N*(112*(8*W+16)+588*(2*W+4)+8*(24*W+64)+16*(2*W+4)+W+1)+N*(W+1)+64 + need(receipt['transitions_upper']==bound,'Independent invoice sum') + if N: + need(bound