From 7e01f693b071bf7cd2587d9cc8a53fa0ed3b9401 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Fri, 6 Nov 2026 21:11:11 -0800 Subject: [PATCH] Extend the per-unit cost rounding allowance to the automated check The extended balance test that follows the generated postings of an automated transaction weighed each candidate's residual against the zero test alone, without the per-unit cost rounding allowance that C++ adds before its balance test (xact.cc:908-929): the exact adjustment of rounding each per-unit cost of a real posting at its price's decimals, which the engine models, in `balancePool` as in this check, as half a unit in the last place of every cost in the commodity written with decimals. A balanced automated rule that adds to both balancing groups of regress/3314_rounding_auto (issues 3314 and 1125, each group carrying 0.50 bread @ $3.99 and 1.50 bread @ $4.99 against $-9.49) left a residual of half a cent that the zero test refuses and that the allowance absorbs, so the merged oracle rejected a journal that C++ (5f9855cef, with PR 3317) accepts with the rows `2.00 bread Budget:Bread` and `2.00 bread Expenses:Bread` and that main's oracle (bbd5478) accepts as well. The pre-merge branch engine rejected it too, so the conflict resolution had kept the branch's gap rather than main's behavior. The check now allows the sum of the per-cost allowances of the matched postings and of those generated so far, beside the zero test, as `balancePool` allows it beside its own tests. Witness: regress/3314_rounding_auto prints the four rows of main's oracle, and the C++ binary prints the two rows its test expects; the whole witness set of the previous commit (35 files) still prints identically to main's oracle. Co-Authored-By: GLM (Z.ai) via pi Pi-Session: 01a163ec-1792677793 --- Ledger/Journal.lean | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index f0199f7..cf60de4 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -4558,6 +4558,22 @@ private def verifyExtended (st : St) (hline : Nat) (posts : List PostSpec) acc.map fun (c', s) => (c', if c' == c then s + q else s) else acc ++ [(c, q)] let virt := (bracket.candidates.head?.map (·.residual)).getD [] + -- the per-unit cost rounding allowance, as `balancePool` states it: + -- C++ adds the exact adjustment of rounding each per-unit cost of a + -- real posting at its price's decimals before the balance test + -- (xact.cc:908-929), which the engine models as half a unit in the + -- last place of every cost in the commodity written with decimals, + -- the matched and the generated postings both (regress/3314 and + -- regress/1125, whose per-group case test/regress/3314_rounding_auto + -- reaches this check) + let costTol := fun (posts : List PostSpec) (c : String) => + posts.foldl (init := (0 : ℚ)) fun acc p => + match p.costVal with + | some cv => + if cv.comm == c && p.costDecs > 0 then + acc + 1 / (2 * ((10 ^ p.costDecs : ℕ) : ℚ)) + else acc + | none => acc -- under `o`, the remainder of the first check that fails, if one does; -- the widening reads the costs of the postings generated so far let failure := fun (o : PoolCandidate) => Id.run do @@ -4569,8 +4585,10 @@ private def verifyExtended (st : St) (hline : Nat) (posts : List PostSpec) if mb.isEmpty then continue ws := ws ++ mb.filterMap (weight o) let r := (merge (o.residual ++ virt ++ ws)).filter fun (_, s) => s != 0 + let tol := fun (c : String) => costTol posts c + costTol gens c unless r.all (fun (c, s) => if c == "" then s == 0 - else roundsToZeroAt (zeroTestPrec st (posts ++ gens) c) s) do + else absQ s ≤ tol c + || roundsToZeroAt (zeroTestPrec st (posts ++ gens) c) s) do return some r return none let failures := (real.candidates ++ real.swapped).map failure