Skip to content

Keep the fraction in a variable that starts as an int and is later assigned a quotient, including one that a function returns - #318

Merged
luisleo526 merged 9 commits into
mainfrom
float-reassignment-storage
Nov 3, 2026
Merged

luisleo526 merged 9 commits into
mainfrom
float-reassignment-storage

Conversation

@luisleo526

Copy link
Copy Markdown
Contributor

What changes

A variable that starts from an int and is later assigned a quotient (s = n then s := s / 2) was declared int in the generated C++, and the quotient was cut to an int when it was written. Every later read, a loop start or a plain qty = s, saw only the integer part. TradingView keeps the fraction, whatever the variable's declaration: inferred, an explicit int, a literal start or a series. This change stores such a variable as a double.

Measured on TradingView (BTCUSDT 1h, default inputs, 205 entries each) and pinned from the recorded tapes: int s = n; s := s / 2; qty = s trades 2.5 (the engine gave 2.0), the same for the inferred and the literal forms, the series form trades 2.5 and 3.5 (the engine gave 2.0 and 3.0), and the loop form s = n; s := s / 2; for i = s to s + 2 trades 10.5 (the engine gave 9.0). Main gives the engine values above; the released v1.9.1 was run on the loop form only and gives 9.0 there.

How it works: a pre-pass over the := writes joins the fractional evidence into each int declaration before any reader, member or history snapshot is recorded. It does not look at the int keyword. The loop counter and the storage share one value query (the counter-only query is removed), so there is one rule for "this value can be fractional". A write of a float literal, a quotient that is proved integral, Pine v5 sources and a variable only ever assigned ints keep their present C++.

A variable declared inside a function has the same problem when the function returns it: measure(int seed) => int s = seed; s := s / 2; s (and the same with var int s) returned 2 for seed = 5 where TradingView returns 2.5 (205 entries each). The function's return type was inferred from the written int, so the value was cut at the return; the return inference now reads the same widening annotation. Both the var and the plain-local source are fixed: on main the engine's quantity is 2 on all 205 entries of each, against TradingView's 2.5; on this head both give 2.5 on all 205 entries (measured natively on this exact head against the TradingView tape).

Known gaps

  • A loop whose start is the result of such a function and whose step is a float (for i = measure(5) to 6 by 0.5, x = measure(n) then for i = x to 6 by 0.5) stays refused with PF-E2079, as an int start is: the float-step check merged earlier already refuses these shapes, and this change does not alter it. TradingView refuses them too (CE10106, measured); the tapes are pinned as fixtures.
  • A helper parameter fed a quotient (count_from(n / 2)) still gets an int counter: TradingView 10.5, the engine 9.0, the same on main and on the release. A test named as a gap flips when it closes.
  • A name declared more than once in a file (sibling locals, a local shadowing a global or a parameter, repeated helper clones) is not widened, because the emitter looks storage up by name (codegen/types.py, _slot_scalar_cpp_type); the guard is in loop_types.py.
  • Tuple targets, compound assignments (s /= 2), methods and for-in binders keep their present behaviour. A direct int x = a / b initializer was not measured on TradingView and is unchanged.
  • A loop with a float step that starts at a widened variable (s = n; s := s / 2; for i = s to 6 by 0.5, also with int s = n) is refused with PF-E2079 as before: TradingView refuses it too (CE10106, measured), because it types such a variable as an int for the loop's compile check while its value keeps the fraction. The loop check reads the declared int; only the value and the storage are a double.

Verification

  • Full suite on a host without the engine checkout, base main and this head, same command: base 13,778 passed, 0 failed; head 13,883 passed, 0 failed; nothing fails only on the head.
  • Engine-paired run on the cloud runner (compile environment present), measured against the current engine main 84120311: 19,347 passed, 235 skipped, 0 failed; compile corpus 312 passed; the parity gate step passes. The same run against the previous engine main 8d0f9e75 gave the same counts (history): 19,347 passed, 235 skipped, 0 failed; compile corpus 312 passed; the parity gate step passes.
  • Native values against the recorded TradingView tapes (exact decimals, by fill time), main versus this head (main measured on the previous engine main 8d0f9e75, not re-run on 84120311; this head measured on both): the function-returned quantity sources (var and plain local): main 0 of 205 entries equal (engine 2, TradingView 2.5), this head 205 of 205 for both. The five reassignment sources: main 0 of 205 entries equal for each (engine 9 against TradingView 10.5 for the loop form; engine 2 against 2.5 for the explicit-int, plain and literal forms; engine 2 and 3 against 2.5 and 3.5 for the series form), this head 205 of 205 for each. No source that is equal to its tape on main (measured on engine 8d0f9e75) is unequal on this head (measured on 8d0f9e75 and on 84120311).
  • Translated before and after over the complete 188-source comparison set, with every row's full generated-C++ hash or refusal text compared (translate-level): 188 sources on each side (78 translate, 110 are refused on both); seven differ, and they are exactly the five reassignment sources and the two function-returned sources; nothing is newly refused and nothing is newly translated; the six callable float-step sources that are refused are refused identically before and after.
  • Population before and after (main as BEFORE), translate outcome and generated-code signature per source: a second set of scripts 1,939 sources (1,330 translated and 609 refused, identically before and after), the population 1,384 (1,374 translated, 10 refused), and the tests tree with the corpus 955 (854 and 101): 4,278 source rows in all; and 52 import pairs (10 distinct sources in 52 library environments), all 52 identical: none changed, none newly refused or translated. Limit: the comparison shows that no translated output of these sources changes; how many of them have the reassignment or function-returned shape this change fixes was not counted, so it shows the change does not disturb them, not that the shape occurs in them; the fix itself is shown by the native comparisons above.
  • Full-population parity sweep of this exact head, paired with engine main 84120311 (the current engine main: the sweep was repeated after the engine's last merge), against the active baseline (engine 84120311 with codegen daa51025, the pair now on main): verdict PASS, no improvement and no regression. 7,989 probes are comparable and every one is measured on both sides; the hard gate evaluates 1,009 with 0 moves and 0 regressions, the target gate evaluates 6,980 with 0 moves up or down, and no band gains or loses an entrant. The gate verdict is recorded for this engine and codegen pair and reads back as PASS, no-improve-no-regression; advancing the baseline after the merge is a separate step. An earlier sweep of the same head against the previous engine main 8d0f9e75 and the previous baseline gave the same verdict; it is history and not the pairing used here.
  • Released versions: main before this change gives the integer part for all of these shapes (measured natively above). The released v1.9.1 was run only on the loop form (s = n; s := s / 2; for i = s to s + 2), where it also gives the engine value 9.0 against TradingView's 10.5; the other shapes were not run on v1.9.1.

🤖 Generated with Claude Code

luisleo526 and others added 9 commits November 3, 2026 07:10
…at can be fractional

TradingView keeps the fraction when a variable that starts from an int is later assigned a quotient (`s = n` then `s := s / 2`), whatever its declaration form: inferred, an explicit `int`, a literal start or a series. We declared the variable `int` from its initializer and cut the quotient to an int when it was written, so every later read, a loop start or a plain `qty = s`, saw only the integer part (2 where TradingView trades 2.5; 9.0 where it trades 10.5).

A pre-pass over the `:=` writes now joins the fractional evidence into each int declaration before any reader, member or history snapshot is recorded, so the storage is a double. It does not look at the `int` keyword. A write of a float literal, a quotient that is proved integral, and a variable only ever assigned ints keep their present C++. The loop counter and the storage share one value query, so there is a single rule for "this value can be fractional"; the counter-only query is removed.

Measured on TradingView and pinned from the recorded tapes: the explicit-int, plain, literal and series forms and the loop forms. Names declared more than once, tuple targets, compound assignments, methods and an untyped helper parameter fed a quotient keep their present behaviour and are named in the tests.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
The three rows that write a float expression into an int variable looked for the substring `_pf_v` in every write to the variable, but the state-checkpoint line `this->s = _pf_script_state_checkpoint_->_pf_value_1;` carries a member named `_pf_value_1`, so the rows failed on a line that has no narrowing. They now look for the helper's own text: an int cast of the written value and the int na value.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…and engine-only rows, and state the same-name limit

A loop start that is a function parameter takes the type of the parameter's own hint in the counter check (an int parameter with a float step is refused, a float or untyped one translates), where the check previously followed the function's return type. Three rows pin that branch directly and three more compare the whole generated C++ of a parameter-fed loop against the frozen reference, so the translation of such a loop is shown unchanged. The registry probe `f(float p) => p; f(2)`, which TradingView refuses and we translate, is noted as a known difference in the safe direction; these rows make no TradingView claim.

The explicit-int loop row is named and described as a consistency row (the same shape as the measured untyped loop; TradingView was not run on it), and the rows that compare the engine with an engine twin say so. A comment at the name-collision guard records why a name declared more than once is not widened: the emitter looks storage up by name and cannot tell two same-named bindings apart. No generated C++ changes.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…rage are double

TradingView refuses a float-step loop whose start is a variable that starts as an int and is later assigned a quotient (`s = n`, `s := s / 2`, `for i = s to 6 by 0.5`, and the same with `int s = n`): its compile check types the variable as a series int, while the value it holds is a double. The storage change made the variable a float for the compile check too, so both scripts would have been accepted.

The widened declaration now reads as float only in the value query, which chooses the loop counter family and the storage; the check query that refuses a float step keeps the hint or the initializer's int. The two scripts are refused with the same message as before the storage change, and a loop with the default step or an int step from the same variable keeps its double counter and its translation. No generated C++ changes.

The rows that note a difference from TradingView on a helper parameter now call it a known gap.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… check the engine's location against it

The two refusal rows now carry the span TradingView reports for the step literal (line 7, columns 19 to 21, last column inclusive), and the row asserts that the engine refuses at the same columns, where it previously checked only the code and the message. Test data and assertions only; no generated C++ changes.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ough the function's return type

A persistent `var int s` declared inside a function, assigned a quotient and returned, still gave the integer part when the function was called: the member was already a double, but the function's return type was inferred from the written `int` hint, so the value was cut at the return. The return inference now reads the same widening annotation as the declaration, so such a function returns a double and the caller sees the fraction. A function whose variable is written only with ints keeps its present C++.

Rows: a translation row for the callable `var` form and its `varip` sibling, frozen-C++ controls for int-only writes in the same shapes, and the scope rows are now named and described as engine-consistency controls (the expected quantity is the plain-global tape's value; TradingView was not run on each storage scope).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… of a callable result as a float-step loop start

TradingView accepted both callable sources (a persistent `var int s` and a plain `int s` declared inside a function, assigned a quotient and returned) and traded 2.5 on all 205 entries. The two sources are now byte-exact fixtures with their measurement records (quantity, entry count, full source and tape digests), registered with the native per-entry quantity rows and the source-digest checks. The scope rows that carry the same quotient into other storage scopes stay engine-consistency controls.

Four rows pin that a loop whose start is a callable's result and whose step is a float is refused with the float-step diagnostic, directly and through a name, for both callables. TradingView's verdict for that shape was not measured; the rows say so and only make a later change visible. No product file changes.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ion's result against its recorded verdict

TradingView refuses a loop whose start is the result of a function that holds a persistent `var int s` assigned a quotient (CE10106, the same verdict as for an int start), both for a direct call `for i = measure(5) to 6 by 0.5` and for a result bound to a name. The two sources are now byte-exact fixtures with their recorded verdict, span and digests, and two rows assert that the engine refuses each with the float-step diagnostic at the span's columns.

The four inline rows for a callable result as a loop start keep pinning the engine's refusal for the `var` and plain-local forms; their description now says which shapes TradingView refused (the `var` form directly and bound, the plain-local form directly with a literal, directly with an input and bound) and that the plain-local receipts are not stored as fixtures. No product file changes.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…loat-step loop start

TradingView refused four more loops whose start is the result of a function that holds a quotient-assigned variable: the persistent `var` function called with an input, and the plain-local function called directly with a literal, directly with an input and bound to a name (CE10106 each, one export per source). The four sources are byte-exact fixtures with their recorded verdict, span and digests, and each gets the same row as the two earlier fixtures: the engine must refuse it with the float-step diagnostic at the recorded span's columns.

The description of the inline rows now says that TradingView refused every measured form of the shape, that the fixtures pin the receipts, and that the inline rows pin the engine's refusal of the shapes written inline. No product file changes.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

@graphify-labs graphify-labs Bot left a comment •

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graphify reviewed this change.

No issues found by static checks — no coupling regressions or blocking issues in the code graph. That is not the same as safe to merge: see what was not checked.

Not checked: tests were not run; formal verification proved 0 of 9 changed function(s) (2 sampled, not proven, 7 not verified).

Formal verification. PR-changed functions: 2/9 verified (0 proven, 2 may-equivalent, 0 distinguished) · 7 not verified (7 unsupported).

Not verified on this run: \_visit\_VarDecl (unsupported), analyze (unsupported), \_apply\_callsite\_local\_type\_effects (unsupported), \_\_init\_\_ (unsupported), \_type\_for\_decl (unsupported), \_\_init\_\_ (unsupported), declaration (unsupported).


Graphify review — findings

Fixes int-declared variables that receive a fractional := write by widening them to float storage, even under an explicit int hint. LoopTypeSources runs one shared numeric value query, with its integral-division proofs, over reassignments and loop counters, and the analyzer and codegen use it to set double storage. The step check keeps the hint or initializer's type, so a widened int still refuses a float step with PF-E2079, and call-site return inference keeps the widened family for callable-local var/varip. Duplicate storage names, unknown initializer families and untyped helper parameters stay uncovered, and the unannotated-parameter path in _CounterQuery.infer reaches _hint_spec without a None guard.

Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.

Analysis details — impact, health, verification

Impact & health

Graphify review

Impact — 3856 functions depend on the 712 functions this change touches.

Health — this change adds coupling hotspots:

  • worse: _CounterQuery — 9 callers, 22 callees
  • worse: LoopTypeSources — 11 callers, 11 callees
  • new: _NumericValueQuery — 1 callers, 6 callees
  • new: test_declaration_bound_parameter_check_uses_its_own_hint() — 0 callers, 10 callees

Verification — 3856 functions in the blast radius were not formally verified this run (proofs are advisory here).

Gate & verification

graphify gate

PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.

Advisory (not blocking):

  • verification_scope: 3035 function(s) in the blast radius were not formally verified this run

Cross-repo impact

Cross-repo impact

No cross-repo impact detected among the indexed peer repo(s).

1 peer repo(s) in this group are not yet indexed — cross-repo impact may be incomplete.

Cross-repo linkage is derived (SCIP-moniker matches are sound; name/contract matches are heuristic) and ADVISORY — it never affects this check's conclusion.

Formal verification

Could not verify: Could not verify \_visit\_VarDecl.

The verifier did not have enough to check \_visit\_VarDecl, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify analyze.

The verifier did not have enough to check analyze, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify \_apply\_callsite\_local\_type\_effects.

The verifier did not have enough to check \_apply\_callsite\_local\_type\_effects, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify \_\_init\_\_.

The verifier did not have enough to check \_\_init\_\_, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify \_type\_for\_decl.

The verifier did not have enough to check \_type\_for\_decl, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify \_\_init\_\_.

The verifier did not have enough to check \_\_init\_\_, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify declaration.

The verifier did not have enough to check declaration, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

No difference found (not proven): No behavior difference found in infer (not a proof).

The verifier ran both versions of infer on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: the synth_receiver tier. A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

No difference found (not proven): No behavior difference found in value\_spec (not a proof).

The verifier ran both versions of value\_spec on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: the synth_receiver tier. A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

· 4 grounded finding(s) anchored inline below.

@@ -75,19 +76,37 @@ def _join(specs):


class LoopTypeSources:

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Health regression — LoopTypeSources

fans out to 11 callees (efferent coupling); 11 callers depend on it (afferent coupling).

Grounded coupling-delta finding (deterministic), not an LLM guess.

del candidates[key]


class _CounterQuery:

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Health regression — _CounterQuery

fans out to 22 callees (efferent coupling); 9 callers depend on it (afferent coupling).

Grounded coupling-delta finding (deterministic), not an LLM guess.


class _CounterValueQuery(_CounterQuery):
"""Keep fractional division values unless literal arithmetic proves an int."""
class _NumericValueQuery(_CounterQuery):

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Health regression — _NumericValueQuery

fans out to 6 callees (efferent coupling).

Grounded coupling-delta finding (deterministic), not an LLM guess.

("float p", TypeSpec.primitive("float")),
("p", None),
])
def test_declaration_bound_parameter_check_uses_its_own_hint(parameter, expected):

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Health regression — test_declaration_bound_parameter_check_uses_its_own_hint()

fans out to 10 callees (efferent coupling).

Grounded coupling-delta finding (deterministic), not an LLM guess.

@luisleo526
luisleo526 merged commit d6a3107 into main Nov 3, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant