Skip to content

Hold 0039's page, its derived fourth number and its unpaged read - #253

Open
iderex wants to merge 1 commit into
mainfrom
the-page-the-total-and-the-unpaged-read-39
Open

Hold 0039's page, its derived fourth number and its unpaged read#253
iderex wants to merge 1 commit into
mainfrom
the-page-the-total-and-the-unpaged-read-39

Conversation

@iderex

@iderex iderex commented Aug 30, 2026

Copy link
Copy Markdown
Contributor

The issue this belongs to

#39. It stays open, and the last section says which of its three conditions this reaches, which is none of them.

What changed

src/server/library.rs holds the part of docs/decisions/0039-the-page-the-item-and-what-next-up-is-not.md that a list and a count settle: the offset and the count a paged read is asked for by, the three numbers an answer carries, whether another page exists derived from those three rather than stored beside them, and which of the four library reads 0010's capability table carries takes a page request at all.

git rev-parse origin/the-page-the-total-and-the-unpaged-read-39
449f15c88587a6c2022cd2300d592035ab96a309

git show origin/the-page-the-total-and-the-unpaged-read-39:src/server/library.rs | grep -n '^pub const \|^pub struct \|^pub enum '
68:pub const THE_TOTAL_IS_ALWAYS_ASKED_FOR: bool = true;
79:pub struct PageRequest {
113:pub enum WhatTheReadAnswers {
133:pub enum LibraryRead {
183:pub enum NotAPagedRead {
195:pub enum WhatAskingForAPageDid {
218:pub struct Page<I> {

The QueryResult name in src/server/mod.rs was this record's placeholder, documented in its own doc comment as being #39's to decide, and it is replaced by library::Page rather than left beside it. Two names for one answer is the drift a shared core exists to remove, and a placeholder that survives the issue it was waiting for is the first thing a client author reaches for.

The three other files are the module being registered the way every previous landing registers one: the crate's thread assertions in src/lib.rs, the same statements asked from outside the crate in tests/thread_statements.rs, and the line in .github/coverage/pinned-surface that src/server/ being an area requires of every tracked file under it.

The means is the one this tree already carries, which is the check ## Choosing the means asks for. What decided it here rather than habit is that the record's whole subject is arithmetic over three numbers a server sent. A means in which the derivation could not be refused by a test that deletes it would be recording the rule rather than holding it, and the three runs below are what that buys.

What failure it prevents

A paging loop that stops after one screenful. Both paged routes take a flag that turns counting off, it defaults to on, and with it off the server builds the answer with no total and the constructor fills the field in from the page's own length. The number then arrives in the same field, with the same type, as a real total, and a caller paging until the offset plus the page length reaches the total shows a library with one screenful in it while nothing anywhere reports an error. 0039 fixes that the core never sends the flag; THE_TOTAL_IS_ALWAYS_ASKED_FOR is where that is written down rather than being a default nobody chose.

A fourth field that can disagree with the three it came from. Whether there is another page is derived from the offset, the number of items returned and the total, every time it is asked. The offset the next page begins at is derived from the same three, so it moves by what came back rather than by what was asked for - the same number on every page a server answers in full, and different on the first one it does not.

A request for the second hundred views answered with the first hundred. GET /UserViews takes neither an offset nor a count on either supported line, so a page request carried that far would send nothing extra on the wire and the first answer would come back as though it were the page that was asked for. The caller cannot tell a request that was not sent from one that was answered in full. It is refused where it is made instead.

Evidence

The module's own cases, at the commit above:

cargo test --locked --lib server::library
test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 396 filtered out; finished in 0.00s

The whole suite, which is one of the two commands the README names:

cargo test --locked
test result: ok. 405 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s
test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.20s
test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 28 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.20s
test result: ok. 90 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s

The other one:

cargo build --locked --all-targets
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 3.76s

The formatter and the analyser, under the settings the two checks run:

cargo fmt --check ; echo "exit=$?"
exit=0

cargo clippy --all-targets -- -D warnings -D clippy::all -D clippy::pedantic -D clippy::cargo
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 3.67s

The invariants leg, over its own rules and the tracked set:

bash .github/invariants/invariants.sh check | tail -1
Every rule above was applied to its subject and refused nothing.

The document check, which is what the new register line and the new module path are read by:

bash .github/doc-paths/doc-paths.sh check | tail -1
Every path these documents name resolves against the tracked set.

The size of the change:

git diff --shortstat origin/main...origin/the-page-the-total-and-the-unpaged-read-39
 5 files changed, 524 insertions(+), 16 deletions(-)

What a guard here refuses, and the proof it bites

Three guards, each watched failing on the version of the mistake it is against, and each restored afterwards. Every run below is cargo test --locked --lib server::library, and the green run of the same command with no violation in the tree is the first block under Evidence.

Another page is derived at the boundary and not one past it. The violation is the off-by-one somebody writes when they read the total as the index of the last item:

-        self.offset + self.items.len() < self.total
+        self.offset + self.items.len() <= self.total

thread 'server::library::tests::another_page_is_derived_from_the_three_at_the_boundary' panicked at src\server\library.rs:358:9:
assertion failed: !Page::from_server(0, 100, items(100)).has_another_page()
thread 'server::library::tests::the_unpaged_read_is_one_page_holding_everything' panicked at src\server\library.rs:416:9:
assertion failed: !views.has_another_page()
test result: FAILED. 5 passed; 4 failed; 0 ignored; 0 measured; 396 filtered out; finished in 0.00s

A page request against a read that takes no paging parameters is refused and not carried. The violation is the surface that sends it anyway, which is what this looks like when somebody treats the refusal as decoration:

-            WhatTheReadAnswers::OnePageHoldingEverything => {
-                WhatAskingForAPageDid::RefusedIt(NotAPagedRead::TheWholeAnswerIsOnePage)
-            }
+            WhatTheReadAnswers::OnePageHoldingEverything => {
+                WhatAskingForAPageDid::SendsIt(request)
+            }

thread 'server::library::tests::asking_an_unpaged_read_for_a_page_is_refused_and_not_dropped' panicked at src\server\library.rs:447:9:
  left: SendsIt(PageRequest { offset: 100, count: 100 })
 right: RefusedIt(TheWholeAnswerIsOnePage)
test result: FAILED. 8 passed; 1 failed; 0 ignored; 0 measured; 396 filtered out; finished in 0.00s

The next offset moves by what came back and not by what was asked for. The violation is the one that is correct on every page a full server answers, which is why it needs a short page to catch it:

-            Some(PageRequest::beginning_at(
-                self.offset + self.items.len(),
-                count,
-            ))
+            Some(PageRequest::beginning_at(self.offset + count, count))

thread 'server::library::tests::a_short_page_moves_the_offset_by_what_came_back' panicked at src\server\library.rs:385:9:
  left: Some(PageRequest { offset: 100, count: 100 })
 right: Some(PageRequest { offset: 40, count: 100 })
test result: FAILED. 8 passed; 1 failed; 0 ignored; 0 measured; 396 filtered out; finished in 0.00s

What this does not cover

None of #39's three conditions. They are a test per call against a recorded fixture, paging proven across a boundary rather than within one page, and one item type across the calls. Each needs a request to have been made and a recording of one to exist. Nothing here makes a request, for the reason src/server/transport.rs gives about itself, and tests/recorded/ holds no recording.

The item's fields are not decided, deliberately. 0039 fixes that every read answers with one item type and says in the same paragraph that which fields a read populates depends on what the core asks for in the server's fields parameter, which belongs with the code that makes the request. So Page carries the item as a parameter. Nothing here makes the third condition true and nothing here can break it, because there is no read to break it with.

Nothing sends the counting flag, so nothing here proves it is never sent as false. THE_TOTAL_IS_ALWAYS_ASKED_FOR is the decision written where the code that will build the query meets it. It is a constant, not a guard: no run in this tree constructs a query, so there is nothing for a check to read.

Next up is refused rather than built, and that refusal is 0039's. The route exists on both server lines and answers with the same type, and it is in none of 0010's capabilities. LibraryRead carries the four reads that table names and no fifth. What is owed instead is either 0010 superseded by a record whose table carries the path, or #39's body saying next up is not in its scope; the second is what the decision on #39 of 2026-08-30 took, and this pull request does not edit that body.

The total is not revalidated and that is on purpose. A page states the server's number and nothing more. A total smaller than the offset plus the items returned is a server contradicting itself, and this module answers "no further page" for it rather than repairing a number it did not produce.

The coverage leg was not measured on the machine this was written on. What is run here is the register's own fixtures, .github/coverage/coverage.sh selftest, which reports every one held. The instrumented run and the bar it applies are the runner's, and the verdict on this change is the one the runner produces.

Nothing was run that could raise a consent prompt on this machine. No target outside the runner's own triple was built here, so the targets leg is the runner's verdict as well.

Who has read it

Nobody other than me. There was no second reader available for it, and the evidence above carries the change in place of one.

`src/server/library.rs` holds the part of
docs/decisions/0039-the-page-the-item-and-what-next-up-is-not.md that a list and
a count settle: the offset and the count a paged read is asked for by, the three
numbers an answer carries, whether another page exists derived from those three,
and which of 0010's four library reads takes a page request at all.

What it prevents.

A paging loop that stops after one screenful. Both paged routes take a flag that
turns counting off, and with it off the server fills the total in from the page
it is returning, in the same field and with the same type as a real total. The
core never sends that flag, and the constant here is where that decision is
written down instead of being a default nobody chose.

A fourth field that can disagree with the three it came from. Whether there is
another page is derived from the offset, the number of items returned and the
total, and the offset of the next page moves by what came back rather than by
what was asked for, which are the same number until the first short page.

A request for the second hundred views answered with the first hundred. The view
route takes neither an offset nor a count on either supported line, so a page
request against it is refused where it is made rather than sent as nothing and
answered as though it had been.

The `QueryResult` name in `src/server/mod.rs` was the placeholder for this
record and is replaced by the page rather than left beside it, because two names
for one answer is the drift a shared core exists to remove.

The means is the one this tree already carries, which is the check
`## Choosing the means` asks for. What decided it here rather than habit is that
the record's whole subject is arithmetic over three numbers a server sent: a
means in which the derivation could not be refused by a test that deletes it
would be recording the rule rather than holding it.

Belongs to #39. Which of its three conditions this reaches is stated in the pull
request body, and it is none of them.

Signed-off-by: Nils Lehnen <30603423+iderex@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant