Skip to content

native_decide polishing; zkvm invariant fix - #49

Merged
nadimkobeissi merged 1 commit into
mainfrom
native-decide-polishing-zkvm-invariants
Aug 17, 2026
Merged

nadimkobeissi merged 1 commit into
mainfrom
native-decide-polishing-zkvm-invariants

Conversation

@lmalloc

@lmalloc lmalloc commented Aug 17, 2026

Copy link
Copy Markdown
Collaborator

Summary

This small PR polishes native_decide statements and an outdated structural invariant used within zkVMs. More in details, it:

  • Replaces the native_decide tactic within h_earlyStop of FRIConfig with a kernel-clean equivalent;
  • Removes unnecessary native_decide tactics in determining field consistency of DeepAliCfg within Soundcalc/ZkVM/Zisk.lean;
  • Removes the field consistency invariant at zkVM level. Following #37, soundcalc supports an optional override of the zkVM-field at circuit level.

@nadimkobeissi
nadimkobeissi merged commit c302735 into main Aug 17, 2026
1 check passed
@nadimkobeissi
nadimkobeissi deleted the native-decide-polishing-zkvm-invariants branch August 17, 2026 21:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants