Skip to content

A bunch of stuff#295

Draft
rayman2000 wants to merge 20 commits into
masterfrom
nklose/qol-and-errors
Draft

A bunch of stuff#295
rayman2000 wants to merge 20 commits into
masterfrom
nklose/qol-and-errors

Conversation

@rayman2000

@rayman2000 rayman2000 commented Mar 26, 2026 •
edited by marcoeilers
Loading

Copy link
Copy Markdown
Collaborator
  • Improved the error message for unsupported features
  • Fixed a bug in list_mul: the values in the result were being calculated incorrectly
  • Added support for list.insert: the insert index is complicated, if it is greater than the length, then we append at the end. If it is negative, we go backwards from the end of the list, if negative and greater than the length, we prepend.

This change is Reviewable

@rayman2000

rayman2000 commented Mar 26, 2026

Copy link
Copy Markdown
Collaborator Author
  • Changed the encoding of contains for lists and PSeqs. They now state that an element exists in the collection that object-equals the input.

@rayman2000

rayman2000 commented Mar 30, 2026

Copy link
Copy Markdown
Collaborator Author
  • Added --strict-int mode, which replaces many instances of isinstance(x, int) with type(x) == int in the Viper encoding.

@rayman2000

rayman2000 commented Apr 8, 2026

Copy link
Copy Markdown
Collaborator Author
  • Added support for (some) CLI arguments in server client mode

@rayman2000

rayman2000 commented Apr 8, 2026

Copy link
Copy Markdown
Collaborator Author
  • Added handling for Silicon Timeout Exceptions

rayman2000 and others added 11 commits April 15, 2026 16:06
@rayman2000
Better client error reporting
40db43c
@rayman2000
more try/catch for silicon crashing
9e382af
@rayman2000
added list.copy()
64eb851
@rayman2000
list remove and index
31927b3
@rayman2000
Better strict int for lists
7a2a2c0
@rayman2000
strict int for pseqs
7698653
@rayman2000 @claude
strict-int: Acc ratio annotation, tuple invariants, tuple tests
1ffc399 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@rayman2000
Merge remote-tracking branch 'origin/master' into nklose/qol-and-errors
ea52b04 
# Conflicts:
#	src/nagini_translation/client.py
#	src/nagini_translation/main.py
#	src/nagini_translation/resources/builtins.json
#	tests/functional/verification/test_lists.py
@rayman2000 @claude
service/MCP: expose --strict-int and --force-obligations
b5d1629 
Threads strict_int through both service translate call sites, the
configure tool (strictInt), and the shared service CLI arguments so
nagini_mcp/nagini_lsp can run in strict-int mode. force_obligations
pins the obligation encoding via the existing snapshot mechanism.
Also threads strict_int through the CLI benchmark path.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@rayman2000 @claude
strict-int: move return-type annotation to new error position
df5b4ac 
The implicit 'return type is correct' postcondition error is now
reported on the function definition rather than the return statement.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@rayman2000
Merge branch 'master' into nklose/qol-and-errors
f8897c0
@rayman2000 rayman2000 changed the title Smaller fixes A bunch of stuff Jul 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@rayman2000