Encoding and verifying network intents for stateful networks

A computing device comprising at least:

• a memory;
• a processor executing instructions in the memory to:
• identify three causal precedent relationships about a network function in an intent-based stateful network,
• wherein a first causal precedent relationship indicates that the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded,
• wherein a second causal precedent relationship indicates that an established state in the network function implies that at least one previous network packet was received at the network function,
• wherein a third causal precedent relationship indicates that the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function;
• encode the network function using a combination of at least one of the three identified relationships;
• and
• verify a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.

A non-transitory machine-readable storage medium encoded with instructions executable by a processor of a computing device, the non-transitory machine-readable storage medium comprising instructions to:

• identify three causal precedent relationships about a network function in an intent-based stateful network,
• wherein a first causal precedent relationship indicates that the network function forwarding a network packet implies that at least one previous network packet was received by the network function in the same direction prior to the network packet is forwarded,
• wherein a second causal precedent relationship indicates that an established state in the network function implies that at least one previous network packet was received at the network function,
• wherein a third causal precedent relationship indicates that the network function receiving the network packet as a downward network function implies the network packet was previously sent by a second network function acting as an upward network function;
• encode the network function using a combination of at least one of the three identified relationships;
• and
• verify a plurality of network intents in the intent-based stateful network based at least in part on the encoding of the network function.