-
Notifications
You must be signed in to change notification settings - Fork 12
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
f fixpoint expample progrem / rebale command
- Loading branch information
Showing
3 changed files
with
46 additions
and
4 deletions.
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
|
||
-- Witnesses | ||
-- IMR: [none] | ||
wit_input := witness | ||
|
||
-- All jets have source type 1; but to use the `pair` combinator we want one | ||
-- with source type 2^256. To get this, we compose it with unit. | ||
sha256_init :: 2^256 -> _ | ||
sha256_init := comp unit jet_sha_256_ctx_8_init | ||
|
||
-- Using this, we can write a self-contained "take 32 bytes and compute their | ||
-- sha2 hash" function. | ||
-- IMR: 8e341445... | ||
sha256 :: 2^256 -> 2^256 | ||
sha256 := comp | ||
comp | ||
pair sha256_init iden | ||
jet_sha_256_ctx_8_add_32 | ||
jet_sha_256_ctx_8_finalize | ||
|
||
-- Check eq | ||
assert_fixpoint :: 2^256 -> 1 | ||
assert_fixpoint := comp | ||
comp | ||
pair (comp iden sha256) iden | ||
jet_eq_256 | ||
jet_verify | ||
|
||
-- IMR: [none] | ||
main := comp wit_input assert_fixpoint | ||
|
||
|
This file contains 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
This file contains 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