Repository navigation
Pathname's instance surface is the CRuby name table, not a blanket method_missing (fixes #147) - #149
Open
jiro-by-nori[bot] wants to merge 3 commits into
Open
jiro-by-nori[bot] wants to merge 3 commits into
jiro-by-nori[bot] wants to merge 3 commits into
Conversation
… their ids (issue #53) `Books/FastPower/Proof.lean` named the `Power` instance and the address of the result Array by the literals `114`/`115`. A bootstrap class or a boot fixture object moves every id the program allocates, and the stale id then names a different object without failing where it is written: both sides of each `kernel_rfl` stub reduce to the same wrong machine, so the break shows up as a type mismatch at `setup`/`fast_power_correct` and costs a scavenger hunt per additive boot change. The ids are now read off the machine by the invariant that makes them that object: `powerIdOf` finds the only object carrying both `@base` and `@steps`, and `resultIdOf` is the last object of the heap at `final`, which is the Array the program answers with. `#guard`s pin both invariants at build time, so a second matching object or an extra allocation between the loop head and `final` fails at the definition rather than somewhere below. Proof-only: the model, the prelude and the kernel are untouched. Co-authored-by: Nori <contact@tilework.tech>
…thod_missing (issue #147) A Pathname instance answers every unmodeled selector with a named `Unsupported`, including selectors no Ruby defines, because the prelude's `Pathname` carried a blanket `method_missing` and a `respond_to_missing?` that answered `true` for anything. An invented name therefore looked like an honest gap instead of the `NoMethodError` CRuby raises, and a real unmodeled one (`realpath`, `stat`, ...) lost its own name behind one generic reason. `Pathname` is a prelude class but it ships with every CRuby, so its surface is now generated like a builtin's: `scripts/gen_cruby_names.rb` emits Pathname's instance selectors, singleton methods and constants into `crubyMethodNames` / `crubySingletonNames` / `crubyNamespaceConstants`, and the prelude's `method_missing`/`respond_to_missing?` are deleted. A miss is then an ordinary lookup miss: a real unmodeled method declines as `unmodeled method Pathname#realpath`, an invented one raises CRuby's byte-exact `NoMethodError`, and `respond_to?` answers from the same tables. `Pathname#path` is protected in CRuby, so it is modeled as a protected method: `p.path` raises the protected-method `NoMethodError` and `p.send(:path)` answers. The prelude's `include Comparable` is removed for the same reason: CRuby's Pathname is not Comparable, so `<`, `>` and `between?` on one are `NoMethodError` rather than answers. The checker's copied `nativeInstanceNames` projection grows to keep `instance_covered` true (the conservative direction: more selectors it refuses) and `nativeQueryRows` records Pathname's own `===`/`to_s`. `instance_covered` now needs `maxRecDepth 4000` to walk the larger list. Stacked on #136: the prelude change shifts the boot heap, which the FastPower proof pinned object ids against (issue #53). Co-authored-by: Nori <contact@tilework.tech>
`pathname.so` is booted with the interpreter, but the stdlib's `pathname.rb` reopens the class with `find`, `rmtree` and `Pathname.mktmpdir`. A program that has required pathname can call them, so the snapshot must contain them: without the require the model answered `NoMethodError` for a method CRuby runs. With them the model declines by name (`unmodeled method Pathname#find`), which is honest in both states — a gate where CRuby has nothing is sound, a `NoMethodError` where CRuby has a method is not. The checker's copied projection gains `rmtree`, so `instance_covered` holds. The generator header and the table docstrings said the tables cover the model's *bootstrap* classes; say what they cover now — every class of the model, the prelude's included — and list Pathname in FOLD beside the other class CRuby ships as part of its own stdlib. `docs/testing.md` names the size of the regression corpus, which the new case grows by one. Co-authored-by: Nori <contact@tilework.tech>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pathnameinstances answer every unmodeled selector with a namedUnsupported— including selectors no Ruby defines — because the prelude carries a blanketmethod_missingplus arespond_to_missing?that answerstruefor anything. An invented name therefore looked like an honest gap instead of theNoMethodErrorCRuby raises, a real unmodeled method (realpath,stat, …) lost its own name behind one generic reason, andrespond_to?was a wrong value. This is the instance-side twin of #29 (class side, PR #146) and the sibling of #27 (File/IOinstance methods, fixed in #28).Fixes #147.
What changes
Pathnameis a prelude class, but CRuby ships it as part of the language, so its surface is now generated like a builtin's:scripts/gen_cruby_names.rblistsPathnameinFOLD, socrubyMethodNames,crubySingletonNamesandcrubyNamespaceConstantscarry its real selectors. It alsoloadspathname.rb: the bootedpathname.soanswersrequire "pathname", so a plain require would be a no-op and the snapshot would miss the methods the.rbhalf adds (find,rmtree,Pathname.mktmpdir). Those are real methods a program that required pathname can call, so they must gate, not raise.prelude/prelude.rb:method_missingandrespond_to_missing?are deleted; a miss is an ordinary lookup miss anddispatchMissclassifies it (a real name declines asunmodeled method Pathname#…, an invented one raises CRuby's byte-exactNoMethodError).Pathname#pathis protected in CRuby, so it is modeled as protected:p.pathraises the protected-methodNoMethodError,p.send(:path)answers.include Comparableis removed: CRuby'sPathnameis notComparable, so<,>andbetween?areNoMethodErrorrather than answers.nativeInstanceNamesgains the Pathname selectors,nativeQueryRowsgainsPathname's===/to_s(required byquery_covered), andinstance_coveredneedsmaxRecDepth 4000to walk the larger list.difftest/corpus/regressions/pathname-instance-surfacepins the whole surface;docs/testing.md's reproducer count goes 219 → 224 (it was already stale by four).Behaviour, model vs CRuby 4.0.5
bin/ruby-lean --comparereportsAGREEon that program. Real unmodeled selectors now decline by name — verified for 38 of them (realpath,stat,lstat,children,each_child,readlink,chmod,mkdir,rmdir,delete,unlink,rename,expand_path,relative_path_from,cleanpath,absolute?,relative?,root?,parent,sub_ext,entries,find,rmtree,size,read,write,open,each_line,atime,ctime,mtime,birthtime,utime,world_readable?,zero?,split,fnmatch?,ascend,descend,each_filename), each answeringunmodeled method Pathname#<name>. Without thepathname.rbload,findandrmtreeraisedNoMethodErrorfor methods CRuby has.Test plan
Also
bin/ruby-lean --compareon the program above (agrees) and per-selector probes for the 38 unmodeled names and the invented one.Notes for review
FastPowerpinned heap object ids), included verbatim because this prelude change shifts the boot heap. Drop it when rebasing if Locate FastPower's Power instance and result Array instead of pinning their ids (fixes #53) #136 has landed first.File/Dir/Pathnamemethod gates, an invented one is aNoMethodError#146 fixes the same defect for the class side and touches the same generated tables; whichever lands second needsmake genregenerated, which is mechanical.Pathname#empty?still answersString#empty?instead of asking the filesystem; that is Pathname#empty? answers String#empty? instead of asking the filesystem, so it is a wrong answer #91 (PR Pathname#empty? asks the filesystem, not the path String (fixes #91) #92), deliberately untouched here.