verify receive one message function

• Add/Modify some typing rules
• Modify the type for message struct to use an array_p
• Add one assumption to the specs for read