Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

424 implicitdebug constraints in implementation #440

Merged
merged 25 commits into from
Oct 11, 2024
Merged

424 implicitdebug constraints in implementation #440

merged 25 commits into from
Oct 11, 2024

Conversation

lorenzogentile404
Copy link
Contributor

@lorenzogentile404 lorenzogentile404 self-assigned this Oct 10, 2024
@lorenzogentile404 lorenzogentile404 linked an issue Oct 10, 2024 that may be closed by this pull request
Implicit/debug constraints in implementation #424
Closed
OlivierBBB
OlivierBBB approved these changes Oct 10, 2024
View reviewed changes
Copy link
Collaborator

@OlivierBBB OlivierBBB left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should revert the (debug ... constraints for now.

hub/constraints/instruction-handling/call/standpoint.lisp Outdated
(defconstraint call-instruction---backward-setting-CREATE-instruction ()
(if-not-zero PEEK_AT_SCENARIO
(defconstraint call-instruction---backward-setting-CALL-instruction ()
(debug (if-not-zero PEEK_AT_SCENARIO
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK for the name change

hub/columns/shared.lisp
@@ -29,7 +29,7 @@
( CALLER_CONTEXT_NUMBER :i32 )

;;
( CONTEXT_WILL_REVERT :binary@prove )
( CONTEXT_WILL_REVERT :binary )
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed not required.

hub/constraints/generalities/context.lisp
@@ -33,17 +33,14 @@
stack/HALT_FLAG))

(defconstraint setting-CMC-and-XAHOY ()
(begin (is-binary CMC)
(is-binary XAHOY)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Useless if CMC and XAHOY are binary@prove. Are they ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes.

  ( CONTEXT_MAY_CHANGE                        :binary@prove )
    ( EXCEPTION_AHOY                            :binary@prove )

hub/constraints/instruction-handling/call/finishing_touches/EOA.lisp
@@ -16,7 +16,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint call-instruction---final-context-row-for-unexceptional-unaborted-EOA-CALLs (:guard (* PEEK_AT_SCENARIO (scenario-shorthand---CALL---externally-owned-account)))
(defconstraint call-instruction---final-context-row-for-unexceptional-unaborted-EOA-CALLs (:guard PEEK_AT_SCENARIO)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK

hub/constraints/instruction-handling/call/finishing_touches/SMC.lisp
@@ -16,7 +16,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint call-instruction---final-context-row-for-unexceptional-unaborted-SMC-CALLs (:guard (* PEEK_AT_SCENARIO (scenario-shorthand---CALL---smart-contract)))
(defconstraint call-instruction---final-context-row-for-unexceptional-unaborted-SMC-CALLs (:guard PEEK_AT_SCENARIO)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK

...ts/instruction-handling/call/finishing_touches/setting_up_the_2nd_phase_for_precompiles.lisp
@@ -16,7 +16,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint call-instruction---setting-up-the-second-phase-of-CALLs-to-precompiles (:guard (* PEEK_AT_SCENARIO (scenario-shorthand---CALL---precompile)))
(defconstraint call-instruction---setting-up-the-second-phase-of-CALLs-to-precompiles (:guard PEEK_AT_SCENARIO)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK

hub/constraints/tx_skip/constraints.lisp Outdated
(debug (eq! (shift account/CODE_HASH_HI tx-skip---row-offset---recipient-account) EMPTY_KECCAK_HI))
(debug (eq! (shift account/CODE_HASH_LO tx-skip---row-offset---recipient-account) EMPTY_KECCAK_LO))
(debug (eq! (shift account/CODE_HASH_HI_NEW tx-skip---row-offset---recipient-account) EMPTY_KECCAK_HI))
(debug (eq! (shift account/CODE_HASH_LO_NEW tx-skip---row-offset---recipient-account) EMPTY_KECCAK_LO))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Discard this. I will push the right fix.

@lorenzogentile404
Update constraints.lisp
65efe51 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update ABS_TX_NUM_and_BTC_NUM.lisp
558cc33 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update acc.lisp
a075863 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update add_bin_ext_mod_mul_shf_wcp.lisp
9e06c1a 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update add_bin_ext_mod_mul_shf_wcp.lisp
61fe3fa 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update universal.lisp
ea63727 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update surviving_the_hub.lisp
63238f0 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update common.lisp
02ce640 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update standpoint.lisp
13b002b 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update copy.lisp
94fc33a 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update copy.lisp
2020a2b 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update copy.lisp
be9762c 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update generalities.lisp
678f45c 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update generalities.lisp
066c6e3 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update generalities.lisp
e16f7d4 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update standpoint.lisp
f6a2cee 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update copy.lisp
af1afbb 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update dup.lisp
09d36cf 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
Update return.lisp
af64bb4 
Signed-off-by: Lorenzo Gentile <lorenzogentile404@gmail.com>
@lorenzogentile404
fix: revert debug
3863195
@lorenzogentile404 lorenzogentile404 merged commit 9594649 into master Oct 11, 2024
2 checks passed
@lorenzogentile404 lorenzogentile404 deleted the 424-implicitdebug-constraints-in-implementation branch October 11, 2024 13:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@OlivierBBB OlivierBBB OlivierBBB approved these changes

@letypequividelespoubelles letypequividelespoubelles Awaiting requested review from letypequividelespoubelles

Assignees

@lorenzogentile404 lorenzogentile404

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Implicit/debug constraints in implementation
2 participants
@lorenzogentile404 @OlivierBBB