Help understanding git checkout behavior

Hello,

We are master students at University of Minho in Portugal and we are currently working on a project suggested by CSAIL (MIT), called "Understanding Git with Alloy". The project consists in modeling git using alloy and then check for some properties that git does (not) guarantee.

The project was going pretty fine, till we start modeling the checkout operation. We are with some problems finding useful information about the properties that have to be satisfied when the "git checkout" is performed. We have concluded that if everything that is on index is commited then we have no problems making checkout. The problem is when we have something on index that is not updated with the last commit. We cannot find a general property that says when checkout can be performed. We have even found some files that are lost, like in this case:

smooke  teste $ git init
Initialized empty Git repository in /home/smooke/Dropbox/teste/.git/
smooke  teste $ touch f
smooke  teste $ echo a > f
smooke  teste $ git add f
smooke  teste $ git commit -m 'first commit'
[master (root-commit) dab04b9] first commit
 1 files changed, 1 insertions(+), 0 deletions(-)
 create mode 100644 f
smooke  teste $ git branch b
smooke  teste $ touch something
smooke  teste $ echo b > something
smooke  teste $ git add something
smooke  teste $ git commit -m 'something added'
[master 9f2b8ad] something added
 1 files changed, 1 insertions(+), 0 deletions(-)
 create mode 100644 something
smooke  teste $ git rm something
rm 'something'
smooke  teste $ mkdir something
smooke  teste $ cd something/
smooke  something $ touch f1
smooke  something $ echo c > f1
smooke  something $ cd ..
smooke  teste $ git add something/f1
smooke  teste $ git checkout b
Switched to branch 'b'
smooke  teste $ ls
f
smooke  teste $ git checkout master
Switched to branch 'master'
smooke  teste $ ls
f  something
smooke  teste $ cat something
b

We are not sure if this behavior has an explanation of if it is just a bug.

We are hoping that you could clarify us about this operation or recommend us some place where we can find some useful information about this...

Thank you in advance, Best regards,

Cláudio and Renato