How file reading operations are modeled in the ACL2 logic.
ACL2's io operations are available in
Practically speaking, most users don't need to pay any attention to the details of this story. Instead, they can just include the std/io library, which develops the basic theorems that are necessary to reason about the io primitives.
But if for some reason, you do want to understand the logical story, you might start with this paper:
Jared Davis. Reasoning about ACL2 File Input. ACL2 Workshop 2006.