henry-hz
commented
1 month ago Dafny fixed point arithimetic:
include "number.dfy"
include "maps.dfy"
include "tx.dfy"
// Fixed point arithmetic math
// https://github.com/dapphub/ds-math/blob/master/src/math.sol
module Fixed {
import opened Number
import opened Maps
import opened Tx
const WAD: u256 := 1_000_000_000_000_000_000 // 18 zeros
const RAY: u256 := 1_000_000_000_000_000_000_000_000_000
function Add(x: u256, y: u256) : u256
requires (x as nat) + (y as nat) <= MAX_U256 as nat{
x + y
}
function Sub(x: u256, y: u256) : u256
requires (x as nat) - (y as nat) >= 0 as nat {
x - y
}
function Mul(x: u256, y: u256) : u256
requires (x as nat) * (y as nat) <= MAX_U256 as nat {
x * y
}
function Wmul(x: u256, y: u256) : u256
requires y == 0 || (x as nat) * (y as nat) <= MAX_U256 as nat
requires Mul(x,y) as nat <= MAX_U256 {
var m: u256 := Mul(x,y);
var w: u256 := WAD / 2;
assume {:axiom} (m as nat) + (w as nat) <= MAX_U256 as nat;
(Add(m , w))/WAD
}
function Wmul2(x: nat, y: nat) : nat {
var w := 1000000000000000000;
((x * y) + (w / 2)) / w
}
}
// --- TESTS
import opened Fixed
import opened Number
import opened Maps
import opened Tx
method {:test} testFindMax() {
var j := 1000000000000000000 as u256;
var i := 1000000000000000000 as u256;
var r := 1000000000000000000 as u256;
assert Wmul(j,i) == r;
assert Wmul(WAD, WAD) == WAD;
var x : nat := 100000000000000000;
// 10^18 * 10^18 = 10^36
//print(x*x); // it has 34 zeros ! help
var x1 : nat := 1000000000000000000;
var x2 : nat := 1000000000000000000;
var r1 : nat := 1000000000000000000000000000000000000;
var r2 : nat := (r1 + (x1/2)) / x1;
assert x1*x2 == r1;
assert Wmul2(x1, x2) == 1000000000000000000; // 18 zeros
print(x1*x2);
assert r2 == x1;
}
In this task you should do the following with the tutorial
scriptfolder] in solidity. See hereCompoundWhitepaper.pdf Compound.Whitepaper-2.pdf Compound V2 in Depth. A hands-on guide by R Better Programming.pdf
International Accounting Standards (IAS) are a set of principles-based standards and interpretations established to ensure consistency, transparency, and comparability in financial statements across different countries. They are designed to provide a global framework for how public companies prepare and disclose their financial statements. The International Accounting Standards Board (IASB) is responsible for developing and issuing these standards, known collectively as International Financial Reporting Standards (IFRS).
Key Concepts of International Accounting Standards (IAS):
Principles-Based Approach: IAS/IFRS use a principles-based approach, which provides broad guidelines and objectives, allowing for flexibility and professional judgment in applying the standards.
Consistency: By following IAS/IFRS, companies ensure their financial statements are consistent over time and comparable with those of other companies, both domestically and internationally.
Transparency: These standards aim to improve transparency in financial reporting, helping stakeholders understand the financial position and performance of a company.
Comprehensive Framework: IAS/IFRS cover various aspects of accounting, including recognition, measurement, presentation, and disclosure of transactions and events.
Double-Entry Accounting:
The double-entry accounting system is a fundamental concept in accounting, which ensures that every financial transaction affects at least two accounts, maintaining the accounting equation:
Assets = Liabilities + Equity
For every transaction:
Compound's Accounting Framework:
The given formula for Compound’s money markets follows the basic accounting principles:
Cash-a + Borrows-a = Supply-a + Equity-a
Where:
How Transactions Generate Accounting Entries:
Each transaction in Compound’s system affects the balance sheet by creating two corresponding accounting entries (debit and credit) to maintain the accounting equation. Let's break down a few example transactions:
1. Supply (Deposit) Transaction:
When a user supplies assets to the money market:
2. Borrow Transaction:
When a user borrows assets from the money market:
3. Repayment of Borrow:
When a user repays the borrowed amount:
4. Interest Accrual on Borrowed Amount:
When interest accrues on the borrowed amount:
5. Interest Accrual on Supplied Amount:
When interest accrues on the supplied amount:
Auditable Balance Sheet and Ledger:
Maintaining an auditable balance sheet and ledger means that all transactions are recorded with detailed entries that can be traced and verified. This involves:
By adhering to these principles, Compound ensures that its financial records are accurate, transparent, and compliant with international standards, facilitating trust and confidence among users, regulators, and investors.
The equation Assets = Liabilities + Equity is the foundational principle of double-entry accounting, known as the accounting equation. It represents the relationship between a company's resources and the claims against those resources. This equation must always balance, ensuring that the financial statements are accurate and consistent.
Components of the Accounting Equation:
Assets:
Liabilities:
Equity:
Understanding the Equation:
The accounting equation shows that what the company owns (assets) is financed by what it owes (liabilities) and the owners’ investment (equity). This relationship can be expressed as follows:
Assets = Liabilities + Equity
This equation must always balance because every financial transaction affects at least two accounts, keeping the equation in equilibrium.
Example Transactions and Their Impact:
1. Owner Investment:
When an owner invests cash into the business:
Entry:
Assets = Liabilities + Equity $10,000 = $0 + $10,000
2. Taking Out a Loan:
When the company takes out a loan:
Entry:
Assets = Liabilities + Equity $15,000 = $5,000 + $10,000
3. Purchasing Equipment with Cash:
When the company purchases equipment using cash:
Entry:
Assets = Liabilities + Equity $12,000 + $3,000 = $5,000 + $10,000 $15,000 = $5,000 + $10,000
4. Earning Revenue:
When the company earns revenue and receives cash:
Entry:
Assets = Liabilities + Equity $17,000 = $5,000 + $12,000
5. Paying Expenses:
When the company pays expenses with cash:
Entry:
Assets = Liabilities + Equity $16,000 = $5,000 + $11,000
Maintaining Balance:
The double-entry system ensures that the accounting equation always remains balanced. Each transaction is recorded in at least two accounts, with equal debits and credits. This system not only ensures accuracy but also helps in tracking financial performance and the company’s financial position over time.
Conclusion:
The accounting equation Assets = Liabilities + Equity is crucial for maintaining the integrity of a company's financial records. It provides a clear and consistent framework for recording and reporting financial transactions, ensuring that the company's financial statements are accurate, reliable, and comparable.