Michelson (and higher level language like Liquidity on top of it) does not allow a smart contract to call another smart contract without commmitting its state/storage first. It makes reentrancy attacks less likely to happen, but not impossible.
The clue to the solution is in the part of the error saying that Validation of block BK... failed.
It seems that it wasn't checking to see if there was any new free disk space available, it was just reading back the error of why it failed in the first place. And when it failed to validate the block, the block was marked as invalid.
After running ./tezos-...
So this is a huge question and I think there are many people more qualified than me, but I'll offer some initial guidance.
In Software Foundations, a book on Coq, they talk about an implied language called Imp. Imp has a syntax like:
Z ::= X;;
Y ::= 1;;
WHILE ~(Z = 0) DO
Y ::= Y * Z;;
Z ::= Z - 1
Which should be somewhat easily understood as ...
If we agree that the purpose of analyses is to both prove properties and help users of smart contracts to understand them, I would say:
Values: studying what values each element of the storage can take in the future.
Effects: studying what effects can occur in the future: typically what transfers can occur and on what conditions.
Ownership: who can trigger ...
How to check the proof
Currently, the only way to check the proof is to install and run the Coq proof assistant on the manager.tz file. This is automated in the continuous integration script of the Mi-Cho-Coq project so you can see it here.
In the future, we plan to use JsCoq to run Mi-Cho-Coq proofs from web browsers.
What is proved
The family of ...
If it's a tz1 account (or the manager key of a KT1 account), the simplest is to sign a message and provide the public key. This can be done in command line in the following way:
./tezos-client hash data '"This key belongs to Caleb"' of type string
This will give you a serialization of the data
you can then run
./tezos-client sign ...
@ArthurB please correct me if I said anything silly :)
Nondeterminism: two bakers won't produce the same block
The baking process is not deterministic. Among other things, if several people bake independently, the list of transactions included in the block will not be the same (e.g. one might include a transaction that the other never heard about, due to ...