Activity
refactor: rename TrafficManager to ReplicationEngine.
refactor: rename TrafficManager to ReplicationEngine.
fix: fix a bug in GenLoc.
fix: fix a bug in GenLoc.
feat: add SubQueue relation and related lemmas.
feat: add SubQueue relation and related lemmas.
feat: change the definition of concat_queue and related proofs.
feat: change the definition of concat_queue and related proofs.
feat: add one lemma and clear_AList_tags and forallb.
feat: add one lemma and clear_AList_tags and forallb.
feat: more lemmas about queue.
feat: more lemmas about queue.
refactor: using rev' from Coq stdlib instead of self-defined.
refactor: using rev' from Coq stdlib instead of self-defined.
Change the result type of qlength to Z.
Change the result type of qlength to Z.
More lemmas about queue.
More lemmas about queue.
Update AListUtil.v
Update AListUtil.v
simplified gcl compiler
simplified gcl compiler
Prove lemmas about output of tm.
Prove lemmas about output of tm.
Add a lemma about AList.get and kv_map.
Add a lemma about AList.get and kv_map.
Update Queue.v
Update Queue.v
Improve queue and tm.
Improve queue and tm.
Update P4Arith.v
Update P4Arith.v
statements done
statements done
Add lemmas about kv_map.
Add lemmas about kv_map.
Change the definition of Queue.
Change the definition of Queue.
Deleted branch
anonym inst
anonym inst