diff --git a/programs/manifest/src/certora/spec/cancel_order_checks.rs b/programs/manifest/src/certora/spec/cancel_order_checks.rs index deda8f25a..071574c82 100644 --- a/programs/manifest/src/certora/spec/cancel_order_checks.rs +++ b/programs/manifest/src/certora/spec/cancel_order_checks.rs @@ -122,7 +122,6 @@ pub fn cancel_order_by_index_no_revert() { // -- call to cancel_order_by_index let market_data = &mut market_info.try_borrow_mut_data().unwrap(); let mut dynamic_account: MarketRefMut = get_mut_dynamic_account(market_data); - let trader_index = crate::state::second_trader_index(); let order_index = maker_order_index; let result = dynamic_account.cancel_order_by_index(order_index, &[None, None]); cvt_assert!(result.is_ok()); diff --git a/programs/manifest/src/certora/spec/funds_checks.rs b/programs/manifest/src/certora/spec/funds_checks.rs index 7d1d1f8c4..6a35ee116 100644 --- a/programs/manifest/src/certora/spec/funds_checks.rs +++ b/programs/manifest/src/certora/spec/funds_checks.rs @@ -371,7 +371,6 @@ pub fn cancel_order_by_index_check() { cvt_assume_funds_invariants(balances_old); // -- call to cancel_order_by_index - let trader_index = second_trader_index(); let order_index = maker_order_index; cancel_order_by_index!(market_info, order_index); diff --git a/programs/manifest/src/certora/spec/matching_checks.rs b/programs/manifest/src/certora/spec/matching_checks.rs index f0c107105..7628645d8 100644 --- a/programs/manifest/src/certora/spec/matching_checks.rs +++ b/programs/manifest/src/certora/spec/matching_checks.rs @@ -446,7 +446,7 @@ pub fn matching_decrease_maker_order_atoms() { place_single_order_nondet_inputs::(market_info); // -- call to place_single_order - let (res, _total_base_atoms_traded, _total_quote_atoms_traded) = place_single_order!( + let (_res, _total_base_atoms_traded, _total_quote_atoms_traded) = place_single_order!( market_info, args, remaining_base_atoms, diff --git a/programs/manifest/src/state/global.rs b/programs/manifest/src/state/global.rs index 082010d0a..10f9a2252 100644 --- a/programs/manifest/src/state/global.rs +++ b/programs/manifest/src/state/global.rs @@ -11,7 +11,6 @@ use hypertree::{ get_helper, get_mut_helper, DataIndex, FreeList, Get, HyperTreeReadOperations, HyperTreeWriteOperations, RBNode, RedBlackTree, RedBlackTreeReadOnly, NIL, }; - use shank::ShankType; use solana_program::{entrypoint::ProgramResult, program_error::ProgramError, pubkey::Pubkey}; use static_assertions::const_assert_eq; diff --git a/programs/manifest/src/validation/loaders.rs b/programs/manifest/src/validation/loaders.rs index 07b422e1e..47e186df8 100644 --- a/programs/manifest/src/validation/loaders.rs +++ b/programs/manifest/src/validation/loaders.rs @@ -466,7 +466,11 @@ impl<'a, 'info> BatchUpdateContext<'a, 'info> { ManifestAccountInfo::::new(next_account_info(account_iter)?)?; let system_program: Program = Program::new(next_account_info(account_iter)?, &system_program::id())?; - + // Certora version is not mutable. + #[cfg(feature = "certora")] + let global_trade_accounts_opts: [Option>; 2] = + [None, None]; + #[cfg(not(feature = "certora"))] let mut global_trade_accounts_opts: [Option>; 2] = [None, None]; diff --git a/programs/manifest/verify-manifest b/programs/manifest/verify-manifest deleted file mode 100755 index 588b7b740..000000000 --- a/programs/manifest/verify-manifest +++ /dev/null @@ -1,250 +0,0 @@ -#!python3 - -from enum import Enum -import subprocess -import io -import sys -import datetime -import time -import os -import json -import argparse - -remote = False - - -class VerificationResult(Enum): - Verified = 0 - Violated = 1 - Timeout = 2 - UnexpectedError = 3 - - def __str__(self): - return f"{self.name}" - - @staticmethod - def from_string(result: str) -> 'VerificationResult': - return VerificationResult[result] - - @staticmethod - def from_command_result(command_result: subprocess.CompletedProcess[str]) -> 'VerificationResult': - if command_result.returncode == 0: - assert "|Not violated" in command_result.stdout, "The verification terminated successfully, but cannot find the '|Not violated' substring in stdout" - return VerificationResult.Verified - elif "|Violated" in command_result.stdout: - # If the return code is not zero, and in the stdout we find `|Violated`, - # then the verification of the rule failed. - return VerificationResult.Violated - elif "|Timeout" in command_result.stdout: - # If the return code is not zero, and in the stdout we find `|Timeout`, - # then the verification of the rule failed. - return VerificationResult.Timeout - else: - # If the return code is not zero, but we cannot find `|Violated` in - # stdout, then we had an unexpected error while calling `just`. - return VerificationResult.UnexpectedError - - -class ProverOption: - '''Option to give to the prover.''' - pass - - -class Bmc(ProverOption): - def __init__(self, n: int): - self.n = n - - def __str__(self) -> str: - return f'-bmc {self.n}' if not remote else f'--loop_iter {self.n}' - - -class AssumeUnwindCond(ProverOption): - def __str__(self) -> str: - return f'-assumeUnwindCond' if not remote else f'--optimistic_loop' - - -class CargoFeature: - '''Cargo feature to use when calling `cargo build-sbf`.''' - pass - - -class CvtDbMock(CargoFeature): - def __str__(self) -> str: - return 'cvt-db-mock' - - -class Rule: - def __init__(self, name: str, expected_result: VerificationResult, prover_options: list[ProverOption], cargo_features: list[CargoFeature]): - self.name = name - self.expected_result = expected_result - self.prover_options = prover_options - self.cargo_features = cargo_features - - def __str__(self) -> str: - return f"{self.name}" - - @staticmethod - def list_from_json(rules_config_file_path: str) -> list['Rule']: - with open(rules_config_file_path, 'r') as f: - data = json.load(f) - - rules = [] - for rule_data in data['rules']: - name = rule_data['name'] - - # Load expected result - expected_result_str = rule_data.get('expected_result') - if expected_result_str not in VerificationResult.__members__: - raise ValueError(f"Invalid expected result '{ - expected_result_str}' for rule '{name}'") - expected_result = VerificationResult.from_string( - expected_result_str) - - # Load prover options - prover_options = [] - for option in rule_data['prover_options']: - if 'bmc' in option: - if not isinstance(option['bmc'], int): - raise TypeError(f"Invalid type for 'bmc' option in rule '{ - name}', expected integer") - prover_options.append(Bmc(option['bmc'])) - elif 'assumeUnwindCond' in option: - if not isinstance(option['assumeUnwindCond'], bool): - raise TypeError(f"Invalid type for 'assumeUnwindCond' option in rule '{ - name}', expected boolean") - prover_options.append(AssumeUnwindCond()) - else: - raise ValueError(f"Unknown prover option '{ - option}' in rule '{name}'") - - # Load cargo features - cargo_features = [] - valid_features = { - 'cvt-db-mock': lambda: CvtDbMock() - } - for feature in rule_data['cargo_features']: - if feature not in valid_features: - raise ValueError(f"Unknown cargo feature '{ - feature}' in rule '{name}'") - else: - cargo_features.append(valid_features[feature]()) - - rules.append(Rule(name, expected_result, - prover_options, cargo_features)) - - return rules - - -class VerificationRunner: - def __init__(self): - self.had_error = False - - def verify_all(self, rules: list[Rule]): - logfile_name = VerificationRunner.generate_logfile_name() - with open(logfile_name, 'w') as logfile: - for (index, rule) in enumerate(rules): - print(f'[{index+1:2}/{len(rules)}] {rule.name} ... ', end='') - self.verify_rule(logfile, rule) - VerificationRunner.clean() - if self.had_error: - sys.exit(1) - - def verify_rule(self, logfile: io.TextIOWrapper, rule: Rule): - sys.stdout.flush() - command = VerificationRunner.build_command(rule) - try: - start_time = time.time() - verification_result = self.run_verification(command, logfile, rule) - end_time = time.time() # Record the end time - elapsed_time = end_time - start_time # Calculate the elapsed time - self.check_verification_result( - verification_result, rule.expected_result, command, elapsed_time) - except FileNotFoundError: - print(f"Failed to run command: `{command}`") - - @staticmethod - def build_command(rule: Rule) -> str: - command = f'just verify{'-remote' if remote else ''} {rule.name}' - for option in rule.prover_options: - command += f' {option}' - return command - - def run_verification(self, command: str, logfile: io.TextIOWrapper, rule: Rule) -> VerificationResult: - verification_env = VerificationRunner.build_verification_env(rule) - # Run the verifier and capure the output. - command_result = subprocess.run( - command.split(), check=False, text=True, capture_output=True, env=verification_env) - VerificationRunner.log_output( - logfile, rule.name, command, command_result) - return VerificationResult.from_command_result(command_result) - - @staticmethod - def build_verification_env(rule: Rule) -> dict[str, str]: - # Start with the current environment variables - verification_env = os.environ.copy() - cargo_features = '' - for feature in rule.cargo_features: - cargo_features += f' {feature}' - verification_env["CARGO_FEATURES"] = cargo_features - return verification_env - - def check_verification_result(self, verification_result: VerificationResult, expected_result: VerificationResult, command: str, elapsed_seconds: float) -> None: - # Assert that we did not have an unexpected error (i.e., compilation - # error), since all the rules should be verified or not verified. - assert verification_result != VerificationResult.UnexpectedError, \ - f"Had unexpected error running `{command}`" - - # A timeout is an unexpected event - assert verification_result != VerificationResult.Timeout, \ - f"Had a timeout event running `{command}`" - - if verification_result == expected_result: - print(f'ok ({elapsed_seconds:.2f}s)') - else: - print(f'error ({elapsed_seconds:.2f}s)') - print(f'\tExpected result: {expected_result}') - print(f'\tActual result: {verification_result}') - self.had_error = True - - @staticmethod - def generate_logfile_name() -> str: - current_time = datetime.datetime.now() - return current_time.strftime("log_verification_%Y-%m-%d_%H:%M:%S") - - @staticmethod - def log_output(logfile: io.TextIOWrapper, rule_name: str, command: str, command_result: subprocess.CompletedProcess[str]) -> None: - print(f'---- Rule {rule_name} ----', file=logfile) - print(f'Command: `{command}`', file=logfile) - print(f'Return code: {command_result.returncode}', file=logfile) - print(f'Stdout:', file=logfile) - print(command_result.stdout, file=logfile) - print(f'Stderr:', file=logfile) - print(command_result.stderr, file=logfile) - - @staticmethod - def clean() -> None: - ''' Call `just clean`. ''' - subprocess.run(["just", "clean"], check=True, capture_output=True) - -# TODO: @phreppo - should sanity rules be added? - - -# Parse the CLI options -parser = argparse.ArgumentParser( - description="Run the rules as specified in a JSON configuration file") -parser.add_argument( - "-r", "--rules", - help="Path to the JSON configuration file with the rules specification.", - type=str, - default="rules.json" -) -parser.add_argument('--remote', action='store_true', - help="Run the verification on remote.") -args = parser.parse_args() - -if args.remote: - remote = True - -rules = Rule.list_from_json(args.rules) -runner = VerificationRunner() -runner.verify_all(rules)