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.

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

Bump debian from buster-20211011 to buster-20220125 in /docker/init #2

Closed

Conversation

dependabot[bot]
Copy link
Contributor

@dependabot dependabot bot commented on behalf of github Feb 23, 2022

Bumps debian from buster-20211011 to buster-20220125.

Dependabot compatibility score

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.


Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

  • @dependabot rebase will rebase this PR
  • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
  • @dependabot merge will merge this PR after your CI passes on it
  • @dependabot squash and merge will squash and merge this PR after your CI passes on it
  • @dependabot cancel merge will cancel a previously requested merge and block automerging
  • @dependabot reopen will reopen this PR if it is closed
  • @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
  • @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
  • @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
  • @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

Bumps debian from buster-20211011 to buster-20220125.

---
updated-dependencies:
- dependency-name: debian
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <[email protected]>
@dependabot @github
Copy link
Contributor Author

dependabot bot commented on behalf of github Feb 23, 2022

The following labels could not be found: docker, dependencies.

@dependabot dependabot bot temporarily deployed to Docker February 23, 2022 05:54 Inactive
@dependabot dependabot bot temporarily deployed to Sccache February 23, 2022 05:54 Inactive
@dependabot dependabot bot changed the base branch from scripts to main February 23, 2022 17:45
@davidiw davidiw closed this Mar 2, 2022
@dependabot @github
Copy link
Contributor Author

dependabot bot commented on behalf of github Mar 2, 2022

OK, I won't notify you again about this release, but will get in touch when a new version is available. You can also ignore all major, minor, or patch releases for a dependency by adding an ignore condition with the desired update_types to your config file.

If you change your mind, just re-open this PR and I'll resolve any conflicts on it.

@dependabot dependabot bot deleted the dependabot/docker/docker/init/debian-buster-20220125 branch March 2, 2022 00:22
wrwg pushed a commit to wrwg/aptos-core that referenced this pull request Jul 19, 2022
wrwg pushed a commit to wrwg/aptos-core that referenced this pull request Jul 19, 2022
wrwg pushed a commit to wrwg/aptos-core that referenced this pull request Jul 19, 2022
wrwg pushed a commit to wrwg/aptos-core that referenced this pull request Jul 19, 2022
wrwg added a commit that referenced this pull request Jul 19, 2022
clay-aptos pushed a commit that referenced this pull request Oct 5, 2022
UseEffect dependency arrays were updated
ibalajiarun added a commit that referenced this pull request Jul 14, 2023
ibalajiarun added a commit that referenced this pull request Jul 14, 2023
ibalajiarun added a commit that referenced this pull request Jul 14, 2023
ibalajiarun added a commit that referenced this pull request Jul 17, 2023
movekevin added a commit that referenced this pull request Oct 23, 2023
# This is the 1st commit message:

Example EVM bridge

# This is the commit message #2:

Example EVM bridge

# This is the commit message #3:

Update instructions
wrwg added a commit that referenced this pull request Oct 23, 2023
wrwg added a commit that referenced this pull request Oct 29, 2023
wrwg added a commit that referenced this pull request Oct 29, 2023
* [compiler v2] Resource access control (read-write sets)

This is an e2e implementation of resource access control for Move, with most parts in place:

- Replaces the acquires syntax in a downwards-compatible way
- The extended syntax is only available in compiler v2
- One can now specify `acquires`, `reads`, and `writes`
- One can specify the address of a resource in dependency of parameters
- Multiple levels of wildcards are allowed, e.g. `acquires *(object::address_of(param))` specifies that all resources at the given address are read or written.
- Implements parsing->expansion->move model->file format generator
- Extends `file_format::FunctionHandle` to carry the new information, introducing bytecode version v7. v7 became the new experimental version only available in test code for now.
- TODO: dynamic runtime checking of resource access. Static analysis is also on the horizon, but not needed for an MVP of this feature.
- TODO: bytecode verification of access specifiers

An AIP for this new feature will be filed soon.

As an example, here is some extract from the tests:

```move
module 0x42::m {

    struct S has store {}
    struct R has store {}
    struct T has store {}
    struct G<T> has store {}

    fun f1() acquires S {
    }

    fun f2() reads S {
    }

    fun f3() writes S {
    }

    fun f4() acquires S(*) {
    }

    fun f_multiple() acquires R reads R writes T, S reads G<u64> {
    }

    fun f5() acquires 0x42::*::* {
    }

    fun f6() acquires 0x42::m::R {
    }

    fun f7() acquires *(*) {
    }

    fun f8() acquires *(0x42) {
    }

    fun f9(a: address) acquires *(a) {
    }

    fun f10(x: u64) acquires *(make_up_address(x)) {
    }

    fun make_up_address(x: u64): address {
        @0x42
    }
}
```

* Addressing reviewer comments

* Addressing reviewer comments #2

* Addressing reviewer comments #3

* Addressing reviewer comments #4

* Reviewer comments #5
zjma added a commit that referenced this pull request Dec 12, 2023
* [feat][aptos-stdlib] crypto algebra bn254

Signed-off-by: caojiafeng <[email protected]>

* scripts: fix update_algebra_gas_params.py

Signed-off-by: caojiafeng <[email protected]>

* add bn254 to default features to make unit test pass

* fix a bug mentioned in the comments

* add test for bn254

* bn254: add test and doc

* ark_bn254 benches and derived gas parameters (#2)

* [feat][aptos-stdlib] crypto algebra bn254

Signed-off-by: caojiafeng <[email protected]>

* scripts: fix update_algebra_gas_params.py

Signed-off-by: caojiafeng <[email protected]>

* add bn254 to default features to make unit test pass

* fix a bug mentioned in the comments

* initial

* update

* initial gas param

* benches for fq and fq2

* it compiles

* gas script now also specifies quantity types

* update scripts

---------

Signed-off-by: caojiafeng <[email protected]>
Co-authored-by: caojiafeng <[email protected]>

* resolve comments

* doc: `cargo run -p aptos-framework release` to generate doc

* address comments, and regenerate doc

* update doc

* update doc

* lint, fix ut

* lint

* address comments from `alinush`

Signed-off-by: caojiafeng <[email protected]>

* delete bn254_fq2 related code

* address comments on bench

Signed-off-by: caojiafeng <[email protected]>

* lint, also hardcode BN254 Gt generator to save cold start time

* revert debugging stuff

* update gas version

* lint

---------

Signed-off-by: caojiafeng <[email protected]>
Co-authored-by: zhoujunma <[email protected]>
Co-authored-by: zhoujun.ma <[email protected]>
zjma added a commit that referenced this pull request Feb 5, 2024
* jwk types update

* update

* update

* jwk txn and execution

* update

* consensus ensure jwk txns are expected

* update

* fix dummy

* update

* update

* update

* update

* update

* update

* remove dummy txns

* check voting power than verify signature

* fix warnings

* debug

* debug

* debug

* debug

* debug

* debug

* debug

* finish debug

* fmt
zjma added a commit that referenced this pull request Feb 23, 2024
* types update from randomnet

* update

* lint

* real dkg and rounding

* rounding

---------

Co-authored-by: danielxiangzl <[email protected]>
wrwg added a commit that referenced this pull request Mar 11, 2024
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.
wrwg added a commit that referenced this pull request Mar 11, 2024
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.
wrwg added a commit that referenced this pull request Mar 12, 2024
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.
wrwg added a commit that referenced this pull request Mar 13, 2024
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.
wrwg added a commit that referenced this pull request Mar 13, 2024
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.
wrwg added a commit that referenced this pull request Mar 13, 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
wrwg added a commit that referenced this pull request Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
wrwg added a commit that referenced this pull request Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
wrwg added a commit that referenced this pull request Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
wrwg added a commit that referenced this pull request Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
wrwg added a commit that referenced this pull request Dec 19, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
wrwg added a commit that referenced this pull request Dec 20, 2024
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
georgemitenkov pushed a commit that referenced this pull request Jan 6, 2025
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant