Skip to content

Add one-time pad example with map, linked list, and sequence based implentations#1160

Merged
shigoel merged 3 commits into
strata-org:main2from
Dragon-Hatcher:otp-sequence-fix
May 19, 2026
Merged

Add one-time pad example with map, linked list, and sequence based implentations#1160
shigoel merged 3 commits into
strata-org:main2from
Dragon-Hatcher:otp-sequence-fix

Conversation

@Dragon-Hatcher
Copy link
Copy Markdown

Add a one-time pad example using three different methods for the array data structure: a map of ints, a linked list, and the new sequence type. The map version is verified with gen_smt_vcs and the two others with #eval verify.

…tations

Demonstrates Encrypt, Decrypt, and RoundTrip procedures verified across three data structure backends in the Boole and Core languages.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@Dragon-Hatcher Dragon-Hatcher requested a review from a team as a code owner May 13, 2026 16:56
Comment thread StrataTest/Languages/Boole/otp.lean
@joscoh joscoh added the CSLib PRs and issues marked with this label indicate contributions from/for the CSLib community. label May 14, 2026
@shigoel shigoel added this pull request to the merge queue May 19, 2026
@aqjune-aws
Copy link
Copy Markdown
Contributor

Umm, I was about to create a draft PR that includes the updates in this PR to check whether internal benchmark check passes, but this PR is in a merge queue and for some reason it can't be removed. I will create a separate draft PR one and check in parallel.

Merged via the queue into strata-org:main2 with commit 83e3e54 May 19, 2026
24 of 25 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CSLib PRs and issues marked with this label indicate contributions from/for the CSLib community. Waiting-For-Review

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants