Skip to content

revert to old macros #2

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 5 commits into
base: abs-gas-algebra
Choose a base branch
from
Open

revert to old macros #2

wants to merge 5 commits into from

Conversation

@zjma
Copy link

@zjma zjma commented Jul 19, 2023

No description provided.

@vgao1996 vgao1996 self-requested a review as a code owner July 19, 2023 19:57
@vgao1996 vgao1996 force-pushed the abs-gas-algebra branch 8 times, most recently from ed07539 to eb7fdac Compare July 21, 2023 22:15
vgao1996 pushed a commit that referenced this pull request Nov 13, 2023
@wrwg
[compiler v2] Resource access control (read-write sets) (aptos-labs#1…
58271fd 
…0480)

* [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 aptos-labs#3

* Addressing reviewer comments aptos-labs#4

* Reviewer comments aptos-labs#5
vgao1996 pushed a commit that referenced this pull request Dec 13, 2023
@nanne007 @zjma
[Features] support bn254_algebra in aptos_stdlib (aptos-labs#11142)
3686979 
* [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]>
vgao1996 pushed a commit that referenced this pull request Feb 14, 2024
@zjma
jwk #2: ensure jwk txns are expected in consensus (aptos-labs#11855)
0503b18 
* 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
vgao1996 pushed a commit that referenced this pull request Feb 28, 2024
@zjma @danielxiangzl
randomness #2: real dkg from randomnet (aptos-labs#12127)
e8b9b28 
* types update from randomnet

* update

* lint

* real dkg and rounding

* rounding

---------

Co-authored-by: danielxiangzl <[email protected]>
vgao1996 pushed a commit that referenced this pull request Mar 14, 2024
@wrwg
[compiler-v2] Making v2 the basis of the prover (step #1) (aptos-labs…
2141444 
…#12462)

* [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
vgao1996 pushed a commit that referenced this pull request Jul 8, 2024
Attempt #2: switch high-perf-docker to runs-on.com runners (aptos-lab…
ad42e03 
…s#13851)
vgao1996 pushed a commit that referenced this pull request Jan 7, 2025
@wrwg
[move-prover][cli] Add benchmark functionality (aptos-labs#15636)
673023c 
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 aptos-labs#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

Reviewers

@vgao1996 vgao1996 Awaiting requested review from vgao1996 vgao1996 is a code owner

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@zjma @vgao1996