Repository navigation
Keep the fraction in a variable that starts as an int and is later assigned a quotient, including one that a function returns - #318
Conversation
…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>
There was a problem hiding this comment.
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: | |||
There was a problem hiding this comment.
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: |
There was a problem hiding this comment.
_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): |
There was a problem hiding this comment.
_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): |
There was a problem hiding this comment.
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.
What changes
A variable that starts from an int and is later assigned a quotient (
s = nthens := s / 2) was declaredintin the generated C++, and the quotient was cut to an int when it was written. Every later read, a loop start or a plainqty = s, saw only the integer part. TradingView keeps the fraction, whatever the variable's declaration: inferred, an explicitint, 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 = strades 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 forms = n; s := s / 2; for i = s to s + 2trades 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 theintkeyword. 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 withvar int s) returned 2 forseed = 5where TradingView returns 2.5 (205 entries each). The function's return type was inferred from the writtenint, so the value was cut at the return; the return inference now reads the same widening annotation. Both thevarand 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
for i = measure(5) to 6 by 0.5,x = measure(n)thenfor 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.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.codegen/types.py,_slot_scalar_cpp_type); the guard is inloop_types.py.s /= 2), methods and for-in binders keep their present behaviour. A directint x = a / binitializer was not measured on TradingView and is unchanged.s = n; s := s / 2; for i = s to 6 by 0.5, also withint 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
84120311: 19,347 passed, 235 skipped, 0 failed; compile corpus 312 passed; the parity gate step passes. The same run against the previous engine main8d0f9e75gave the same counts (history): 19,347 passed, 235 skipped, 0 failed; compile corpus 312 passed; the parity gate step passes.8d0f9e75, not re-run on84120311; this head measured on both): the function-returned quantity sources (varand 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 engine8d0f9e75) is unequal on this head (measured on8d0f9e75and on84120311).84120311(the current engine main: the sweep was repeated after the engine's last merge), against the active baseline (engine84120311with codegendaa51025, 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 main8d0f9e75and the previous baseline gave the same verdict; it is history and not the pairing used here.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