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 ...
Program verification is recognised as crucial in the Tezos community since the very beginning of the Tezos project. It is mentioned in the position and white papers and many teams work on this topic. Smart contract verification in particular is a key aspect in the design of the Tezos smart contract languages (Michelson and the various high-level languages).
For implicit accounts, the address is nothing more than the hash of the public key so this means that you can compute the address from the public key but not the other way around.
In Michelson, you have:
HASH_KEY : key -> key_hash
IMPLICIT_ACCOUNT : key_hash -> contract unit
ADDRESS : contract _ -> address
I don't understand how I would apply this ...