rahxephon89

rahxephon89

Member Since 7 years ago

Facebook,

Experience Points
3
follower
Lessons Completed
7
follow
Lessons Completed
11
stars
Best Reply Awards
26
repos

60 contributions in the last year

Pinned
⚡ DARPA Cyber Grand Challenge Sample Challenges
⚡ The runtime verification QEA tool
⚡ Runtime verification tool for Solidity smart contracts.
⚡ Runtime verification system for Java, using AspectJ for instrumentation.
⚡ RV-Monitor core system code
⚡ Bitcoin Core integration/staging tree
Activity
Jan
15
1 week ago
started
started time in 1 week ago
Jan
14
1 week ago
push

rahxephon89 push rahxephon89/move

rahxephon89
rahxephon89

Fix failing test due to name conflict

Closes: #11

rahxephon89
rahxephon89

print out global memory in the counterexample trace

commit sha: a5edb84372a232957a90aa0f7b637654a6f4c6b1

push time in 1 week ago
pull request

rahxephon89 pull request diem/move

rahxephon89
rahxephon89

print out global memory in the counterexample trace

Motivation

A new feature to print out the content of the related global memory along with the counter example trace when "--trace" is set in the prover. In this PR, we define the global memory as the memory that is accessed in the function where the verification fails.

The output looks like:

    =         Resource name: DiemTimestamp_CurrentTimeMicroseconds 
    =         Values: 
    =           {
    =             Address(173345816): DiemTimestamp.CurrentTimeMicroseconds{
    =               microseconds = 18446744073709551615},
    =             Default: DiemTimestamp.CurrentTimeMicroseconds{
    =               microseconds = 18446744073709551615}}

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

cargo test

push

rahxephon89 push rahxephon89/move

rahxephon89
rahxephon89

[move-prover][tacas] Getting camera ready.

Only addressed spelling errors spotted by reviewers as well as updated the benchmark and linked to Meng's repo with the artifact evaluation which explains the benchmark methodology. There are many interesting questions from the reviewers but we do not have space to address them IMO.

Closes: #12

rahxephon89
rahxephon89

print out global memory in the counterexample trace

commit sha: 02e7a7f8735c92a4cbf3454800c316558c1568bd

push time in 1 week ago
Activity icon
created branch

rahxephon89 in rahxephon89/move create branch print_fun_global_mem

createdAt 1 week ago
Jan
13
1 week ago
Activity icon
issue

rahxephon89 issue diem/move

rahxephon89
rahxephon89

[Move Prover] Verification timeout when checking two proof targets together

The prover cannot verify two proof targets for the function cmp_bcs_bytes in Compare.move.

The two proof targets can be found here. Both of them involve universal quantifiers with operators on vectors. We suspect this issue may relate to quantifier instantiation. More detailed investigation is needed.

started
started time in 1 week ago
Activity icon
issue

rahxephon89 issue diem/move

rahxephon89
rahxephon89

[move-prover] Boogie exited with compilation errors when "--trace" is set

When the prover is run against several Move modules in the DPN with the option “—trace”, output.bpl cannot pass compilation. To reproduce the error, using the following command:

move package -p diem-move/diem-framework/DPN/sources/ prove -t VASP -- —trace

The output:

Error: [internal] boogie exited with compilation errors: output.bpl(8284,62): Error: undeclared identifier: a output.bpl(8290,66): Error: undeclared identifier: a output.bpl(8427,62): Error: undeclared identifier: a output.bpl(8433,66): Error: undeclared identifier: a output.bpl(8450,70): Error: undeclared identifier: parent output.bpl(8457,73): Error: undeclared identifier: parent output.bpl(8463,78): Error: undeclared identifier: parent output.bpl(8592,62): Error: undeclared identifier: a output.bpl(8598,66): Error: undeclared identifier: a output.bpl(8615,70): Error: undeclared identifier: parent output.bpl(8622,73): Error: undeclared identifier: parent output.bpl(8628,78): Error: undeclared identifier: parent output.bpl(8950,63): Error: undeclared identifier: a output.bpl(8956,67): Error: undeclared identifier: a output.bpl(8973,71): Error: undeclared identifier: parent .... 37 name resolution errors detected in output.bpl

The following code in output.bpl triggers the compilation failure:

// assume Identical($t5, exists<VASP::ChildVASP>(a)) at ./sources/VASP.move:252:37+20
assume {:print "$at(46,10573,10593)"} true;
assume ($t5 == $ResourceExists($1_VASP_ChildVASP_$memory, a));

The Move code at ./sources/VASP.move:252:37+20: ensures forall a: address : exists(a) == old(exists(a));

push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

[operator-tool] Add addtional checks to VerifyValidatorState command

Closes: #10106

rahxephon89
rahxephon89

[dependency] upgrading anyhow -> 1.0.52

to overcome:

error[E0554]: #![feature] may not be used on the stable release channel

Closes: #10114

rahxephon89
rahxephon89

WIP layered accounts

[WIP] Updating frameworks

[WIP] Layering prologues/epilogues

[WIP] prologue layering with chain-specific account info

Closes: #10017

rahxephon89
rahxephon89

[move-model] Represent Move attributes in the move-model.

Attributes weren't yet represented in the move-model. This PR adds a representation and extends the model builder to translate them from the expansion AST.

Attributes in the model are needed for playing with EVM code generation, and possibly also Jazz.

Closes: #10109

rahxephon89
rahxephon89

[move][evm] Experiments for EVM Move Programming Model

This PR contains some rough experiments for a possible programming model for EVM in Move. Check the README.md for details.

Closes: #10104

rahxephon89
rahxephon89

[move-prover] print global memory related to a function in diagnostic output

commit sha: 3df73e6e4b36eae6c11ebc4b3d94e6b6ed9abc9f

push time in 1 week ago
Activity icon
fork

rahxephon89 forked diem/move

⚡ Move documentation
rahxephon89 Apache License 2.0 Updated
fork time in 1 week ago
Jan
12
1 week ago
Activity icon
issue

rahxephon89 issue diem/diem

rahxephon89
rahxephon89

[move-prover] Boogie exited with compilation errors when "--trace" is set

When the prover is run against several Move modules in the DPN with the option “—trace”, output.bpl cannot pass compilation. To reproduce the error, using the following command:

move package -p diem-move/diem-framework/DPN/sources/ prove -t VASP -- —trace

The output:

Error: [internal] boogie exited with compilation errors: output.bpl(8284,62): Error: undeclared identifier: a output.bpl(8290,66): Error: undeclared identifier: a output.bpl(8427,62): Error: undeclared identifier: a output.bpl(8433,66): Error: undeclared identifier: a output.bpl(8450,70): Error: undeclared identifier: parent output.bpl(8457,73): Error: undeclared identifier: parent output.bpl(8463,78): Error: undeclared identifier: parent output.bpl(8592,62): Error: undeclared identifier: a output.bpl(8598,66): Error: undeclared identifier: a output.bpl(8615,70): Error: undeclared identifier: parent output.bpl(8622,73): Error: undeclared identifier: parent output.bpl(8628,78): Error: undeclared identifier: parent output.bpl(8950,63): Error: undeclared identifier: a output.bpl(8956,67): Error: undeclared identifier: a output.bpl(8973,71): Error: undeclared identifier: parent .... 37 name resolution errors detected in output.bpl

The following code in output.bpl triggers the compilation failure:

// assume Identical($t5, exists<VASP::ChildVASP>(a)) at ./sources/VASP.move:252:37+20
assume {:print "$at(46,10573,10593)"} true;
assume ($t5 == $ResourceExists($1_VASP_ChildVASP_$memory, a));

The Move code at ./sources/VASP.move:252:37+20: ensures forall a: address : exists(a) == old(exists(a));

Jan
7
2 weeks ago
started
started time in 2 weeks ago
Jan
5
2 weeks ago
pull request

rahxephon89 merge to diem/diem

rahxephon89
rahxephon89

[move-model] Represent Move attributes in the move-model.

Attributes weren't yet represented in the move-model. This PR adds a representation and extends the model builder to translate them from the expansion AST.

Motivation

Attributes in the model are needed for playing with EVM code generation, and possibly also Jazz.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

NA

Related PRs

NA

pull request

rahxephon89 merge to diem/diem

rahxephon89
rahxephon89

[move-model] Represent Move attributes in the move-model.

Attributes weren't yet represented in the move-model. This PR adds a representation and extends the model builder to translate them from the expansion AST.

Motivation

Attributes in the model are needed for playing with EVM code generation, and possibly also Jazz.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

NA

Related PRs

NA

Dec
30
3 weeks ago
Activity icon
created branch

rahxephon89 in rahxephon89/diem create branch print_fun_global_mem

createdAt 3 weeks ago
Dec
17
1 month ago
pull request

rahxephon89 merge to diem/diem

rahxephon89
rahxephon89

[move-tutorial] Fix "Coin" to be "BasicCoin" in step 1 of tutorial

This updates the name of the module in step 1 to match the code in the tutorial text.

This closes #9982

Dec
16
1 month ago
Activity icon
issue

rahxephon89 issue comment diem/diem

rahxephon89
rahxephon89

[move-prover] MultiToken Specification

Motivation

Request for feedback and suggestions for specifying MultiToken.move and MultiTokenBalance.move.

Issues: some aborts_if conditions in transfer_multi_token_between_galleries, add_to_gallery and create are yet to be defined.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

cargo run -- -T 3000 ../../diem-move/diem-framework/experimental/sources/MultiToken.move ../../diem-move/diem-framework/experimental/sources/MultiTokenBalance.move

Dec
15
1 month ago
push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

[move-prover] Specification of multitoken

commit sha: 5a73de9ee6746820db1d1e3bfe29a7f791e45a85

push time in 1 month ago
pull request

rahxephon89 pull request diem/diem

rahxephon89
rahxephon89

[move-prover]Fix the link to the document of Move Specification Language

Motivation

fix the link to the document of Move Specification Language

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

click the link

push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

[move-prover] Specification of multitoken

commit sha: 88c4a9739d72d2fc3878d6c068e23d44611a6d7b

push time in 1 month ago
push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

Revert the Z3 version

This PR reverts the Z3 version. The new version causes a build error.

Closes: #9893

rahxephon89
rahxephon89

Added the experimental stdlib modules Role and ACL

  • the Role module is a generic module for role-based access control (RBAC).

  • the ACL module is a module that defines the access control list (ACL)

Closes: #9603

rahxephon89
rahxephon89

[move-cli] Update Move CLI to use packages

Closes: #9871

rahxephon89
rahxephon89

[api] get core account resource

Closes: #9885

rahxephon89
rahxephon89

[move] Provide code completion via language server

Implement a completion provider in the move-analyzer language server, so users of the Visual Studio Code extension see code completion suggestions as they type.

This first iteration of completion in the language server is as simple as possible, and performs no semantic analysis. However, it must still lex the source program. That is because, as soon as move-analyzer informs VS Code that it provides completions, VS Code stops its internal completion engine entirely. Originally, the intent of this change to move-analyzer was to supplement VS Code's completion items (for example, if you typed foo anywhere in the source file, VS Code would surface foo as a completion item everywhere else) with Move's keywords and built-in operators. Since there is no easy way to add to VS Code's simple textual completion engine, this commit implements such an engine on its own, and adds to that the Move keywords and operators.

Doing so resulted in several decisions and future work items:

  • Users spend most of their time editing source code that is not saved to disk. They only save that code to disk at certain times, such as when they feel it is worth saving. To provide completions, move-analyzer cannot just rely on what's on disk, and so must receive notifications from the language server client as to what source buffers the user is editing. (This could be improved by processing incremental updates from the client.)
  • Language servers can define "trigger characters" that prompt the client to present completions. For Move and many other languages, . and :: make sense for these (for example, foo. and foo::). Move keywords (if, fun, etc.) and operators (move and copy) can't appear in these positions, so they are filtered out when the user's cursor appears in these positions. (This could be improved by performing semantic analysis and filtering completion items based on whether the cursor is within a address, module, or fun block, based on what identifiers are in scope, etc.)
  • Currently, the source file being edited is lexed whenever completions are requested for that file. Instead, move-analyzer could maintain an ever-ready syntax tree view of the entire package being edited, that is updated as files are modified. When completions are suggested, they ought to be readily available based on this tree, instead of being computed reactively as requested.
  • I noticed that certain contextual keywords were not included in the regex-based TextMate grammar for Move, so I added them. (Once the language server begins relying on parsed, semantic analyzed views of Move programs, it can begin providing semantically-aware syntax highlighting that ensures these are not colored as keywords unless appropriate.)

Closes: #9589

rahxephon89
rahxephon89

[diem-wallet] cleanup dependencies and interface

Closes: #9808

rahxephon89
rahxephon89

[mempool] Remove PeerId from metrics

PeerId in metrics doesn't add significant value, and causes a large increase in the number of tracked values. This gets rid of them in the metrics.

Closes: #9832

rahxephon89
rahxephon89

[hackathon] add tutorial for Move workshop

Closes: #9894

rahxephon89
rahxephon89

[shuffle] extract out deno diem client from devapi

Closes: #9895

rahxephon89
rahxephon89

[shuffle] clean up latest/test methods

Closes: #9899

rahxephon89
rahxephon89

[forge][k8s] custom genesis modules on Resize

rahxephon89
rahxephon89

[forge] different ways to provide genesis modules

Closes: #9851

rahxephon89
rahxephon89

[shuffle] annotate API call arguments and return types

rahxephon89
rahxephon89

[shuffle] switch to call get account for account core resource instead of looking up DiemAccount resource

rahxephon89
rahxephon89

[shuffle] rename some devapi function to be more consistent with API names

Closes: #9900

rahxephon89
rahxephon89

[diem-rest-client] update get_account to call get_account API

Closes: #9901

rahxephon89
rahxephon89
rahxephon89
rahxephon89

[shuffle] Update to refactored receiver

rahxephon89
rahxephon89

[shuffle] Add hello nft tutorial

commit sha: fd50a49a785db9dfb1fbaa9773377f3b05843c1b

push time in 1 month ago
Activity icon
issue

rahxephon89 issue comment diem/diem

rahxephon89
rahxephon89

[move-prover] MultiToken Specification

Motivation

Request for feedback and suggestions for specifying MultiToken.move and MultiTokenBalance.move.

Issues: some aborts_if conditions in transfer_multi_token_between_galleries, add_to_gallery and create are yet to be defined.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

cargo run -- -T 3000 ../../diem-move/diem-framework/experimental/sources/MultiToken.move ../../diem-move/diem-framework/experimental/sources/MultiTokenBalance.move

Activity icon
issue

rahxephon89 issue comment diem/diem

rahxephon89
rahxephon89

[move-prover] Fix bug for choice operator on type instantiation

Motivation

Resolve https://github.com/diem/diem/issues/9862

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

Add a test case in choice.move

Dec
14
1 month ago
push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

fix bug for choice operator on type instantiation

commit sha: 1bd04195a1ab8d3256640c9e5e06f8845e4ef490

push time in 1 month ago
push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

fix bug for choice operator on type instantiation

commit sha: df5aad9a92c1df78df5785095eb4e04ff5fc79a9

push time in 1 month ago
push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

[language] move diem-transactional-test-harness, e2e-tests, e2e-testsuite into diem-move

Closes: #9998

rahxephon89
rahxephon89

[move-prover] Fixing error with auto trace wrongly applied

This ignores autogenerated TRACE expressions which are on untraceable items instead of generating an error, as happens with a user provided explicit TRACE.

Closes: #10036

rahxephon89
rahxephon89

[forge] Add buffer time for node sync up

Closes: #10038

rahxephon89
rahxephon89

[language] minor fixes to allow Move crates to compile outside the Diem repo - 1

Closes: #10031

rahxephon89
rahxephon89

fix bug for choice operator on type instantiation

commit sha: 4dc62fb4f1f7fd2ba215d192db33b48562545262

push time in 1 month ago
pull request

rahxephon89 merge to diem/diem

rahxephon89
rahxephon89

[move-prover] Fixing error with auto trace wrongly applied

This ignores autogenerated TRACE expressions which are on untraceable items instead of generating an error, as happens with a user provided explicit TRACE.

Motivation

Bug fix

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

New test

Related PRs

NA

push

rahxephon89 push rahxephon89/diem

rahxephon89
rahxephon89

Added examples/experimental/math-puzzle

This PR adds the examples folder in language/documentation.

math-puzzle is added to the examples/experimental directory.

TODO:

  • make examples a cargo project
  • add the document generation and the test features to the examples project

Closes: #10023

rahxephon89
rahxephon89

[tf][aws] add aws terraform for validator

Closes: #10019

rahxephon89
rahxephon89

[data-client] Add structured logging to data client

Closes: #9994

rahxephon89
rahxephon89

[api] switch tests to use rest client from jsonrpc client: transaction-emitter

Closes: #10026

rahxephon89
rahxephon89

[tf][vault-init] add terraform for vault initialization

Closes: #10028

rahxephon89
rahxephon89

[data-client] change data client config type to u64

Closes: #10029

rahxephon89
rahxephon89

[tf][azure] add terraform files for validator deployment in Azure

Closes: #10033

rahxephon89
rahxephon89

fix bug for choice operator on type instantiation

commit sha: a40bf9261941581feede88e67e33895e46fe8054

push time in 1 month ago
open pull request

rahxephon89 wants to merge diem/diem

rahxephon89
rahxephon89

[move-prover] Fix bug for choice operator on type instantiation

Motivation

Resolve https://github.com/diem/diem/issues/9862

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

Add a test case in choice.move

rahxephon89
rahxephon89

I have tried using NodeId but it does not work for the example in Meng's PR

pull request

rahxephon89 merge to diem/diem

rahxephon89
rahxephon89

[move-prover] Fix bug for choice operator on type instantiation

Motivation

Resolve https://github.com/diem/diem/issues/9862

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

Add a test case in choice.move

Previous