earnAUSD (share symbol sAUSD)

No counterexample in 16 fuzz runs at this block.

Checks: asset() does not revert

No counterexample in 16 fuzz runs at this block.

Checks: totalAssets() does not revert

No counterexample in 16 fuzz runs at this block.

Checks: convertToShares gives the same result for any caller

No counterexample in 16 fuzz runs at this block.

Checks: convertToAssets gives the same result for any caller

No counterexample in 16 fuzz runs at this block.

Checks: maxDeposit does not revert

No counterexample in 16 fuzz runs at this block.

Checks: deposit mints at least the shares previewDeposit quoted

No counterexample in 16 fuzz runs at this block.

Checks: deposit moves assets from the caller, credits shares to the receiver and spends allowance

No counterexample in 16 fuzz runs at this block.

Checks: maxMint does not revert

No counterexample in 16 fuzz runs at this block.

Checks: mint pulls at most the assets previewMint quoted

No counterexample in 16 fuzz runs at this block.

Checks: mint moves assets from the caller, credits shares to the receiver and spends allowance

No counterexample in 16 fuzz runs at this block.

Checks: maxWithdraw does not revert

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw burns at most the shares previewWithdraw quoted

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 291 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw burns owner shares, pays the receiver and spends share allowance

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 291 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

No counterexample in 16 fuzz runs at this block.

Checks: withdraw on behalf of an owner without allowance reverts

No counterexample in 16 fuzz runs at this block.

Checks: maxRedeem does not revert

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem pays at least the assets previewRedeem quoted

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 291 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem burns owner shares, pays the receiver and spends share allowance

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 291 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

No counterexample in 16 fuzz runs at this block.

Checks: redeem on behalf of an owner without allowance reverts

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem(deposit(a)) returns no more than a

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw(a) burns at least the shares deposit(a) minted

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: deposit(redeem(s)) mints no more than s

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: mint(s) costs at least the assets redeem(s) paid

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw(mint(s)) burns at least s shares

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem(s) pays no more than mint(s) cost

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: mint(withdraw(a)) costs at least a

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 325 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: deposit(a) mints no more than the shares withdraw(a) burned

reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 325 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0

No counterexample in 16 fuzz runs at this block.

Checks: deposit goes through up to min(maxDeposit, 1e6 tokens); when a smaller amount is refused the bound must go through, and refusals are counted (EIP-4626: maxDeposit MUST NOT be higher than what deposit accepts)

No counterexample in 16 fuzz runs at this block.

Checks: mint goes through up to min(maxMint, shares of 1e6 tokens); when a smaller amount is refused the bound must go through, and refusals are counted (EIP-4626: maxMint MUST NOT be higher than what mint accepts)

maxWithdraw was 609,877,786,697, but withdraw(609,877,786,695) reverted with 0x75ed2e3e, WithdrawalRequestRequired(). EIP-4626: maxWithdraw MUST return the maximum amount of assets withdraw accepts without reverting, and 0 while withdrawals are disabled.

For an asynchronous vault, ERC-7540 still requires maxWithdraw and maxRedeem to report what can be claimed now.

Checks: withdraw goes through up to maxWithdraw; when a smaller amount is refused maxWithdraw must go through, and refusals are counted (EIP-4626: maxWithdraw MUST NOT be higher than what withdraw accepts, and MUST be 0 when withdrawals are disabled)

reason: withdraw(609877786695) reverted with selector 0x75ed2e3e while maxWithdraw is 609877786697
runs: 0
call: test_sf_maxWithdraw_honored(204021641170440950934057, 170272127362186878622977996674609877786698, 115792089237316195423570985008687907853269984665640564039457584007913129639933)
calldata: 0x72b950e2000000000000000000000000000000000000000000002b34090b5b8898106a29000000000000000000000000000001f46282e0cd79769bb5d41b6d1ee9cea04afffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd

maxRedeem was 606,678,772,778, but redeem(606,678,772,776) reverted with 0x75ed2e3e, WithdrawalRequestRequired(). EIP-4626: maxRedeem MUST return the maximum amount of shares redeem accepts without reverting, and 0 while redemptions are disabled.

For an asynchronous vault, ERC-7540 still requires maxWithdraw and maxRedeem to report what can be claimed now.

Checks: redeem goes through up to maxRedeem; when a smaller amount is refused maxRedeem must go through, and refusals are counted (EIP-4626: maxRedeem MUST NOT be higher than what redeem accepts, and MUST be 0 when redemptions are disabled)

reason: redeem(606678772776) reverted with selector 0x75ed2e3e while maxRedeem is 606678772778
runs: 0
call: test_sf_maxRedeem_honored(204021641170440950934057, 170272127362186878622977996674609877786698, 115792089237316195423570985008687907853269984665640564039457584007913129639933)
calldata: 0x942509aa000000000000000000000000000000000000000000002b34090b5b8898106a29000000000000000000000000000001f46282e0cd79769bb5d41b6d1ee9cea04afffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd