Reclaim requires both durability acknowledgements. A poisoned sink cannot
be retried by appending behind its possibly partial tail. Recovery owns a
new admitted sink/frontier; this primitive never silently discards a batch.
76def publicationReclaimAdmission =
77 (lambda unrestricted version : Nat .
78 (lambda unrestricted writeFull : Nat .
79 (lambda unrestricted fileSynced : Nat .
80 (lambda unrestricted directorySynced : Nat .
81 (lambda unrestricted poisoned : Nat .
82 (aosChoose
83 Nat
84 (naturalAnd
85 (naturalEqual version 1)
86 (naturalAnd
87 (naturalLessOrEqual writeFull 1)
88 (naturalAnd
89 (naturalLessOrEqual fileSynced 1)
90 (naturalAnd
91 (naturalLessOrEqual directorySynced 1)
92 (naturalLessOrEqual poisoned 1)))))
93 (aosChoose
94 Nat
95 poisoned
96 6
97 (aosChoose
98 Nat
99 writeFull
100 (aosChoose Nat (naturalAnd fileSynced directorySynced) 0 3)
101 2))
102 4))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.