[Prover] Added DeFi examples

[junkil-park]

Description

• Created two DeFi examples, revamping the previous rounding error examples
  • One is a simple dex pool based on Uniswap V1
  • Another is a simple reserve-backed currency system
• Defined the safety properties for the examples, and proved them with Move Prover

[trunk-io]

⏱️ 2h 37m total CI duration on this PR

Job	Cumulative Duration	Recent Runs
rust-move-unit-coverage	1h	🟩 🟩 🟩
rust-move-tests	36m	🟩 🟩 🟩
rust-targeted-unit-tests	17m	🟩 🟩 🟩
rust-lints	17m	🟩 🟩 🟩
run-tests-main-branch	14m	🟩 🟩 🟩
general-lints	5m	🟩 🟩 🟩
check-dynamic-deps	4m	🟩 🟩 🟩
semgrep/ci	1m	🟩 🟩 🟩
file_change_determinator	35s	🟩 🟩 🟩
file_change_determinator	29s	🟩 🟩 🟩
permission-check	12s	🟩 🟩 🟩
permission-check	9s	🟩 🟩 🟩
permission-check	8s	🟩 🟩 🟩
permission-check	7s	🟩 🟩 🟩

🚨 1 job on the last run was significantly faster/slower than expected

Job	Duration	vs 7d avg	Delta
rust-targeted-unit-tests	6m	19m

_{settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io}

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 58.4%. Comparing base (6ca7c3f) to head (28b67a4).

Additional details and impacted files

@@             Coverage Diff             @@
##             main   #13281       +/-   ##
===========================================
- Coverage    71.9%    58.4%    -13.6%     
===========================================
  Files        2314      821     -1493     
  Lines      455089   197405   -257684     
===========================================
- Hits       327642   115411   -212231     
+ Misses     127447    81994    -45453     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[rahxephon89]

LGTM, thanks!

[github-actions]

✅ Forge suite compat success on a68e71c05caebf01504d4499110f3fba213fb53d ==> 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e

Compatibility test results for a68e71c05caebf01504d4499110f3fba213fb53d ==> 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e (PR)
1. Check liveness of validators at old version: a68e71c05caebf01504d4499110f3fba213fb53d
compatibility::simple-validator-upgrade::liveness-check : committed: 9746.495630454841 txn/s, latency: 3016.958414316818 ms, (p50: 2700 ms, p90: 3600 ms, p99: 9200 ms), latency samples: 376620
2. Upgrading first Validator to new version: 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 3326.075584258906 txn/s, latency: 9296.80203023758 ms, (p50: 9300 ms, p90: 14100 ms, p99: 14500 ms), latency samples: 138900
3. Upgrading rest of first batch to new version: 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 3393.7527987116705 txn/s, latency: 9136.500649540214 ms, (p50: 9400 ms, p90: 14100 ms, p99: 14400 ms), latency samples: 137020
4. upgrading second batch to new version: 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 6385.542686253354 txn/s, latency: 5092.579079002958 ms, (p50: 4800 ms, p90: 8300 ms, p99: 9400 ms), latency samples: 236700
5. check swarm health
Compatibility test for a68e71c05caebf01504d4499110f3fba213fb53d ==> 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e passed
Test Ok

• Grafana dashboard
• Humio Logs
• Axiom Logs
• Validator CPU Profile
• Fullnode CPU Profile
• Test runner output
• Test run is land-blocking

[github-actions]

✅ Forge suite realistic_env_max_load success on 28b67a4575360b8bfcc4ecf8cd022d2c75d7fe9e

two traffics test: inner traffic : committed: 8507.04305090524 txn/s, latency: 4609.708181144778 ms, (p50: 4500 ms, p90: 5400 ms, p99: 10200 ms), latency samples: 3671980
two traffics test : committed: 99.96345066766115 txn/s, latency: 2049.0604395604396 ms, (p50: 2000 ms, p90: 2300 ms, p99: 3100 ms), latency samples: 1820
Latency breakdown for phase 0: ["QsBatchToPos: max: 0.217, avg: 0.205", "QsPosToProposal: max: 0.221, avg: 0.208", "ConsensusProposalToOrdered: max: 0.398, avg: 0.375", "ConsensusOrderedToCommit: max: 0.371, avg: 0.358", "ConsensusProposalToCommit: max: 0.741, avg: 0.733"]
Max round gap was 1 [limit 4] at version 1702146. Max no progress secs was 4.896326 [limit 15] at version 1702146.
Test Ok

• Grafana dashboard
• Humio Logs
• Axiom Logs
• Validator CPU Profile
• Fullnode CPU Profile
• Test runner output
• Test run is land-blocking