I’ve been doing a lot of Alloy modeling for practical applications. I’m also looking into stuff to model just for fun/learning. I think I found some educational opportunities.
Keep posting! There’s not enough “real world” Alloy, every little bit helps.
I hope you continue this series. 1) git is a totally baroque system that I myself am constantly eluded by. 2) models help to understand such systems, and I’m always amazed how terse Alloy models can be.
From my forgotten Git internals knowledge, which is very sparse, I remember that the hashes can come from a textual representation, i.e., a tree is a file with a list of blobs, and the tree’s hash is the hash of the file, as any other object in Git.
Given that, is it possible to have two trees with different hashes and the same objects?
Yes, it’s possible. You’d need to get a SHA-1 hash collision. I linked to someone who did that in the post; they changed the git code to only take the first byte of the hash to see what happened (segfault)
See also: ValidAlloy: A tool for validating a git alloy specification using testcase generation. It is an impressive work where model refined using real testcases for real Git implementation.
Oh wow! Thank you for sharing this. I’m gonna have to read it carefully
Seems to me that modeling git internals is a really clever pedagogical choice here! Appreciate the post. Look forward to part 2.
Nice start to the series.
I’ve been doing a lot of Alloy modeling for practical applications. I’m also looking into stuff to model just for fun/learning. I think I found some educational opportunities.
Keep posting! There’s not enough “real world” Alloy, every little bit helps.
The graph or dag module contains an implementation of the tree predicate, which I started using instead of constraining the parent relation directly
in Alloy, you mean? Does it have any side effects? (Like opening ordered on some sig making it fixed-size?)
Nope! You can check it manually under
open sample models > utils.I hope you continue this series. 1) git is a totally baroque system that I myself am constantly eluded by. 2) models help to understand such systems, and I’m always amazed how terse Alloy models can be.
I plan to continue! I’ve already got a second part drafted getting to commits!
From my forgotten Git internals knowledge, which is very sparse, I remember that the hashes can come from a textual representation, i.e., a tree is a file with a list of blobs, and the tree’s hash is the hash of the file, as any other object in Git.
Given that, is it possible to have two trees with different hashes and the same objects?
From a blog post by Mike Street:
So, as a trivial case, amending a commit message changes the hash, without changing any of the files.
Yes, it’s possible. You’d need to get a SHA-1 hash collision. I linked to someone who did that in the post; they changed the git code to only take the first byte of the hash to see what happened (segfault)