Document `work`'s algorithm by pgiarrusso-sl · Pull Request #17 · SkyLabsAI/auto-docs

pgiarrusso-sl · 2026-05-08T12:56:50Z

Begin writing our internal manual.

Over #16.

Fix https://github.com/SkyLabsAI/agent-foundation/issues/35.

skylabs-ai-ci · 2026-05-08T13:04:49Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/auto-docs/	paolo/doc-work-2	097eb86	paolo/doc-work ( ⚠️ non-default)	684e410	#17

Passive Repos

Repo	Job Branch	Job Commit
./	main	b9f28b5
fmdeps/BRiCk/	main	d94485e
fmdeps/auto/	main	63d5e05
bluerock/NOVA/	skylabs-proof	6cbef03
bluerock/bhv/	skylabs-main	448828c
fmdeps/brick-libcpp/	main	2014908
fmdeps/ci/	main	680889d
vendored/elpi/	skylabs-master	aa4475f
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	fb160a9
psi/protos/	main	8fe3e7c
psi/backend/	main	0b5fea6
psi/ide/	main	6b596cf
psi/data/	main	76acc2f
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	ac7e4ec
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	e8b88a7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.00%	125439.4	125439.5	+0.0	total
+0.00%	22788.6	22788.6	+0.0	├ translation units
+0.00%	102650.9	102650.9	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	125439.4	125439.5	+0.0	total
+0.00%	22788.6	22788.6	+0.0	├ translation units
+0.00%	102650.9	102650.9	+0.0	└ proofs and tests

pgiarrusso-sl · 2026-05-13T15:13:53Z

+
+## Iris goals
+
+`sep` works on Iris goals `Γ ; Γp ; Γs ⊢ Q`, where `Γ` is the Rocq context,


Needed: show how Γ ; Γp ; Γs ⊢ Q actually looks in Rocq.

Possible: use actual goals instead of this notation. (But they seem unwieldy).

Janno · 2026-05-13T15:09:58Z

+2. then apply forward and backward hints to simplify assumptions and
+conclusions, as far as possible
+3. then apply learning hints to instantiate any existentials as far as possible
+4. if enabled, instantiate any remaining existential quantifiers with evars


This needs to be at the very end; ework will only do that if there is nothing else it can do.

Janno · 2026-05-13T15:12:05Z

+4. if enabled, instantiate any remaining existential quantifiers with evars
+5. apply introduction rules for joint conjunctions
+<!-- when? this seems the most reasonable point -->
+6. then apply framing/identity cancellation, and cancellation hints as far as possible


Identity cancellation is at a fixed cost (hopefully higher than most hints users write). Is this list the wrong place to announce that priorities/costs matter?

Janno · 2026-05-13T15:15:03Z

+
+## Iris goals
+
+`sep` works on Iris goals `Γ ; Γp ; Γs ⊢ Q`, where `Γ` is the Rocq context,


sep technically also works on plain bi entailments; not sure if this is relevant here (and you do not claim that it doesn't)

Janno · 2026-05-13T15:16:06Z

+Iris assumptions can be named or anonymous; by default `sep` will preserve named
+assumptions unchanged, but `$usenamed=true` will override this behavior.
+
+`sep` will eliminate separating conjunctions in assumptions.


Also existentials. And conjunctions in the intuitionistic context. And separation conjunctions in the intuitionistic context if the bi is positive.

Another thing to mention somewhere around here: sep bubbles up existentials to the top of the conclusion (but will not treat this as progress, i.e. the bubbling up is not committed unless actual progress is made in another fashion)

pgiarrusso-sl · 2026-05-15T14:59:52Z

+`sep` simplifies or solves separation logic entailments `P ⊢ Q` via builtin
+proof rules and user-defined Rocq hints.
+
+1. apply introduction rules for universals and wands


Suggested change

1. apply introduction rules for universals and wands

The core algorithm repeats these steps:

1. apply introduction rules for universals and wands

pgiarrusso-sl · 2026-05-15T15:00:49Z

+conclusions, as far as possible
+3. then apply learning hints to instantiate any existentials as far as possible
+4. if enabled, instantiate any remaining existential quantifiers with evars
+5. apply introduction rules for joint conjunctions


Gregory asked what this means, I answered iSplit — maybe

Suggested change

5. apply introduction rules for joint conjunctions

5. apply introduction rules for joint conjunctions (like `iSplit`)

pgiarrusso-sl · 2026-05-15T15:01:36Z

+
+1. apply introduction rules for universals and wands
+2. then apply forward and backward hints to simplify assumptions and
+conclusions, as far as possible


Suggested change

conclusions, as far as possible

conclusions, as far as possible; hints are applied in order

pgiarrusso-sl · 2026-05-15T15:05:50Z

+`sep` works on Iris goals `Γ ; Γp ; Γs ⊢ Q`, where `Γ` is the Rocq context,
+`Γp` is the intuitionistic context, `Γs` is the spatial context, and `Q` is the
+conclusion.
+In an Iris goal, assumptions in `Γp` can be duplicated or discarded


Pull this section out into a separate section on "Iris goals" .

Also explain difference between pure and Iris assertions. (Is that a separate section).

also point out the existence of evars. (But users know them, and maybe the user of evars is an extension since we avoid ego).

gmalecha-at-skylabs · 2026-05-15T15:08:14Z

+## Iris goals
+
+`sep` works on Iris goals `Γ ; Γp ; Γs ⊢ Q`, where `Γ` is the Rocq context,
+`Γp` is the intuitionistic context, `Γs` is the spatial context, and `Q` is the
+conclusion.
+In an Iris goal, assumptions in `Γp` can be duplicated or discarded
+freely, unlike assumptions in `Γs`.


I would propose moving this out to a separate page.

pgiarrusso-sl · 2026-05-15T15:13:19Z

+freely, unlike assumptions in `Γs`.
+
+Iris assumptions can be named or anonymous; by default `sep` will preserve named
+assumptions unchanged, but `$usenamed=true` will override this behavior.


"Idiomatic IPM proofs name hypotheses, but idiomatic work proofs do not, and we prefer avoiding splitting the context".

See also next section, but we don't just avoid iSplitL.

we prefer to never split the goal eagerly (usually, work in a single goal) — avoid splitting context with iSplitL — avoid splitting context with iApply with multiple premises. "We avoid doing frame inference"...

idiomatically we avoid name management for assumptions

avoid introducing existentials

pgiarrusso-sl · 2026-05-15T15:44:43Z

+`sep` simplifies or solves separation logic entailments `P ⊢ Q` via builtin
+proof rules and user-defined Rocq hints.
+
+1. apply introduction rules for universals and wands


(Need to add mentions of naming policies).

gmalecha-at-skylabs · 2026-05-15T15:49:03Z

+Instead, we can cancel spatial assumptions against conclusion conjuncts using
+the following cancellation rule:
+```
+P1 ⊢~ P2              Γ ; Γp ; Γs ⊢ Q
+-------------------------------------- CANCEL
+Γ ; Γp ; P1, Γs ⊢ P2 ∗ Q
+```


Suggested change

Instead, we can cancel spatial assumptions against conclusion conjuncts using

the following cancellation rule:

```

P1 ⊢~ P2 Γ ; Γp ; Γs ⊢ Q

-------------------------------------- CANCEL

Γ ; Γp ; P1, Γs ⊢ P2 ∗ Q

```

The core automation applies "rules" eagerly based on priorities.

Instead, we can cancel spatial assumptions against conclusion conjuncts using

the following cancellation rule:

P1 ⊢~ P2 Γ ; Γp ; Γs ⊢ Q
-------------------------------------- CANCEL
Γ ; Γp ; P1, Γs ⊢ P2 ∗ Q

bwd.md

Applying a BWD rules replace a (separation) conjunction in the goal with another:

Definition my_hint := \bwd \proving A \through B \end. Next Obligation. .. Qed.

When applying this rule on a goal of the form

... ---------------* exists a b c, A ** X ** ...

will result in a goal of the form

... --------------* exists a b c, B ** X ** ...

add this to the bwd.md from auto-docs.

pgiarrusso-sl · 2026-05-15T15:52:13Z

+proof rules and user-defined Rocq hints.
+
+1. apply introduction rules for universals and wands
+2. then apply forward and backward hints to simplify assumptions and


Are the priorities for \bwd and \fwd different?

We're confused about an hint like this, but I plan to not explain it — but figure it out so the explanation isn't false.

#[program] Definition type_ptrR_to_type_ptr_FB p ty := \fwd \proving p |-> type_ptrR ty (* spatial conclusion to match *) \through type_ptr ty p (* replacement spatial conclusion *) \end.

pgiarrusso-sl · 2026-05-15T15:57:45Z

+Instead, we can cancel spatial assumptions against conclusion conjuncts using
+the following cancellation rule:
+```
+P1 ⊢~ P2              Γ ; Γp ; Γs ⊢ Q


Probably go back to identity cancellation here.

Gregory suggests leaving the "other steps" (the hints) to other documents (about bwd/fwd etc), so we don't need to talk much about the generalization here.

pgiarrusso-sl · 2026-05-15T16:24:33Z

+5. apply introduction rules for joint conjunctions
+<!-- when? this seems the most reasonable point -->
+6. then apply framing/identity cancellation, and cancellation hints as far as possible
+7. restart from 1


Maybe talk about priorities rather than bwd/fwd as a separate step?

The actual implementation has separate phases — but this should not matter because hints should be "confluent" — concretely,

~~idiomatic cancelx hints will introduce terms in "bwd/fwd normal form"~~ not possible, because normal forms are not preserved by instantiating hint metavariables

idiomatic cancelx hints should only be triggered on conjuncts in normal forms — which is easier, so if you introduce a non-normal form (and phase ordering questions apply) no cancelx hints will apply on it, so that'll be processed by the next bwd phase. This way, phases aren't exposed to the user.

also, bwd/fwd hints shouldn't be "orphans" morally

skylabs-ai-ci · 2026-05-19T16:56:24Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/auto-docs/	paolo/doc-work-2	626c2e8	paolo/doc-work ( ⚠️ non-default)	684e410	#17

Passive Repos

Repo	Job Branch	Job Commit
./	main	7d2ee30
fmdeps/BRiCk/	main	f029bba
fmdeps/auto/	main	020df41
bluerock/NOVA/	skylabs-proof	dc3d314
bluerock/bhv/	skylabs-main	c46f5e3
fmdeps/brick-libcpp/	main	2014908
fmdeps/ci/	main	9e6e574
vendored/elpi/	skylabs-master	aa4475f
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	e5188db
psi/protos/	main	8fe3e7c
psi/backend/	main	0b5fea6
psi/ide/	main	6b596cf
psi/data/	main	82cb305
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	ac7e4ec
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	e8b88a7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.00%	126419.2	126419.2	+0.0	total
+0.00%	22690.6	22690.6	+0.0	├ translation units
+0.00%	103728.6	103728.6	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	126419.2	126419.2	+0.0	total
+0.00%	22690.6	22690.6	+0.0	├ translation units
+0.00%	103728.6	103728.6	+0.0	└ proofs and tests

Begin writing our internal manual

8bd7e04

pgiarrusso-sl requested a review from Janno May 13, 2026 15:07

pgiarrusso-sl commented May 13, 2026

View reviewed changes

Janno reviewed May 13, 2026

View reviewed changes

pgiarrusso-sl commented May 15, 2026

View reviewed changes

gmalecha-at-skylabs reviewed May 15, 2026

View reviewed changes

pgiarrusso-sl commented May 15, 2026

View reviewed changes

gmalecha-at-skylabs reviewed May 15, 2026

View reviewed changes

pgiarrusso-sl commented May 15, 2026

View reviewed changes

pgiarrusso-sl added 4 commits May 19, 2026 05:18

Old wip

048501f

Move away doc V1

167cce5

Add completed doc on Iris goals

ec4270c

Address comments

f5f2b69


		## Iris goals

		`sep` works on Iris goals `Γ ; Γp ; Γs ⊢ Q`, where `Γ` is the Rocq context,

	1. apply introduction rules for universals and wands
	The core algorithm repeats these steps:
	1. apply introduction rules for universals and wands

	5. apply introduction rules for joint conjunctions
	5. apply introduction rules for joint conjunctions (like `iSplit`)

	conclusions, as far as possible
	conclusions, as far as possible; hints are applied in order

Conversation

pgiarrusso-sl commented May 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

skylabs-ai-ci Bot commented May 8, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

pgiarrusso-sl May 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pgiarrusso-sl May 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pgiarrusso-sl May 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

skylabs-ai-ci Bot commented May 19, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

pgiarrusso-sl commented May 8, 2026 •

edited

Loading

pgiarrusso-sl May 13, 2026 •

edited

Loading

pgiarrusso-sl May 15, 2026 •

edited

Loading

pgiarrusso-sl May 15, 2026 •

edited

Loading