[debug] Debug the workflow auth issues #1
Closed
Conversation
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
perryjrandall
force-pushed
the
perry/test-workflow
branch
5 times, most recently
from
7313aac
to
9ac55f0
Compare
perryjrandall
force-pushed
the
perry/test-workflow
branch
from
9ac55f0
to
7633e8e
Compare
aptos-bot
pushed a commit
that referenced
this pull request
Sep 17, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Sep 17, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 8, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 8, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 8, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 8, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 23, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 24, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 30, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 30, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Oct 30, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Oct 30, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
aptos-bot
pushed a commit
that referenced
this pull request
Nov 14, 2024
* jwk types update * update * update * jwk txn and execution * update * fix dummy * update * update * update * update * update * update * remove dummy txns * check voting power than verify signature * fix warnings * update * update QuorumCertifiedUpdate struct GitOrigin-RevId: 793563fc9a022994fbc1d1c073e7090fc8091fe1
aptos-bot
pushed a commit
that referenced
this pull request
Nov 14, 2024
* [compiler-v2] Making v2 the basis of the prover (step #1) This adds the missing parts to let compiler v2 fully support the specification language, and switches the prover to use v2 as the basis for verification of v1 bytecode. There is one further step needed to run the prover also on the code generated by v2 but that one is smaller than here. Notice that with this, we are dogfooding the v2 compiler frontend in production with the Move prover. There is no switching back and forth, code for the v1 prover integration has been removed. In more detail this does the following: - There are two new env processors, the spec_checker and the spec_rewriter: - `spec_checker` checks the correct use of Move functions in the specification language. Those functions must be 'pure' and not depend on state or use certain other constructs. The checker is to be run as part of the regular compiler chain. - `spec_rewriter` rewrites specification expressions by converting used Move functions into specification functions, and doing other transformations to lift a Move expression into the specification language. This is only run by the prover itself. - Inlining has been extended to deal with specification constructs. - To support the inlining refactoring and the new processors, a new module `rewrite_target` is introduced which allows to collect functions and specification elements in a program in a unified fashion, rewriting them, and writing back to the environment. This new data structure has been inspired by the current design of the inliner and naturally extends it. - A lot of ugliness has been ripped out of the model builder infrastructure (e.g. `TryImplAsSpec` mode is gone, as this is now handled by the `spec_rewriter`). More should come in step #2. - Multiple test cases have been added. - The prover driver has been adapted to use the new components. * Fixing some unit tests * Making hopefully all tests pass: - Adding tuple support to the specification language as they are created by the inliner. - Fixing an issue in memory usage calculation - Adding a flag `--aptos` to the prover command line for easier debugging, avoiding the CLI. * Disabling a condition for CI because of timeout. * Rebasing GitOrigin-RevId: 2141444ca406992a2d16de2b50a42ac584c49818
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.