# This justfile compiles the code and copies the executable in the current
# working directory. After modifying the source code, remember to recompile the
# code and commit the changes to the executable.
# This script is only used to update the .so file when needed. The test itself
# does not call `cargo certora-sbf`

export ARCH := env_var_or_default("ARCH", "")

export EXECUTABLE_PATH := if ARCH == "v1" {
    "./target/sbpfv1-solana-solana/release/counter.so"
} else {
    "./target/sbpf-solana-solana/release/counter.so"
}

_arch_flag := if ARCH == "v1" { "--arch v1" } else { "" }
_tools_version := "v1.53"
_output_name := if ARCH == "v1" { "counter.sbpfv1.so" } else { "counter.so" }

build-sbf:
    cargo certora-sbf --tools-version {{ _tools_version }} {{ _arch_flag }}
    cp $EXECUTABLE_PATH {{ _output_name }}
    rm -Rf target

# java executable
export JAVA := env_var_or_default("JAVA", "java")
# optimization level, 0 by default
export TAC_OPT_LEVEL := env_var_or_default("TAC_OPT_LEVEL", "0")
# sanity check level: none, basic, advanced (none by default)
export SANITY_CHECKS := env_var_or_default("SANITY_CHECKS", "none")

inliner_cfg := "../cvlr_inlining.txt"
summaries_cfg := "../cvlr_summaries.txt"
sbf_file := if ARCH == "v1" { "../counter.sbpfv1.so" } else { "../counter.so" }

# location of prover jar
emv_jar := "$CERTORA/emv.jar"

# Usage: verify name_of_rule extra_options
verify RULE *OPTS: # build-sbf
		mkdir -p certora_out
		cd certora_out && ${JAVA} \
		-Dtopic.spec -Dlevel.sbf=${CERTORA_VERBOSE:-info} \
		-Dverbose.times -Dcvt.simple.parallel -Djava.awt.headless=true \
		-jar {{ emv_jar }} \
		-deleteSMTFile false -graphDrawLimit 2000 \
		{{ sbf_file }} \
		-solanaInlining {{ inliner_cfg }} \
		-solanaSummaries {{ summaries_cfg }} \
		-solanaPrintDevMsg true \
		-solanaPrintAnalyzedToDot \
		-solanaTACOptimize ${TAC_OPT_LEVEL} \
		-ruleSanityChecks ${SANITY_CHECKS} \
		-rule {{ RULE }} \
		{{ OPTS }}

clean:
    rm -Rf emv-*
    rm -f *.dot *.svg *.pdf
    rm -Rf .certora_internal