-
Notifications
You must be signed in to change notification settings - Fork 229
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
316aada
commit 541e993
Showing
13 changed files
with
1,135 additions
and
0 deletions.
There are no files selected for viewing
43 changes: 43 additions & 0 deletions
43
.../zoe/test/unitTests/contracts/constantProduct/propertyBased/test-calcDeltaY-calcDeltaX.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import jsc from 'jsverify'; | ||
import { AmountMath } from '@agoric/ertp'; | ||
|
||
import { | ||
calcDeltaYSellingX, | ||
calcDeltaXSellingX, | ||
} from '../../../../../src/contracts/constantProduct/core'; | ||
import { setupMintKits } from '../setupMints'; | ||
|
||
const doTest = (x, y, deltaX) => { | ||
const { run, bld } = setupMintKits(); | ||
const runX = run(x); | ||
const bldY = bld(y); | ||
const runDeltaX = run(deltaX); | ||
const deltaY = calcDeltaYSellingX(runX, bldY, runDeltaX); | ||
const newDeltaX = calcDeltaXSellingX(runX, bldY, deltaY); | ||
|
||
// Pass through again, should always get the same answer. | ||
const newDeltaY = calcDeltaYSellingX(runX, bldY, newDeltaX); | ||
|
||
return AmountMath.isEqual(deltaY, newDeltaY); | ||
}; | ||
|
||
test('jsverify constant product calcDeltaYSellingX', t => { | ||
const runPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const secondaryPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const runValueInArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
|
||
const zeroOut = jsc.forall( | ||
runPoolAllocationArbitrary, | ||
secondaryPoolAllocationArbitrary, | ||
runValueInArbitrary, | ||
doTest, | ||
); | ||
|
||
t.true(jsc.check(zeroOut)); | ||
}); |
39 changes: 39 additions & 0 deletions
39
...es/zoe/test/unitTests/contracts/constantProduct/propertyBased/test-calcDeltaY-property.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import jsc from 'jsverify'; | ||
import { AmountMath } from '@agoric/ertp'; | ||
|
||
import { calcDeltaYSellingX } from '../../../../../src/contracts/constantProduct/core'; | ||
import { setupMintKits } from '../setupMints'; | ||
|
||
const doTest = (x, y, deltaX) => { | ||
const { run, bld } = setupMintKits(); | ||
const runX = run(x); | ||
const bldY = bld(y); | ||
const runDeltaX = run(deltaX); | ||
const deltaY = calcDeltaYSellingX(runX, bldY, runDeltaX); | ||
const oldK = BigInt(runX.value) * BigInt(bldY.value); | ||
const newX = AmountMath.add(runX, runDeltaX); | ||
const newY = AmountMath.subtract(bldY, deltaY); | ||
const newK = BigInt(newX.value) * BigInt(newY.value); | ||
return newK >= oldK; | ||
}; | ||
|
||
test('jsverify constant product calcDeltaYSellingX', t => { | ||
const runPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const secondaryPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const runValueInArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
|
||
const zeroOut = jsc.forall( | ||
runPoolAllocationArbitrary, | ||
secondaryPoolAllocationArbitrary, | ||
runValueInArbitrary, | ||
doTest, | ||
); | ||
|
||
t.true(jsc.check(zeroOut)); | ||
}); |
28 changes: 28 additions & 0 deletions
28
packages/zoe/test/unitTests/contracts/constantProduct/propertyBased/test-largeValues.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
|
||
import jsc from 'jsverify'; | ||
|
||
import { runTest } from '../runTest'; | ||
|
||
// larger values than this seem to take a really long time and the | ||
// test hangs | ||
test('jsverify constant product large values', t => { | ||
const runPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 30468); | ||
const secondaryPoolAllocationArbitrary = jsc.suchthat( | ||
jsc.nat(), | ||
u => u > 30468, | ||
); | ||
const runValueInArbitrary = jsc.suchthat(jsc.nat(), u => u < 30468 && u > 0); | ||
|
||
const constantProduct = jsc.forall( | ||
runPoolAllocationArbitrary, | ||
secondaryPoolAllocationArbitrary, | ||
runValueInArbitrary, | ||
runTest, | ||
); | ||
|
||
t.true(jsc.check(constantProduct)); | ||
}); |
43 changes: 43 additions & 0 deletions
43
packages/zoe/test/unitTests/contracts/constantProduct/propertyBased/test-reduction.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import jsc from 'jsverify'; | ||
import { AmountMath } from '@agoric/ertp'; | ||
|
||
import { | ||
calcDeltaYSellingX, | ||
calcDeltaXSellingX, | ||
} from '../../../../../src/contracts/constantProduct/core'; | ||
import { setupMintKits } from '../setupMints'; | ||
|
||
// Not currently functional | ||
const doTest = (x, y, deltaX) => { | ||
const { run, bld } = setupMintKits(); | ||
const runX = run(x); | ||
const bldY = bld(y); | ||
const runDeltaX = run(deltaX); | ||
const deltaY = calcDeltaYSellingX(runX, bldY, runDeltaX); | ||
const newDeltaX = calcDeltaXSellingX(runX, bldY, deltaY); | ||
|
||
const reduction = AmountMath.subtract(runDeltaX, newDeltaX); | ||
|
||
return AmountMath.isGTE(run(23), reduction); | ||
}; | ||
|
||
test('jsverify constant product calcDeltaYSellingX', t => { | ||
const runPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const secondaryPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
const runValueInArbitrary = jsc.suchthat(jsc.nat(), u => u > 1); | ||
|
||
const zeroOut = jsc.forall( | ||
runPoolAllocationArbitrary, | ||
secondaryPoolAllocationArbitrary, | ||
runValueInArbitrary, | ||
doTest, | ||
); | ||
|
||
t.true(jsc.check(zeroOut)); | ||
}); |
26 changes: 26 additions & 0 deletions
26
packages/zoe/test/unitTests/contracts/constantProduct/propertyBased/test-smallValues.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
|
||
import jsc from 'jsverify'; | ||
|
||
import { runTest } from '../runTest'; | ||
|
||
test('jsverify constant product small values', t => { | ||
const runPoolAllocationArbitrary = jsc.suchthat(jsc.nat(), u => u > 10000); | ||
const secondaryPoolAllocationArbitrary = jsc.suchthat( | ||
jsc.nat(), | ||
u => u > 10000, | ||
); | ||
const runValueInArbitrary = jsc.suchthat(jsc.nat(), u => u < 10000 && u > 0); | ||
|
||
const constantProduct = jsc.forall( | ||
runPoolAllocationArbitrary, | ||
secondaryPoolAllocationArbitrary, | ||
runValueInArbitrary, | ||
runTest, | ||
); | ||
|
||
t.true(jsc.check(constantProduct)); | ||
}); |
38 changes: 38 additions & 0 deletions
38
packages/zoe/test/unitTests/contracts/constantProduct/runTest.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
// @ts-check | ||
|
||
import { Nat } from '@agoric/nat'; | ||
|
||
import { | ||
DEFAULT_POOL_FEE, | ||
DEFAULT_PROTOCOL_FEE, | ||
} from '../../../../src/contracts/constantProduct/defaults'; | ||
import { specifyRunIn } from '../../../../src/contracts/constantProduct/specifyRunIn'; | ||
import { checkKInvariantSellingX } from '../../../../src/contracts/constantProduct/invariants'; | ||
import { setupMintKits } from './setupMints'; | ||
|
||
export const runTest = ( | ||
runPoolAllocationNat, | ||
secondaryPoolAllocationNat, | ||
runValueInNat, | ||
) => { | ||
const { bld, run } = setupMintKits(); | ||
const runAmountIn = run(Nat(runValueInNat)); | ||
const runPoolAllocation = run(Nat(runPoolAllocationNat)); | ||
const bldPoolAllocation = bld(Nat(secondaryPoolAllocationNat)); | ||
|
||
const result = specifyRunIn( | ||
runAmountIn, | ||
runPoolAllocation, | ||
bldPoolAllocation, | ||
DEFAULT_PROTOCOL_FEE, | ||
DEFAULT_POOL_FEE, | ||
); | ||
// console.log(result); | ||
|
||
return checkKInvariantSellingX( | ||
runPoolAllocation, | ||
bldPoolAllocation, | ||
result.deltaRun, | ||
result.deltaSecondary, | ||
); | ||
}; |
19 changes: 19 additions & 0 deletions
19
packages/zoe/test/unitTests/contracts/constantProduct/setupMints.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
// @ts-check | ||
|
||
import { AmountMath, makeIssuerKit, AssetKind } from '@agoric/ertp'; | ||
|
||
export const setupMintKits = () => { | ||
const runKit = makeIssuerKit( | ||
'RUN', | ||
AssetKind.NAT, | ||
harden({ decimalPlaces: 6 }), | ||
); | ||
const bldKit = makeIssuerKit( | ||
'BLD', | ||
AssetKind.NAT, | ||
harden({ decimalPlaces: 6 }), | ||
); | ||
const run = value => AmountMath.make(runKit.brand, value); | ||
const bld = value => AmountMath.make(bldKit.brand, value); | ||
return { runKit, bldKit, run, bld }; | ||
}; |
69 changes: 69 additions & 0 deletions
69
packages/zoe/test/unitTests/contracts/constantProduct/test-calcDeltaY.js
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
// @ts-check | ||
|
||
// eslint-disable-next-line import/no-extraneous-dependencies | ||
import { test } from '@agoric/zoe/tools/prepare-test-env-ava'; | ||
import { AmountMath } from '@agoric/ertp'; | ||
|
||
import { calcDeltaYSellingX } from '../../../../src/contracts/constantProduct/core'; | ||
import { setupMintKits } from './setupMints'; | ||
|
||
// the brands of x and y shouldn't matter (test this explicitly in a | ||
// separate test) | ||
const doTest = (t, x, y, deltaX, expectedDeltaY) => { | ||
const { run, bld } = setupMintKits(); | ||
const result = calcDeltaYSellingX(run(x), bld(y), run(deltaX)); | ||
t.true( | ||
AmountMath.isEqual(result, bld(expectedDeltaY)), | ||
`${result.value} equals ${expectedDeltaY}`, | ||
); | ||
}; | ||
|
||
// deltaXPlusX is 0 | ||
test('0, 0, 0, 0', t => { | ||
t.throws(() => doTest(t, 0, 0, 0, 0), { | ||
message: 'No infinite ratios! Denominator was 0/"[Alleged: RUN brand]"', | ||
}); | ||
}); | ||
|
||
test('0, 0, 1, 0', t => { | ||
doTest(t, 0, 0, 1, 0); | ||
}); | ||
|
||
test('1, 0, 0, 0', t => { | ||
doTest(t, 1, 0, 0, 0); | ||
}); | ||
|
||
// deltaXPlusX is 0 | ||
test('0, 1, 0, 0', t => { | ||
t.throws(() => doTest(t, 0, 1, 0, 0), { | ||
message: 'No infinite ratios! Denominator was 0/"[Alleged: RUN brand]"', | ||
}); | ||
}); | ||
|
||
test('1, 1, 0, 0', t => { | ||
doTest(t, 1, 1, 0, 0); | ||
}); | ||
|
||
test('1, 1, 1, 0', t => { | ||
doTest(t, 1, 1, 1, 0); | ||
}); | ||
|
||
test('1, 2, 1, 1', t => { | ||
doTest(t, 1, 2, 1, 1); | ||
}); | ||
|
||
test('2, 3, 4, 2', t => { | ||
doTest(t, 2, 3, 4, 2); | ||
}); | ||
|
||
test('928861206, 130870247, 746353662, 58306244', t => { | ||
doTest(t, 928861206n, 130870247n, 746353662n, 58306244n); | ||
}); | ||
|
||
test('9, 3, 17, 1', t => { | ||
doTest(t, 9, 3, 17, 1); | ||
}); | ||
|
||
test('10000, 5000, 209, 102', t => { | ||
doTest(t, 10000, 5000, 209, 102); | ||
}); |
Oops, something went wrong.