AMOUNT += run[0]
execute(DESTINATION1, FLOOR(AMOUNT/2), DESTINATION2, CEILING(AMOUNT/2))
}
execute(args){
PayTo(args[1], args[2])
PayTo(args[3], args[4])
}
Proof that this coin halver is buggy (there is no final balance stability):
1. Load first history entry that pays 0.0000001 COMB to coin halver
2. Load another history entry that pays 0.0000001 COMB to coin halver
3. Load coin halver
4.
DESTINATION1 = 0.0000001 COMB
DESTINATION2 = 0.0000001 COMB
1. Load first history entry that pays 0.0000001 COMB to coin halver
2. Load coin halver
3. Load another history entry that pays 0.0000001 COMB to coin halver
4.
DESTINATION1 = 0.0000000 COMB
DESTINATION2 = 0.0000002 COMB
Now it is not true that only the inventor of a buggy primitive loses money, what's worse that
the inventor will defraud others. In this case by sending history 1 to the DESTINATION1 user
and by sending history 2 to the DESTINATION2 user. Collectively they will see more money than there is.
This is why we need to be proving final balance stability and other virtuous properties about every
new primitive added to the currency.
We need to prove that (except on chain reorgs):
a. CONDITION can change to being TRUE only after being FALSE. (Or CONDITION be TRUE all the time)
b. if CONDITION is TRUE, CONNECT_TO address calculated cannot suddenly change. This means it must be impractical
to come up with two DISTINCT argument vectors so that ADDRESS1 == ADDRESS2 and CONDITION1 == CONDITION2 == TRUE and
CONNECT_TO1 != CONNECT_TO2
Fixed the hot cash.
256bit ARG[1] = Fallback address
256bit ARG[2] = Value at the end of the hashing sequence (to sign with the left leg of the decider)
256bit ARG[3] = Value at the end of the hashing sequence (to sign with the right leg of the decider)
256bit ARG[4] = Destination address.. A free variable (not hashed to the address)
256bit ARG[5] = Value needed to be commited on chain, a free variable (to sign with the left leg of the decider)
256bit ARG[6] = Value needed to be commited on chain, a free variable (to sign with the right leg of the decider)
ADDRESS = SHA256(ARG[1] CAT ARG[2] CAT ARG[3])
CONDITION = ENTRENCHED(ARG[5]) && ENTRENCHED(ARG[6]) &&
(IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3], 0, ARG[5...6]) ||
((ENTRENCHED(ARG[1]) && ENTRENCHED(ARG[4]) && IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3],
(CHAINPOSITON(ARG[4]) - CHAINPOSITON(ARG[1]), ARG[5...6])))))
CONNECT_TO = IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3], 0, ARG[5...6]) ? ARG[1] : ARG[4]
a. assume TRUE == IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3], 0, ARG[5...6]).
CONDITION = ENTRENCHED(ARG[5]) && ENTRENCHED(ARG[6])
the CONDITION is just TRUE because those preimages ARG[5], ARG[6] needed to be entrenched
assume FALSE == IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3], 0, ARG[5...6])
CONDITION = ENTRENCHED(ARG[5]) && ENTRENCHED(ARG[6]) &&
(((ENTRENCHED(ARG[1]) && ENTRENCHED(ARG[4]) && IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES(ARG[2...3],
(CHAINPOSITON(ARG[4]) - CHAINPOSITON(ARG[1]), ARG[5...6])))))
only 16bit numbers are signeable by the decider therefore to make the CONDITION TRUE:
- CHAINPOSITON(ARG[4]) - CHAINPOSITON(ARG[1]) must fit into 16bit int.
- CONDITION forces all of the values ARG[5], ARG[6], ARG[1], ARG[4] to be entrenched in order to become TRUE
- this turns them into CONSTANTS
- this turns the CONDITION into CONSTANTLY TRUE.
b. the CONNECT_TO can only change if IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES changes.
by ADDRESS1 == ADDRESS2 we have ARG1[2...3] == ARG2[2...3]
this forces ARG1[5...6] == ARG2[5...6] by 0 being a constant:
therefore IF_DECIDER_SIGNS_VALUE_USING_PREIMAGES cannot change.
therefore CONNECT_TO cannot change.
Guess this primitive
256bit ARG[1] = ALICE_ADDRESS
256bit ARG[2] = BOB_ADDRESS
256bit ARG[3] = ARBITRARY 256bit number
ADDRESS = SHA256(ARG[1] CAT ARG[2] CAT ARG[3])
CONDITION = TRUE
CONNECT_TO = SHA256( SHA256( SHA256(ARG[1] CAT ARG[2] CAT (ARG[3]+1)) CAT ARG[1] CAT 0.00000001 COMB ) CAT ARG[2] CAT 0.00000001 COMB )
a. CONDITION is always TRUE (end of proof)
b. by contradiction: ADDR1 != ADDR2 || CONNECT_TO1 == CONNECT_TO2
if ADDR1 != ADDR2:
then by SHA256 collision resistance ARGS1 == ARGS2:
but ARGS1 != ARGS2 if we want to prove something
if CONNECTTO1 == CONNECTTO2:
then by SHA256 collision resistance ARGS1 == ARGS2:
but ARGS1 != ARGS2 if we want to prove something
and so: ADDR1 == ADDR2 && CONNECT_TO1 != CONNECT_TO2
and therefore: CONNECT_TO1 != CONNECT_TO2
EDIT1: added code blocks.