diff --git a/research/p104-retained-operand-independent-audit/CALLER.json b/research/p104-retained-operand-independent-audit/CALLER.json new file mode 100644 index 0000000000..408b02fa78 --- /dev/null +++ b/research/p104-retained-operand-independent-audit/CALLER.json @@ -0,0 +1,53 @@ +{ + "6144": { + "controls_rejected": [ + "exterior_sign", + "global_phase", + "helper_alias_collision", + "laurent_exponent_overflow", + "lost_idle", + "missing_final_main_translation", + "missing_inverse_Q_correction", + "omitted_contact_translation", + "owned_lifetime", + "wrong_route" + ], + "native_checks": { + "distinct_signed_Pauli_and_independent_phase_anchors": 346, + "fresh_helpers": 10116, + "owned_peak": 13 + }, + "ordinary_pass_upper": 126558820, + "output_sha256": "503bfe6d3aab2d60265045dd6d31f89e02414501d61013a9771f03e071d17c92", + "paid_calls": 66762, + "productive_fields": 13444, + "retained_raw_scalar_upper": 184647552, + "status": "PASS_SCOPED_CALLER_AND_TARGET_BINDING" + }, + "6167": { + "controls_rejected": [ + "exterior_sign", + "global_phase", + "helper_alias_collision", + "laurent_exponent_overflow", + "lost_idle", + "missing_final_main_translation", + "missing_inverse_Q_correction", + "omitted_contact_translation", + "owned_lifetime", + "wrong_route" + ], + "native_checks": { + "distinct_signed_Pauli_and_independent_phase_anchors": 346, + "fresh_helpers": 10116, + "owned_peak": 13 + }, + "ordinary_pass_upper": 126631036, + "output_sha256": "abfe1c4cd6dbc3f7a6ce6a348fe724af664ef5a7b9dfe66bc0a250d8dcba3a3e", + "paid_calls": 66762, + "productive_fields": 13444, + "retained_raw_scalar_upper": 184647552, + "status": "PASS_SCOPED_CALLER_AND_TARGET_BINDING" + }, + "positive_control_sha256": "b51a7d19c10faea7d569a48e9536db8ba1e7418f8dd8dfb25646cc87cc9c4009" +} diff --git a/research/p104-retained-operand-independent-audit/NEW-MAPS.json b/research/p104-retained-operand-independent-audit/NEW-MAPS.json new file mode 100644 index 0000000000..78be73b3a1 --- /dev/null +++ b/research/p104-retained-operand-independent-audit/NEW-MAPS.json @@ -0,0 +1 @@ +{"schema":"p104-6144-6167-new-dense-maps/1","maps":[[["move",3,529,0],7,"dcdb1a896ef8c98018be0111bec67cd30761a9d9190e1876841b7c6fae40d806"],[["move",3,541,0],7,"5088029cc5077a65a05587d84f43ea70d104365368dc66c3756d2f9a256d1c15"],[["move",3,549,0],7,"433074b49e9846058624e3f9b764748d571c31478ddaba68b307ad6a6071f4b8"],[["move",117,594,0],4,"a01e5f10ffa3252fd34dc542710b28b93d60c8b5f31f9eb999e847e39bf28ca9"],[["move",520,595,0],5,"6d648b121a7139022f78b425546399e4404578b3d613447db9e1053f3ec57013"],[["move",520,737,0],2,"45b79c2b4d43bddc7a713ace98aafb18fd8f1f2803fe604e821c284d2c2094fb"],[["move",529,520,0],1,"6cb29fe68a85e01b13b937dcd8723b099673b015fc38fd2f1bdfbba8a9f70aa1"],[["move",534,117,0],1,"b5c680d70aa6c2d6473e93f8ed057f167c472fb8cd48bb11e4e194acefa11e6c"],[["move",541,534,0],1,"360660134cba45a3746abd491d748ed45dee77a12980cf599fcce40227bf266d"],[["move",549,553,0],1,"e2d10177a1aa4306104f68f6988967247a88019eb44801c1bce00e466d2e6c40"],[["move",553,1047,0],2,"4400f9671eb753e8a8fd70b52c689be46c8f7352e49a763f22173f916582b4e4"],[["move",737,595,0],3,"62180012f1f2ef1338b46a982bf1f058681af990ca0204ad1b6a611f6dc0198c"],[["move",1047,593,0],3,"7887bca4a4cf3c533bac9050cee339a2514bd21e3cf219cced6502a70b936a7d"]]} diff --git a/research/p104-retained-operand-independent-audit/README.md b/research/p104-retained-operand-independent-audit/README.md new file mode 100644 index 0000000000..3e3015f2b2 --- /dev/null +++ b/research/p104-retained-operand-independent-audit/README.md @@ -0,0 +1,90 @@ +# Independent replay, delta, invoice, native, caller and funding audit of PR6144 and PR6167 + +**Result (scoped independent audit, no new κ).** An independent check of the two unadmitted conditional P104 words +above the selected record finds no error: +[PR #6144](https://github.com/CrocSwap/integer-mult-bounds/pull/6144) (DreamingOfClouds, owned registers 770, 771 +and 772 descend through the frames of helpers 705, 706 and 731, κ 0.003128386) and +[PR #6167](https://github.com/CrocSwap/integer-mult-bounds/pull/6167) (Ali Romman, a retained operand removes one +stop of root 772, κ 0.003128645). On canonical main, an own exact replay, exact structural deltas +PR6030 → PR6144 → PR6167, an own invoice recount, a dense all-column absolute-phase check of every native operator +in both inventories, the maintainers' independent caller checker and an own decimal funding engine all reproduce +the authors' claims, including the raw crossings (0.00312839320327, …328) and (0.00312865201590, …591). + +This package supplies, for both words, the same layers that the +[PR6030 admission review](../../docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md) used: Matarener's +PR5960 interpreter for the word and invoice, Clear1nsight's dense interpreter for every new native map, the +generalized independent caller checker with its positive control, and the authors' primary chain (rerun here on +Linux, both PASS). It changes no decision by itself. + +Base: canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, which contains PR6030 +(`research/p104-helper470-twin-rung-removal`), PR6144 (`research/p104-root-relay-descent-2`, head `5ec9b6da`) and +PR6167 (`research/p104-retained-operand-descent`, head `564a076b`). Inputs are pinned in [SOURCES.json](SOURCES.json). + +## What is checked + +The replay, invoice and dense-comparison functions are imported unchanged from Matarener's +[PR5827/PR5907 audit](../p104-unread-rung-independent-audit/README.md) (PR #5960); its FULL-CHECK digests and the +[PR6030 audit](../p104-6030-independent-audit/README.md)'s NEW-MAPS digests are the reference for unchanged maps. +Nothing is imported from the PR6144 or PR6167 packages except their data files and, in layer 0 only, PR6144's +`construct.py`. PR6167's word is rebuilt from the five replacements stated in its PROOF.md, without its `construct.py`. + +| Layer | Check | Result | +|---|---|---| +| 0. Sources | PR6144's pinned PR6030 word, PR6167's pinned PR6144 word and PR6144 `pricing.py` against canonical main; the PR5827 archive in all three packages; PR6144 `construct.py` on canonical PR6030 word with `EDIT.json.gz`; PR6167 PROOF.md replacements (events 12913, 12918, 13486–13488) on canonical PR6144 word | all pinned bytes equal canonical main; both regenerated words equal the shipped decompressed payloads byte for byte | +| 1. Own replay | PR6030, PR6144 and PR6167 words: strict span nesting of every MOVE, common chart of every ADD/COPY/SCALE, dyadic coefficients, owned INIT/CLEAR lifetimes, all 799 endpoint rows, helper nesting | PASS on all three; 770 public, 29 owned labels, lifetimes 31 / 31 / 32, peak 13; paid and helper histograms equal each author's `local` block | +| | PR6030 → PR6144 delta | only `program` changes (no boundary chart); exactly seven itineraries change, as in the PR6144 README: helpers 705, 706, 731 keep one hop (3→549, 3→541, 3→529), helper 732 goes 3→117→222→127, owned 770: 549→553→1047→593, 771: 541→534→117→594, 772: 529→520→737→595; INIT, CLEAR, COPY, SCALE and every other MOVE unchanged as multisets; 52 ADD removed, 71 added; paid delta −4H1 −H4 +H5 −3H6 +3H7, helper delta 0; 22,818 events ≤ 26,000 | +| | PR6144 → PR6167 delta | exactly three itineraries change: reader 451 3→595→737→…, root 772 529→520→595 and a new 770 lifetime at frame 737; exactly one INIT, one COPY (`770 ← 228` at 737) and one CLEAR are added; MOVE outside 451/772 unchanged; paid delta +H1 −H2 −H4 +H5, helper delta 0; 22,821 events | +| | margin signs | per-LOCAL margin change 4H1+H4−H5+3H6−3H7 (PR6144) and H2+H4−H1−H5 (PR6167): equal rank mass and the positive ranks are majorized by the negative ones, so by Karamata and strict concavity of r^t each is positive for 0PR6144 and PR6144->PR6167 deltas with a Karamata proof of each margin sign, nine tamper controls, own invoice recount from the physical caller, dense all-column absolute-phase check of every native map new after PR6030 (all maps in --full), own decimal funding engine with compiler-threshold integers and predecessor-failure checks, and the PR6030 admission review's independent caller checker on both words.", + "scope_change_reason": "Delta coverage of the two newest P104 candidates, as the card first_experiment asks; the maintainer intake records for PR6144 and PR6167 leave independent scientific review and source-bound replay open. Extends Matarener's PR5960 audit and the PR6030 audits to the next two words in the same line; no new construction or kappa.", + "bottleneck_link": "PR6167 is the newest conditional P104 word (kappa 0.003128645, above the selected 0.003125804). Its admission and PR6144's wait on an independent check of the changed words; this package supplies the layers the PR6030 admission review used.", + "budget_minutes": 90, + "stop_rule": "Stop when all layers pass or one fails with a concrete counterexample; no search for new itineraries or constructions.", + "outcome": "completed", + "evidence": "research/p104-retained-operand-independent-audit/RESULT.json", + "author": "Matarener (session run by Claude)", + "ai_assistance": "Prepared with Claude Opus 5.5 (Anthropic) via Claude Code.", + "open_questions": [ + { + "question": "Can the 54 strict and 4 functional outer conditions and the compiler threshold be recomputed by code that does not descend from PR5827 pricing.py?", + "why_it_matters": "This audit, like its predecessor, checks those only through the authors' chain.", + "first_step": "Write the outer inequalities from their source documents as exact rationals at kappa 625729/200000000 and compare with complete_cost.outer.", + "blocked_by": "Locating the formula source for each named margin" + }, + { + "question": "Does the uniform compiler preserve the finite native maps checked here at every recursion level?", + "why_it_matters": "Only the fixed 9-qubit local word is checked.", + "first_step": "Bind the uniform-compiler contract to the FULL-CHECK.json and both NEW-MAPS.json digests.", + "blocked_by": "Inherited native_all_columns premise" + } + ] +} diff --git a/research/p104-retained-operand-independent-audit/VERIFY.json b/research/p104-retained-operand-independent-audit/VERIFY.json new file mode 100644 index 0000000000..5ef91aee1e --- /dev/null +++ b/research/p104-retained-operand-independent-audit/VERIFY.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar", + "research/p104-root-relay-descent-2/WORD.json.gz", + "research/p104-root-relay-descent-2/RESULT.json", + "research/p104-root-relay-descent-2/EDIT.json.gz", + "research/p104-root-relay-descent-2/construct.py", + "research/p104-root-relay-descent-2/pricing.py", + "research/p104-root-relay-descent-2/inputs/pr6030-WORD.json.gz", + "research/p104-root-relay-descent-2/inputs/pr5827-source.tar", + "research/p104-retained-operand-descent/WORD.json.gz", + "research/p104-retained-operand-descent/RESULT.json", + "research/p104-retained-operand-descent/PROOF.md", + "research/p104-retained-operand-descent/inputs/pr6144-WORD.json.gz", + "research/p104-retained-operand-descent/inputs/pr6144-pricing.py", + "research/p104-retained-operand-descent/inputs/pr5827-source.tar", + "research/p104-unread-rung-independent-audit/FULL-CHECK.json", + "research/p104-unread-rung-independent-audit/verify.py", + "research/p104-6030-independent-audit/NEW-MAPS.json", + "research/p104-productive-controller/CONTROLLER.json", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-contact-independent-audit/capsule/outputs/p104-native-contact-audit-20261025/check.py", + "docs/research/pr-intake-evidence/pr6030-audit/prepare.py", + "docs/research/pr-intake-evidence/pr6030-audit/INPUTS.json", + "docs/research/pr-intake-evidence/pr6030-audit/caller-check.py", + "docs/research/pr-intake-evidence/pr6030-audit/run_caller.py", + "docs/research/pr-intake-evidence/pr6030-audit/independent.py", + "docs/research/pr-intake-evidence/pr6030-repair/run_bounded.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Serial bounded replay: authenticated inputs; pinned PR6030/PR6144 words, PR6144 pricing and the PR5827 archive equal canonical main; PR6144 word regenerated by its construct.py and PR6167 word regenerated from the five PROOF.md replacements without its construct.py; own exact replay of the PR6030, PR6144 and PR6167 words with all 799 endpoint rows and helper nesting; exact PR6030->PR6144 and PR6144->PR6167 deltas (declared itineraries, owned-operation and other MOVE multisets, paid and helper rank deltas, Karamata proof that each per-LOCAL margin change is positive on 0 0 for every 0 < t < 1, by Karamata: pad the negative ranks with zeros (0^t = 0); if the + positive ranks are majorized by the negative ones, are not a permutation of them and have the same sum, strict + concavity of x^t gives sum H(pos) > sum H(neg).""" + pos = sorted((r for r, c in m.items() if c > 0 for _ in range(c)), reverse=True) + neg = sorted((r for r, c in m.items() if c < 0 for _ in range(-c)), reverse=True) + size = max(len(pos), len(neg)) + pos, neg = pos+[0]*(size-len(pos)), neg+[0]*(size-len(neg)) + need(sum(pos) == sum(neg) and pos != neg, 'equal rank mass, different profiles') + need(all(sum(pos[:i]) <= sum(neg[:i]) for i in range(1, size+1)), 'positive ranks majorized by negative ranks') + for k in range(1, 1000): # numerical corroboration on a grid + t = k/1000 + need(sum(c*r**t for r, c in m.items()) > 0, 'margin positive at t=%s' % t) + return {'positive': [r for r in pos if r], 'negative': [r for r in neg if r]} + + +def step_delta(words, rp, new): + s = STEPS[new] + w0, w1 = words[s['base']], words[new] + need(w0.keys() == w1.keys(), 'same word fields') + need(all(w0[k] == w1[k] for k in w0 if k != 'program'), 'frames, ports, live, sizes and boundary charts unchanged') + i0, i1 = itineraries(w0), itineraries(w1) + changed = {str(r): [i0[r], i1[r]] for r in i0 if i0[r] != i1[r]} + need(changed == s['itineraries'], 'exactly the declared itineraries change: %s' % changed) + ms = lambda w, keep: Counter(json.dumps(e) for e in w['program'] if keep(e)) + for op in ('INIT', 'CLEAR', 'COPY', 'SCALE'): + c = ms(w1, lambda e: e[0] == op); c.subtract(ms(w0, lambda e: e[0] == op)) + want = Counter({json.dumps(s['owned_ops_added'][op]): 1}) if op in s['owned_ops_added'] else Counter() + need(+c == want and not -c, op+' events change exactly as declared') + other = lambda e: e[0] == 'MOVE' and str(e[1]) not in s['itineraries'] + need(ms(w0, other) == ms(w1, other), 'every MOVE outside the declared itineraries unchanged as a multiset') + d, h = diff(rp[new][0], rp[s['base']][0]), diff(rp[new][1], rp[s['base']][1]) + need(d == s['paid_delta'] and h == {}, 'paid and helper deltas %s %s' % (d, h)) + margin = Counter({int(k): -v for k, v in d.items()}) + margin = {k: v for k, v in margin.items() if v} + need(margin == s['margin'], 'per-LOCAL margin change %s' % margin) + karamata = margin_positive(margin) + ops = diff(Counter(e[0] for e in w1['program']), Counter(e[0] for e in w0['program'])) + need(ops == s['ops_delta'], 'operation counts change as declared: %s' % ops) + o = rp[new][3] + need(len(w1['program']) == s['events'] <= 26000, 'event count and cap') + need([o['public'], o['owned_fields'], o['owned_lifetimes'], o['peak_owned']] == s['inventory'], 'storage inventory') + adds = ms(w1, lambda e: e[0] == 'ADD'); adds.subtract(ms(w0, lambda e: e[0] == 'ADD')) + seq = lambda w: {r: [json.dumps(e) for e in w['program'] if e[1] == r or (e[0] in ('ADD', 'COPY') and e[2] == r)] + for r in range(w['public']+w['owned_fields'])} + s0, s1 = seq(w0), seq(w1) + out = {'itineraries': changed, 'paid_delta': d, 'helper_delta': h, + 'margin_delta_per_local': {str(k): v for k, v in sorted(margin.items()) if v}, 'margin_positive_on_0_1_by_karamata': karamata, + 'ops_delta': ops, 'add_events_removed_added': [-sum((-adds).values()), sum((+adds).values())], + 'events': [len(w0['program']), len(w1['program'])], + 'registers_with_changed_event_sequence': sorted(r for r in s0 if s0[r] != s1[r])} + log('L1_delta_'+new, **out) + return out + + +def layer1(words): + rp = {k: replay(w, k) for k, w in words.items()} + res = {k: rp[k][3] for k in rp} + for k, P in PACK.items(): + a, o = read(P/'RESULT.json')['local'], res[k] + need([a['paid'], a['helpers'], a['paid_rank_mass'], a['public_inputs'], a['owned_fields'], a['owned_lifetimes'], a['peak_owned_fields']] == + [o['paid'], o['helpers'], o['paid_rank_mass'], o['public'], o['owned_fields'], o['owned_lifetimes'], o['peak_owned']], + 'own replay statistics equal author local block '+k) + for new in STEPS: + res['delta_'+STEPS[new]['base']+'_'+new] = step_delta(words, rp, new) + return res, rp + + +def tamper_controls(words): + """Mutated PR6144 / PR6167 words must be rejected by the own replay.""" + def at(w, ev): + return w['program'].index(ev) + + def rm(ev): + return lambda w: w['program'].pop(at(w, ev)) + + def sign(ev): + def f(w): + e = w['program'][at(w, ev)]; e[-2] = str(-Q(e[-2])) + return f + + def swap_later(ev, after): # move an event to just after another one + def f(w): + e = w['program'].pop(at(w, ev)); w['program'].insert(at(w, after)+1, e) + return f + + def relay_back_705(w): # give helper 705 its PR6030 first hop back + w['program'][next(i for i, e in enumerate(w['program']) if e[:2] == ['MOVE', 705])][3] = 593 + cases = { + '6144': [('drop_root770_descent_move', rm(next(e for e in words['6144']['program'] if e[:4] == ['MOVE', 770, 549, 553]))), + ('flip_first_read_of_771', sign(next(e for e in words['6144']['program'] if e[0] == 'ADD' and e[2] == 771))), + ('relay_hop_705_restored', relay_back_705)], + '6167': [('drop_cache_copy', rm(['COPY', 770, 228, '1', 737])), + ('flip_cache_copy_sign', sign(['COPY', 770, 228, '1', 737])), + ('drop_late_operand', rm(['ADD', 451, 770, '1', 737])), + ('drop_cache_clear', rm(['CLEAR', 770, 737])), + ('root_coefficient_-2', lambda w: w['program'][at(w, ['ADD', 451, 772, '-4', 595])].__setitem__(3, '-2')), + ('copy_after_helper228_leaves_737', swap_later(['COPY', 770, 228, '1', 737], + next(e for e in words['6167']['program'][12919:] if e[:2] == ['MOVE', 228])))], + } + out, quiet = {}, M.log + M.log = lambda *a, **k: None + try: + for k, muts in cases.items(): + for name, mut in muts: + w = deepcopy(words[k]); mut(w) + try: + replay(w, 'tamper'); out[k+'_'+name] = 'ACCEPTED' + except (ValueError, IndexError) as e: + out[k+'_'+name] = 'rejected: '+str(e).split(':')[0] + finally: + M.log = quiet + need(all(v.startswith('rejected') for v in out.values()), 'tamper controls %s' % out) + log('L1_controls', **out) + return out + + +# ---------------------------------------------------------------- layer 2: invoice +def layer2(rp, results): + out = {} + for k in PACK: + P, T = invoice(rp[k][0], rp[k][1]) + cost = results[k]['complete_cost'] + AP = Counter({int(r): v for r, v in cost['paid'].items()}); AT = Counter({int(r): v for r, v in cost['targets'].items()}) + need((+P, +T) == (+AP, +AT), 'own invoice equals author complete_cost for '+k) + surplus = sum(r*v for r, v in T.items())-sum(r*v for r, v in P.items()) + out[k] = {'paid_calls': sum(P.values()), 'productive_fields': sum(T.values()), 'rank_mass_surplus': surplus, + 'paid_rank_mass': sum(r*v for r, v in P.items()), 'max_paid_rank': max(P), 'max_target_rank': max(T)} + need([out[k]['paid_calls'], out[k]['productive_fields'], surplus] == [cost['paid_calls'], cost['productive_fields'], cost['rank_mass_surplus']], + 'headline invoice '+k) + log('L2_invoice', word=k, **out[k]) + need(out['6144']['paid_calls'] == out['6167']['paid_calls'] == 66762 and out['6030']['paid_calls'] == 66834, 'paid call counts') + return out + + +# ---------------------------------------------------------------- layer 4: funding +def dec(x): + x = Q(x) + return Decimal(x.numerator)/Decimal(x.denominator) + + +def margin_fn(cost): + pad = Decimal(10)**-70 + + def margin(kap): + t, lo, hi = 1-kap, Decimal(0), Decimal(0) + for r, n in cost['targets'].items(): + v = (t*Decimal(int(r)).ln()).exp(); lo += n*v*(1-pad); hi += n*v*(1+pad) + for r, n in cost['paid'].items(): + v = (t*Decimal(int(r)).ln()).exp(); lo -= n*v*(1+pad); hi -= n*v*(1-pad) + return lo, hi + return margin + + +def layer4(results): + getcontext().prec = 80 + out = {} + for k in PACK: + cost = results[k]['complete_cost'] + margin = margin_fn(cost) + lo, hi, grid = 0, 10**12, 10**14 + while hi-lo > 1: + m = (lo+hi)//2 + if margin(Decimal(m)/grid)[0] > 0: + lo = m + else: + hi = m + need(margin(Decimal(lo)/grid)[0] > 0 and margin(Decimal(hi)/grid)[1] < 0, 'strict crossing '+k) + need([Q(lo, grid), Q(hi, grid)] == [Q(x) for x in cost['raw_root_interval']], 'crossing equals author interval '+k) + claim, tested = Q(cost['kappa']), Q(cost['strictification']['tested']) + need(claim < tested < Q(lo, grid) and margin(dec(tested))[0] > 0, 'claim < tested < crossing, tested positive '+k) + st = cost['strictification'] + need(Q(st['tail_offset']) == Q(1, 7) and int(st['cutoff']) == 16 and int(st['floor']) == 17, 'strictification constants '+k) + pw = lambda r, x: (x*Decimal(int(r)).ln()).exp() + t, u = 1-dec(tested), Decimal(1)/7 + MT = sum(n*pw(r, t) for r, n in cost['targets'].items()) + MP = sum(n*pw(r, t) for r, n in cost['paid'].items()) + MPu = sum(n*pw(r, t+u) for r, n in cost['paid'].items()) + alpha, gamma = MP/MT, MPu/(pw(16, u)*MT) + delta = sum(cost['targets'].values())*17/(pw(16, dec(tested))*MT) + lim = Decimal(125)/128 + need(alpha < 1-Decimal(10)**-12 and gamma < lim and delta < lim, 'tail ratios '+k) + dmax = Decimal(0) + for side, sgn in (('targets', -1), ('paid', 1)): + for r, n in cost[side].items(): + dmax += sgn*n*Decimal(int(r)).ln()*(pw(r, 1-Decimal('0.0034')) if sgn < 0 else pw(r, Decimal(1))) + need(dmax < 0, 'raw margin strictly decreasing on [0,.0034] '+k) + # integer compiler-threshold checks (same statements as the PR6030 admission review) + c = cost['compiler'] + gap = (tested-claim)/7 + H, j = int(c['H']), int(c['integer_test_exponent']) + need(Q(c['gap']) == gap and gap.numerator == 1 and H == gap.denominator*j, 'threshold grid '+k) + need((H+1)**1024 < 2**j and (gap.denominator*(j-1)+1)**1024 >= 2**(j-1), 'threshold and predecessor '+k) + out[k] = {'raw_crossing': [str(Q(lo, grid)), str(Q(hi, grid))], 'raw_crossing_decimal': [str(Decimal(lo)/grid), str(Decimal(hi)/grid)], + 'claim': str(claim), 'tested': str(tested), 'tested_positive': True, 'equals_author': True, + 'alpha': str(alpha)[:22], 'gamma': str(gamma)[:22], 'delta': str(delta)[:22], 'derivative_upper': str(dmax)[:22], + 'compiler_threshold_checked': True} + log('L4_funding', word=k, **out[k]) + need(Q(125, 128)**128 < Q(1, 16) and 1/(1+1024*Q(1, 10**12))+Q(4, 2**32) < 1, 'decay block and completion') + need(16**64 < 17**63 and 2*(16**1024)**64 <= (145**1024)**63, 'splitting and complement') + for new in STEPS: + old = STEPS[new]['base'] + claim = dec(results[new]['complete_cost']['kappa']) + upper = margin_fn(results[old]['complete_cost'])(claim)[1] + need(upper < 0, 'predecessor %s invoice fails at the %s claim' % (old, new)) + g = Q(results[new]['complete_cost']['kappa'])-Q(results[old]['complete_cost']['kappa']) + out['step_'+new] = {'predecessor_margin_upper_at_claim': str(upper)[:24], 'claim_gain': str(g)} + log('L4_step', step=new, **out['step_'+new]) + return out + + +# ---------------------------------------------------------------- layer 3: dense native +def layer3(words, full, jobs): + need(words['6030']['frames'] == words['6144']['frames'] == words['6167']['frames'], 'shared frame table') + inv = {k: M.inventory(words[k]) for k in PACK} + tasks = sorted(inv['6144'][0] | inv['6167'][0]) + reference = {json.dumps(d[0]): d for d in read(PRED/'FULL-CHECK.json')['maps']+read(A30/'NEW-MAPS.json')['maps']} + new = sorted(t for t in tasks if json.dumps(list(t)) not in reference) + need(not set(new) & inv['6030'][0], 'every map outside the reference digests is new after PR6030') + covered = [t for t in tasks if json.dumps(list(t)) in reference] + moves = [t for t in covered if t[0] == 'move'] + adapters = [t for t in covered if t[0] in ('main_in', 'main_out')] + chosen = tasks if full else sorted(set(new) | {t for t in covered if t[0] == 'helper'} | set(adapters[::8]) | set(moves[::64])) + if jobs > 1: + with Pool(jobs, initializer=M._init, initargs=(words['6167']['frames'],)) as pool: + done = pool.map(M.dense_task, chosen, chunksize=4) + else: + M._init(words['6167']['frames']) + done = [M.dense_task(t) for t in chosen] + done = [json.loads(json.dumps(d)) for d in done] + fresh = {json.dumps(d[0]): d for d in done if json.dumps(d[0]) not in reference} + need(sorted(fresh) == sorted(json.dumps(list(t)) for t in new), 'every new map computed') + for d in done: + k = json.dumps(d[0]) + if k in reference: + need(reference[k] == d, 'matrix digest equals reference digest for '+k) + newmaps = HERE/'NEW-MAPS.json' + if newmaps.exists() and '--write' not in sys.argv: + need(read(newmaps)['maps'] == sorted(fresh.values()), 'new-map digests equal NEW-MAPS.json') + M._init(words['6167']['frames']) + C, V, D, F = M._M['C'], M._M['V'], M._M['D'], M._M['F'] + nm = [t for t in new if t[0] in ('move', 'helper') and abs(len(F[t[1]])-len(F[t[2]])) > 0] + _, a, b, _ = nm[0] + rec, _ = C.lower_child(C.canonical_frame(9, tuple(F[a])).adjoint().then(C.canonical_frame(9, tuple(F[b])))) + actual, expected = V.recipe(rec), V.adjoint(V.frame(F[a], 9))+V.frame(F[b], 9) + fault = actual+(('phase', 1),) + need(V.tableau(fault) == V.tableau(actual) and D.first_difference(fault, expected) is not None, 'phase-only fault rejected densely') + flipped = list(actual) + i = next(i for i, g in enumerate(flipped) if g[0] == 'C') + flipped[i] = ('C', flipped[i][1], -flipped[i][2]) + need(D.first_difference(tuple(flipped), expected) is not None, 'wrong child sign rejected') + native = {} + for k in ('6144', '6167'): + w, an = words[k], read(PACK[k]/'RESULT.json')['native'] + signed = len({(t[1], t[2]) for t in inv[k][0] if t[0] in ('move', 'helper')}) + need([signed, 2*(w['public']-2*len(w['live'])), 2*len(w['live'])] == [an['distinct_maps'], an['helper_normalizers'], an['main_adapters']], + 'distinct signed maps, helper normalizers and main adapters equal the author native block '+k) + native[k] = {'tasks': len(inv[k][0]), 'distinct_moves': inv[k][1], 'distinct_helper_pairs': inv[k][2], 'distinct_signed_maps': signed} + out = {'per_word': native, 'union_tasks': len(tasks), 'covered_by_reference_digests': len(covered), + 'new_after_pr6030': [d[0]+[d[1]] for d in sorted(fresh.values())], + 'new_in': {k: sorted(json.dumps(list(t)) for t in new if t in inv[k][0]) for k in ('6144', '6167')}, + 'control_map': [a, b], 'controls': {'phase_only_fault': 'rejected', 'wrong_child_sign': 'rejected'}, + 'reference_sha256': {'pr5960_full_check': sha256((PRED/'FULL-CHECK.json').read_bytes()).hexdigest(), + 'pr6030_audit_new_maps': sha256((A30/'NEW-MAPS.json').read_bytes()).hexdigest()}} + log('L3_dense', checked=len(done), of=len(tasks), new=len(new), full=full) + return out, sorted(fresh.values()) + + +def main(): + full = '--full' in sys.argv + jobs = int(sys.argv[sys.argv.index('--jobs')+1]) if '--jobs' in sys.argv else 1 + authenticate() + words = {k: read(P/'WORD.json.gz') for k, P in PACK.items()} + results = {k: read(P/'RESULT.json') for k, P in PACK.items()} + out = {'layer0_sources': layer0(words)} + out['layer1_replay'], rp = layer1(words) + out['layer1_replay']['tamper_controls'] = tamper_controls(words) + out['layer2_invoice'] = layer2(rp, results) + out['layer4_funding'] = layer4(results) + if '--no-dense' in sys.argv: + print('PASS layers 0, 1, 2, 4 (dense layer skipped)') + return + out['layer3_dense'], fresh = layer3(words, full, jobs) + if '--write' in sys.argv: + (HERE/'NEW-MAPS.json').write_text(json.dumps({'schema': 'p104-6144-6167-new-dense-maps/1', 'maps': fresh}, separators=(',', ':'))+'\n') + out['layer3_dense']['new_maps_sha256'] = sha256((HERE/'NEW-MAPS.json').read_bytes()).hexdigest() + out = json.loads(json.dumps(out, sort_keys=True, default=str)) + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(json.dumps(out, indent=1, sort_keys=True)+'\n') + else: + need(out == read(HERE/'RESULT.json'), 'complete result equals RESULT.json') + print('PASS_P104_6144_6167_INDEPENDENT_AUDIT', 'full' if full else 'subset') + + +if __name__ == '__main__': + main()