Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

feat: introduce named-addresses #255

Merged
merged 2 commits into from
Aug 23, 2024
Merged

feat: introduce named-addresses #255

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
89e9eac
bump movevm to latest
beer-1 Aug 23, 2024
e105fa7
fix to check it at empty flag
beer-1 Aug 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ ARG TARGETARCH
ARG GOARCH

# See https://github.com/initia-labs/movevm/releases
ENV LIBMOVEVM_VERSION=v0.4.2
ENV LIBMOVEVM_VERSION=v0.4.3

# Install necessary packages
RUN set -eux; apk add --no-cache ca-certificates build-base git cmake
Expand Down
203 changes: 51 additions & 152 deletions cmd/move/move.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,9 @@ import (
movetypes "github.com/initia-labs/initia/x/move/types"

"github.com/initia-labs/movevm/api"
"github.com/initia-labs/movevm/types/compiler"
"github.com/initia-labs/movevm/types"
buildtypes "github.com/initia-labs/movevm/types/compiler/build"
coveragetypes "github.com/initia-labs/movevm/types/compiler/coverage"
docgentypes "github.com/initia-labs/movevm/types/compiler/docgen"
provetypes "github.com/initia-labs/movevm/types/compiler/prove"
testtypes "github.com/initia-labs/movevm/types/compiler/test"
"github.com/pelletier/go-toml"
"github.com/spf13/cobra"
Expand Down Expand Up @@ -51,6 +49,7 @@ const (
flagBytecodeVersion = "bytecode-version"
flagCompilerVersion = "compiler-version"
flagLanguageVersion = "language-version"
flagNamedAddresses = "named-addresses"
/* test options */
flagGasLimit = "gas-limit"
flagGasLimitShorthand = "g"
Expand All @@ -66,20 +65,6 @@ const (
flagComputeCoverage = "coverage"
// clean options
flagCleanCache = "clean-cache"
// prove options
flagProcCores = "proc-cores"
flagTrace = "trace"
flagTraceShorthand = "t"
flagCVC5 = "cvc5"
flagStratificationDepth = "stratification-depth"
flagRandomSeed = "random-seed"
flagVcTimeout = "vc-timeout"
flagCheckInconsistency = "check-inconsistency"
flagKeepLoops = "keep-loops"
flagLoopUnroll = "loop-unroll"
flagStableTestOutput = "stable-test-output"
flagDump = "dump"
flagVerbosity = "verbosity"
// verify options
flagVerify = "verify"
// coverage options
Expand Down Expand Up @@ -116,7 +101,6 @@ func MoveCommand(ac address.Codec) *cobra.Command {
moveNewCmd(),
moveCleanCmd(),
moveDeployCmd(ac),
moveProveCmd(),
moveVerifyCmd(),
moveDocgenCmd(),
)
Expand Down Expand Up @@ -178,7 +162,7 @@ func moveTestCmd() *cobra.Command {
if err != nil {
return err
}
tc, err := getTestConfig(cmd)
tc, err := getTestOptions(cmd)
if err != nil {
return err
}
Expand Down Expand Up @@ -249,7 +233,7 @@ func moveCoverageSummaryCmd() *cobra.Command {
return err
}

config, err := getCoverageSummaryConfig(cmd)
config, err := getCoverageSummaryOptions(cmd)
if err != nil {
return err
}
Expand Down Expand Up @@ -280,8 +264,8 @@ func moveCoverageSourceCmd() *cobra.Command {
return err
}

_, err = api.CoverageSource(*arg, coveragetypes.CoverageSourceConfig{
ModuleName: args[0],
_, err = api.CoverageSource(*arg, types.CompilerCoverageSourceOptions{
ModuleName: &args[0],
})
if err != nil {
return err
Expand All @@ -307,8 +291,8 @@ func moveCoverageBytecodeCmd() *cobra.Command {
return err
}

_, err = api.CoverageBytecode(*arg, coveragetypes.CoverageBytecodeConfig{
ModuleName: args[0],
_, err = api.CoverageBytecode(*arg, types.CompilerCoverageBytecodeOptions{
ModuleName: &args[0],
})
if err != nil {
return err
Expand Down Expand Up @@ -355,7 +339,7 @@ func moveCleanCmd() *cobra.Command {
Long: "Remove previously built data and its cache",
Args: cobra.ExactArgs(0),
RunE: func(cmd *cobra.Command, args []string) error {
arg := compiler.CompilerArgument{}
arg := types.CompilerArguments{}

cleanCache, err := cmd.Flags().GetBool(flagCleanCache)
if err != nil {
Expand Down Expand Up @@ -509,38 +493,6 @@ func moveDeployCmd(ac address.Codec) *cobra.Command {
return cmd
}

func moveProveCmd() *cobra.Command {
cmd := &cobra.Command{
Use: "prove [flags]",
Short: "prove a move package",
Long: "run formal verification of a Move package using the Move prover",
Args: cobra.ExactArgs(0),
RunE: func(cmd *cobra.Command, args []string) error {
arg, err := getCompilerArgument(cmd)
if err != nil {
return err
}

pc, err := getProveConfig(cmd)
if err != nil {
return err
}

_, err = api.ProveContract(*arg, *pc)
if err != nil {
return err
}

fmt.Println("Prove success")
return nil
},
}

addMoveBuildFlags(cmd)
addMoveProveFlags(cmd)
return cmd
}

func moveVerifyCmd() *cobra.Command {
cmd := &cobra.Command{
Use: "verify [flags]",
Expand Down Expand Up @@ -578,7 +530,7 @@ func moveDocgenCmd() *cobra.Command {
if err != nil {
return err
}
dgc, err := getDocgenConfig(cmd)
dgc, err := getDocgenOptions(cmd)
if err != nil {
return err
}
Expand Down Expand Up @@ -617,6 +569,7 @@ the 'tests' directory`)
cmd.Flags().Uint32(flagBytecodeVersion, 0, "Specify the version of the bytecode the compiler is going to emit")
cmd.Flags().Uint32(flagCompilerVersion, 1, "Specify the version of the compiler to use")
cmd.Flags().Uint32(flagLanguageVersion, 1, "Specify the version of the language to use")
cmd.Flags().String(flagNamedAddresses, "", "Named addresses to use in compilation. ex: --named-addresses 'name_1=0x1,name_2=0x2'")
}

func addMoveTestFlags(cmd *cobra.Command) {
Expand All @@ -642,21 +595,6 @@ func addMoveDeployFlags(cmd *cobra.Command) {
cmd.Flags().Bool(flagVerify, false, "Verify the contract compared to the onchain package")
}

func addMoveProveFlags(cmd *cobra.Command) {
cmd.Flags().Uint(flagProcCores, provetypes.DefaultProcCores, "The number of cores to use for parallel processing of verification conditions")
cmd.Flags().BoolP(flagTrace, flagTraceShorthand, false, "Whether to display additional information in error reports. This may help debugging but also can make verification slower")
cmd.Flags().Bool(flagCVC5, false, "Whether to use cvc5 as the smt solver backend. The environment variable `CVC5_EXE` should point to the binary")
cmd.Flags().Uint(flagStratificationDepth, provetypes.DefaultStratificationDepth, "The depth until which stratified functions are expanded")
cmd.Flags().Uint(flagRandomSeed, 0, "A seed to the prover")
cmd.Flags().Uint(flagVcTimeout, provetypes.DefaultVcTimeout, "A (soft) timeout for the solver, per verification condition, in seconds")
cmd.Flags().Bool(flagCheckInconsistency, false, "Whether to check consistency of specs by injecting impossible assertions")
cmd.Flags().Bool(flagKeepLoops, false, "Whether to keep loops as they are and pass them on to the underlying solver")
cmd.Flags().Uint(flagLoopUnroll, 0, "Number of iterations to unroll loops")
cmd.Flags().Bool(flagStableTestOutput, false, "Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test output")
cmd.Flags().Bool(flagDump, false, "Whether to dump intermediate step results to files")
cmd.Flags().StringP(flagVerbosity, flagVerboseShorthand, "", "Verbosity level")
}

func addMoveDocgenFlags(cmd *cobra.Command) {
cmd.Flags().Bool(flagIncludeImpl, false, "Whether to include private declarations and implementations into the generated documentation.")
cmd.Flags().Bool(flagIncludeSpecs, false, "Whether to include specifications in the generated documentation.")
Expand All @@ -667,7 +605,7 @@ func addMoveDocgenFlags(cmd *cobra.Command) {
cmd.Flags().String(flagReferencesFile, "", "Package-relative path to a file whose content is added to each generated markdown file.")
}

func getCompilerArgument(cmd *cobra.Command) (*compiler.CompilerArgument, error) {
func getCompilerArgument(cmd *cobra.Command) (*types.CompilerArguments, error) {
bc, err := getBuildConfig(cmd)
if err != nil {
return nil, err
Expand All @@ -683,18 +621,18 @@ func getCompilerArgument(cmd *cobra.Command) (*compiler.CompilerArgument, error)
return nil, err
}

return &compiler.CompilerArgument{
PackagePath: packagePath,
return &types.CompilerArguments{
PackagePath: &packagePath,
Verbose: verbose,
BuildConfig: *bc,
}, nil
}

func getBuildConfig(cmd *cobra.Command) (*buildtypes.BuildConfig, error) {
func getBuildConfig(cmd *cobra.Command) (*types.CompilerBuildConfig, error) {

options := []func(*buildtypes.BuildConfig){}
options := []func(*types.CompilerBuildConfig){}

boolFlags := map[string]func(*buildtypes.BuildConfig){}
boolFlags := map[string]func(*types.CompilerBuildConfig){}
boolFlags[flagDevMode] = buildtypes.WithDevMode()
boolFlags[flagTestMode] = buildtypes.WithTestMode()
boolFlags[flagGenerateDocs] = buildtypes.WithGenerateDocs()
Expand Down Expand Up @@ -736,15 +674,38 @@ func getBuildConfig(cmd *cobra.Command) (*buildtypes.BuildConfig, error) {
}
options = append(options, buildtypes.WithLanguageVersion(languageVersion))

namedAddresses, err := cmd.Flags().GetString(flagNamedAddresses)
if err != nil {
return nil, err
}
if len(namedAddresses) > 0 {
namedAddressMap := make(map[string]types.AccountAddress)
for _, namedAddress := range strings.Split(namedAddresses, ",") {
v := strings.Split(namedAddress, "=")
if len(v) != 2 {
return nil, fmt.Errorf("invalid named-addresses: %s", namedAddresses)
}

name := v[0]
addr, err := types.NewAccountAddress(v[1]) // validate address
if err != nil {
return nil, fmt.Errorf("invalid address: %s", v[1])
}

namedAddressMap[name] = addr
}
options = append(options, buildtypes.WithNamedAddresses(namedAddressMap))
}

bc := buildtypes.NewBuildConfig(options...)

return &bc, nil
}

func getTestConfig(cmd *cobra.Command) (*testtypes.TestConfig, error) {
options := []func(*testtypes.TestConfig){}
func getTestOptions(cmd *cobra.Command) (*types.CompilerTestOptions, error) {
options := []func(*types.CompilerTestOptions){}

boolFlags := map[string]func(*testtypes.TestConfig){}
boolFlags := map[string]func(*types.CompilerTestOptions){}
boolFlags[flagComputeCoverage] = testtypes.WithComputeCoverage()
boolFlags[flagReportStatistics] = testtypes.WithReportStatistics()
boolFlags[flagReportStorageOnError] = testtypes.WithReportStorageOnError()
Expand All @@ -768,11 +729,11 @@ func getTestConfig(cmd *cobra.Command) (*testtypes.TestConfig, error) {
options = append(options, testtypes.WithFilter(filter))
}

tc := testtypes.NewTestConfig(options...)
tc := testtypes.NewTestOptions(options...)
return &tc, nil
}

func getCoverageSummaryConfig(cmd *cobra.Command) (*coveragetypes.CoverageSummaryConfig, error) {
func getCoverageSummaryOptions(cmd *cobra.Command) (*types.CompilerCoverageSummaryOptions, error) {
functions, err := cmd.Flags().GetBool(flagFunctions)
if err != nil {
return nil, err
Expand All @@ -781,78 +742,16 @@ func getCoverageSummaryConfig(cmd *cobra.Command) (*coveragetypes.CoverageSummar
if err != nil {
return nil, err
}
return &coveragetypes.CoverageSummaryConfig{
return &types.CompilerCoverageSummaryOptions{
Functions: functions,
OutputCSV: outputCSV,
OutputCsv: outputCSV,
}, nil
}

func getProveConfig(cmd *cobra.Command) (*provetypes.ProveConfig, error) {
options := []func(*provetypes.ProveConfig){}

boolFlags := map[string]func(*provetypes.ProveConfig){}
boolFlags[flagTrace] = provetypes.WithTrace()
boolFlags[flagCVC5] = provetypes.WithCVC5()
boolFlags[flagCheckInconsistency] = provetypes.WithCVC5()
boolFlags[flagKeepLoops] = provetypes.WithKeepLoops()
boolFlags[flagStableTestOutput] = provetypes.WithStableTestOutput()
boolFlags[flagDump] = provetypes.WithDump()

for fn, opt := range boolFlags {
flag, err := cmd.Flags().GetBool(fn)
if err != nil {
return nil, err
}
if flag {
options = append(options, opt)
}
}

procCores, err := cmd.Flags().GetUint(flagProcCores)
if err != nil {
return nil, err
}
options = append(options, provetypes.WithProcCores(procCores))

stratificationDepth, err := cmd.Flags().GetUint(flagStratificationDepth)
if err != nil {
return nil, err
}
options = append(options, provetypes.WithStratificationDepth(stratificationDepth))

randomSeed, err := cmd.Flags().GetUint(flagRandomSeed)
if err != nil {
return nil, err
}
options = append(options, provetypes.WithRandomSeed(randomSeed))

vcTimeout, err := cmd.Flags().GetUint(flagVcTimeout)
if err != nil {
return nil, err
}
options = append(options, provetypes.WithVcTimeout(vcTimeout))

loopUnroll, err := cmd.Flags().GetUint(flagLoopUnroll)
if err != nil {
return nil, err
}
options = append(options, provetypes.WithLoopUnroll(loopUnroll))

verbosity, err := cmd.Flags().GetString(flagVerbosity)
if err != nil {
return nil, err

}
options = append(options, provetypes.WithVerbosity(verbosity))

pc := provetypes.NewProveConfig(options...)
return &pc, nil
}

func getDocgenConfig(cmd *cobra.Command) (*docgentypes.DocgenConfig, error) {
options := []func(*docgentypes.DocgenConfig){}
func getDocgenOptions(cmd *cobra.Command) (*types.CompilerDocgenOptions, error) {
options := []func(*types.CompilerDocgenOptions){}

boolFlags := map[string]func(*docgentypes.DocgenConfig){}
boolFlags := map[string]func(*types.CompilerDocgenOptions){}
boolFlags[flagIncludeImpl] = docgentypes.WithIncludeImpl()
boolFlags[flagIncludeSpecs] = docgentypes.WithIncludeSpecs()
boolFlags[flagSpecsInlined] = docgentypes.WithSpecsInlined()
Expand Down Expand Up @@ -881,6 +780,6 @@ func getDocgenConfig(cmd *cobra.Command) (*docgentypes.DocgenConfig, error) {
options = append(options, docgentypes.WithReferencesFile(referencesFile))
}

dgc := docgentypes.NewDocgenConfig(options...)
dgc := docgentypes.NewDocgenOptions(options...)
return &dgc, nil
}
2 changes: 1 addition & 1 deletion go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ require (
github.com/hashicorp/go-metrics v0.5.3
github.com/initia-labs/OPinit v0.4.2
// we also need to update `LIBMOVEVM_VERSION` of Dockerfile#9
github.com/initia-labs/movevm v0.4.2
github.com/initia-labs/movevm v0.4.3
github.com/noble-assets/forwarding/v2 v2.0.0-20240521090705-86712c4c9e43
github.com/pelletier/go-toml v1.9.5
github.com/pkg/errors v0.9.1
Expand Down
4 changes: 2 additions & 2 deletions go.sum
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -733,8 +733,8 @@ github.com/initia-labs/OPinit/api v0.4.1 h1:Q8etW92LiwekKZxzDYVFdiHF3uOpEA4nyajy
github.com/initia-labs/OPinit/api v0.4.1/go.mod h1:Xy/Nt3ubXLQ4zKn0m7RuQOM1sj8TVdlNNyek21TGYR0=
github.com/initia-labs/cometbft v0.0.0-20240802022359-e0a5ce0336b6 h1:ObKvj9nGiKE+MWZ/LnH3rPcXsnBVVn4c30/iw+fMsd4=
github.com/initia-labs/cometbft v0.0.0-20240802022359-e0a5ce0336b6/go.mod h1:jHPx9vQpWzPHEAiYI/7EDKaB1NXhK6o3SArrrY8ExKc=
github.com/initia-labs/movevm v0.4.2 h1:5E4YaLyL7bJfL0mqBnMlu2jB5b3nkOys/RpLzuVkM+Q=
github.com/initia-labs/movevm v0.4.2/go.mod h1:6MxR4GP5zH3JUc1IMgfqAe1e483mZVS7fshPknZPJ30=
github.com/initia-labs/movevm v0.4.3 h1:BQmhv5zwakjzWDLoGmLFQAyCAbGQkDds1La4w3cOAJ4=
github.com/initia-labs/movevm v0.4.3/go.mod h1:6MxR4GP5zH3JUc1IMgfqAe1e483mZVS7fshPknZPJ30=
github.com/jhump/protoreflect v1.15.3 h1:6SFRuqU45u9hIZPJAoZ8c28T3nK64BNdp9w6jFonzls=
github.com/jhump/protoreflect v1.15.3/go.mod h1:4ORHmSBmlCW8fh3xHmJMGyul1zNqZK4Elxc8qKP+p1k=
github.com/jmespath/go-jmespath v0.0.0-20180206201540-c2b33e8439af/go.mod h1:Nht3zPeWKUH0NzdCt2Blrr5ys8VGpn0CEB0cQHVjt7k=
Expand Down
Loading