Definitive guide to understanding how to formulate an IPv6 address

For fun, I'd like to better understand the building blocks or elements that are within an IPv6 address.

Here are the basics, from my understanding:

IPv6 addresses are 128 bits long (written as 8 blocks, each with 16 bits)
Each block is encoded as hex digits between 0 and 0xffff. Leading zeroes may be omitted.
One can append an IPv4 doted-quad address, and it will occupy the lower 32 bits of the IPv6 address. 1:2:3:4:5:6:200.201.202.203. (The rules for the IPv4 are as expected.)
The IPv4 representation can only appear at the end.
It is possible to use double colons syntax to represent one or more blocks with zeroes. 1:2::7:8 is equivalent to 1:2:0:0:0:0:7:8.
Each IPv6 address may only have one double colon within it, otherwise it is syntactically wrong.
Double colon may appear at the beginning, middle or end of an ip6, but not within an IPv4 dotted-quad address.

Are all the above points correct?

Please don't tell me to read the RFC. There are several about this matter, and none actually comes with a few simple examples to describe the various encoding mechanisms. I'm sure many would appreciate a simple list with examples.

Online testing tool The closest online tool to help is http://www.dominicsayers.com/source/beta/is_email/test/ but the messages are confusing and it does not actually say in plain English what is right and wrong and why. It's also actually built for emails which of course may contain IPv6 addresses, so its not exactly ideal.

Solution

In general, yes, your points are correct.

Are you sure you read the RFC? RFC 3513, section 2.2 has exactly what you are asking for. It's very well written, for an RFC. =) I can't help but point this out since it may be very helpful to future people reading this question.