  Intermittently powered energy-harvesting devices enable new applications in
inaccessible environments. Program executions must be robust to unpredictable
power failures, introducing new challenges in programmability and correctness.
One hard problem is that input operations have implicit constraints, embedded
in the behavior of continuously powered executions, on when input values can be
collected and used. This paper aims to develop a formal framework for enforcing
these constraints. We identify two key properties -- freshness (i.e., uses of
inputs must satisfy the same time constraints as in continuous executions) and
temporal consistency (i.e., the collection of a set of inputs must satisfy the
same time constraints as in continuous executions). We formalize these
properties and show that they can be enforced using atomic regions. We develop
Ocelot, an LLVM-based analysis and transformation tool targeting Rust, to
enforce these properties automatically. Ocelot provides the programmer with
annotations to express these constraints and infers atomic region placement in
a program to satisfy them. We then formalize Ocelot's design and show that
Ocelot generates correct programs with little performance cost or code changes.
