[claude-experiments] Add rem/Long support and fromEpochDays verification test#97
Open
[claude-experiments] Add rem/Long support and fromEpochDays verification test#97
Conversation
- Register Int.rem() as a special Kotlin function (was defined but not wired up) - Add Long arithmetic operators (plus, minus, times, div, rem, inc, dec, unaryMinus) mapped to the same Viper Int type, plus Int<->Long identity conversions - Add Long literal support in StmtConversionVisitor and Long type mapping in ProgramConverter - Port kotlinx-datetime's fromEpochDays/toEpochDays as an expensive verification test with intermediate verify() assertions to guide the SMT solver through nonlinear arithmetic Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Verify properties from the source comments: adjustCycles <= -1, adjust <= 0, zeroDay >= 0, doyEst >= 0, marchMonth0 in 0..11, month in 1..12, dom in 1..31, yearEst >= 0. These compose into a strong postcondition: res in 101..99991231. The remaining gap is doyEst <= 365 (day-of-year upper bound), which requires reasoning about the year-estimation division — too much nonlinear arithmetic for the solver. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
jesyspa
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Int.rem()as a special Kotlin function — it was defined asRemIntIntbut never wired up inSpecialKotlinFunctions.byName, so%in verified code compiled to an opaque method call instead of Viper'sMod.Longtype support: arithmetic operators, literals, type mapping, andInt↔Longconversions. Both map to Viper's unboundedInt.fromEpochDays/toEpochDaysas an expensive verification test with intermediateverify()assertions that guide the SMT solver through nonlinear arithmetic involving large constants (146097, 153, 306).Details
The
fromEpochDaystest demonstrates both the power and limits of automated verification on real-world date arithmetic. The intermediate assertions (zeroDay >= 0after cycle adjustment,doyEst >= 0after year estimation) break the proof into pieces the solver can handle. Stronger postconditions (e.g.month in 1..12) remain out of reach because they require nonlinear modular arithmetic across packed integer representations.Test plan
testFrom_epoch_dayspasses (golden file generated and verified)testArithmeticpasses (no regressions from rem/Long changes)testFull_viper_dumppasses🤖 Generated with Claude Code