Skip to content

Commit f1ef47b

Browse files
claudeclaude
committed
fix(abi): typell Idris package scaffold + 5 errors; proofs do NOT yet compile (honest)
The typell ABI was template-derived code that had never been compiled. This makes it buildable-in-principle and fixes 5 genuine errors, but the proofs are NOT verified -- documented plainly in PROOF-STATUS.adoc (no pretend "PASS"). Scaffold: - normalise namespace to Typell.ABI.* (was inconsistent TYPELL/Typell; Foreign's imports could never resolve) - move files to src/Typell/ABI/ + add typell.ipkg (there was no .ipkg) Types.idr errors fixed: - cSizeOf/cAlignOf matched on (CInt _)/(CSize _) -- type-level functions, not constructors; removed (their Bits32/Bits64 reductions are already handled) - CPtr p _ = Bits (ptrSize p) misused the Data.Bits interface -> Bits64 - added import Decidable.Equality - thisPlatform: %runElab stub -> = Linux (no ElabReflection needed) STILL broken (genuine proof-debt, NOT verified): DecEq for Platform needs Uninhabited (x=y) instances; createHandle has an unsatisfiable So (ptr/=0) obligation; modules 2-6 not yet reached by the checker. See PROOF-STATUS.adoc. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
1 parent c1ff8aa commit f1ef47b

8 files changed

Lines changed: 88 additions & 16 deletions

File tree

‎PROOF-STATUS.adoc‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
= typell — Proof Status (HONEST: ABI proofs do NOT yet compile)
3+
:toc:
4+
5+
[abstract]
6+
*The typell Idris ABI is template-derived code that was never compiled, and it
7+
does NOT type-check.* This PR fixes the package *scaffolding* (so it can be built
8+
at all) and several genuine errors, but the proofs are *not* verified. This is
9+
stated plainly rather than asserted as passing — the opposite of a "✓ PASS"
10+
comment with no build behind it.
11+
12+
== What this PR fixed (scaffolding + 5 real errors)
13+
14+
* *Namespace normalised* to `Typell.ABI.*`. It was inconsistent — `Foreign.idr`
15+
used `Typell.ABI.*` while the other five used `TYPELL.ABI.*` (so `Foreign`'s
16+
imports could never resolve). Finishing the template's "Replace TYPELL" step.
17+
* *Layout + package*: files moved to `src/Typell/ABI/` and a real `typell.ipkg`
18+
added (`sourcedir = "src"`, the six modules, `depends = base, contrib`). There
19+
was no `.ipkg` before, so the package could not be built at all.
20+
* *Types.idr errors fixed (5):*
21+
- `cSizeOf`/`cAlignOf` matched on `(CInt _)`/`(CSize _)`, but those are
22+
type-level *functions* (`Platform -> Type`), not constructors — unmatchable.
23+
Removed; the `Bits32`/`Bits64` clauses they reduce to already cover them.
24+
- `CPtr p _ = Bits (ptrSize p)` misused `Bits` (the `Data.Bits` *interface*,
25+
not a `Nat`-indexed type) → `CPtr p _ = Bits64` (machine word).
26+
- `DecEq` used without `import Decidable.Equality` → added.
27+
- `thisPlatform` was a `%runElab do … pure Linux` stub needing ElabReflection
28+
for no benefit → `thisPlatform = Linux`.
29+
30+
== What is STILL broken (genuine proof-debt — NOT verified)
31+
32+
`idris2 --build typell.ipkg` still fails in module 1/6 (`Types.idr`):
33+
34+
* `decEq` for `Platform`: "Can't find an implementation for `Uninhabited (_ = _)`"
35+
— the decidable-equality instance's negative cases (distinct constructors)
36+
are not provided (derive them, or supply `Uninhabited (Linux = Windows)`-style
37+
instances / `%runElab derive`).
38+
* `createHandle`: "Can't find an implementation for `So (not (… ptr 0))`" — an
39+
unsatisfiable non-null obligation; needs the proof threaded from the caller or
40+
a reformulation.
41+
42+
And modules 2–6 (`Layout`, `Soundness`, `InferenceSoundness`, `LevelMonotonicity`,
43+
`Foreign`) have *not been reached* by the type-checker yet, so their status is
44+
*unknown* — they may carry further errors.
45+
46+
== Honest verdict
47+
48+
typell's ABI is **not** a verified development. `Soundness.idr` (progress /
49+
preservation) and the others contain real intent, but the code does not compile
50+
as written. Making it green is genuine proof work (the `DecEq`/`So` obligations
51+
above + whatever surfaces in modules 2–6), not just scaffolding — flagged here as
52+
the real next step rather than papered over.
53+
54+
Reproduce: `idris2 --build typell.ipkg` (Idris 2; currently fails in `Types.idr`).

src/abi/Foreign.idr renamed to src/Typell/ABI/Foreign.idr

File renamed without changes.

src/abi/InferenceSoundness.idr renamed to src/Typell/ABI/InferenceSoundness.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@
2222
||| @see unify.rs — Robinson unification with occurs check
2323
||| @see infer.rs — Bidirectional type inference
2424

25-
module TYPELL.ABI.InferenceSoundness
25+
module Typell.ABI.InferenceSoundness
2626

27-
import TYPELL.ABI.Soundness
27+
import Typell.ABI.Soundness
2828
import Data.List
2929
import Data.Vect
3030
import Decidable.Equality

src/abi/Layout.idr renamed to src/Typell/ABI/Layout.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88
|||
99
||| @see https://en.wikipedia.org/wiki/Data_structure_alignment
1010

11-
module TYPELL.ABI.Layout
11+
module Typell.ABI.Layout
1212

13-
import TYPELL.ABI.Types
13+
import Typell.ABI.Types
1414
import Data.Vect
1515
import Data.So
1616

src/abi/LevelMonotonicity.idr renamed to src/Typell/ABI/LevelMonotonicity.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@
3030
||| @see ROADMAP.adoc — Level definitions
3131
||| @see check.rs — TypeChecker with level-aware features
3232

33-
module TYPELL.ABI.LevelMonotonicity
33+
module Typell.ABI.LevelMonotonicity
3434

3535
import Data.Nat
3636
import Data.Fin

src/abi/Soundness.idr renamed to src/Typell/ABI/Soundness.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
||| @see infer.rs — Bidirectional type inference
2828
||| @see unify.rs — Robinson unification with occurs check
2929

30-
module TYPELL.ABI.Soundness
30+
module Typell.ABI.Soundness
3131

3232
import Data.Vect
3333
import Data.List

src/abi/Types.idr renamed to src/Typell/ABI/Types.idr

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,12 @@
1010
|||
1111
||| @see https://idris2.readthedocs.io for Idris2 documentation
1212

13-
module TYPELL.ABI.Types
13+
module Typell.ABI.Types
1414

1515
import Data.Bits
1616
import Data.So
1717
import Data.Vect
18+
import Decidable.Equality
1819

1920
%default total
2021

@@ -30,10 +31,10 @@ data Platform = Linux | Windows | MacOS | BSD | WASM
3031
||| This will be set during compilation based on target
3132
public export
3233
thisPlatform : Platform
33-
thisPlatform =
34-
%runElab do
35-
-- Platform detection logic
36-
pure Linux -- Default, override with compiler flags
34+
-- Default platform; override per target via a compiler flag / build option.
35+
-- (Was a `%runElab do … pure Linux` stub that needed ElabReflection for no
36+
-- benefit — it only ever returned Linux.)
37+
thisPlatform = Linux
3738

3839
--------------------------------------------------------------------------------
3940
-- Core Types
@@ -129,7 +130,9 @@ ptrSize WASM = 32
129130
||| Pointer type for platform
130131
public export
131132
CPtr : Platform -> Type -> Type
132-
CPtr p _ = Bits (ptrSize p)
133+
-- Pointers are represented as a machine word. (`Bits (ptrSize p)` was invalid:
134+
-- `Bits` is the Data.Bits interface, not a Nat-indexed fixed-width type.)
135+
CPtr p _ = Bits64
133136

134137
--------------------------------------------------------------------------------
135138
-- Memory Layout Proofs
@@ -148,8 +151,8 @@ data HasAlignment : Type -> Nat -> Type where
148151
||| Size of C types (platform-specific)
149152
public export
150153
cSizeOf : (p : Platform) -> (t : Type) -> Nat
151-
cSizeOf p (CInt _) = 4
152-
cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4
154+
-- NB: `CInt p`/`CSize p` are type-level functions (not constructors), so they
155+
-- cannot be matched directly; they reduce to Bits32/Bits64, handled below.
153156
cSizeOf p Bits32 = 4
154157
cSizeOf p Bits64 = 8
155158
cSizeOf p Double = 8
@@ -158,8 +161,6 @@ cSizeOf p _ = ptrSize p `div` 8
158161
||| Alignment of C types (platform-specific)
159162
public export
160163
cAlignOf : (p : Platform) -> (t : Type) -> Nat
161-
cAlignOf p (CInt _) = 4
162-
cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4
163164
cAlignOf p Bits32 = 4
164165
cAlignOf p Bits64 = 8
165166
cAlignOf p Double = 8

‎typell.ipkg‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
package typell
3+
4+
authors = "Jonathan D.A. Jewell"
5+
license = "MPL-2.0"
6+
version = 0.1.0
7+
8+
sourcedir = "src"
9+
10+
modules = Typell.ABI.Types
11+
, Typell.ABI.Layout
12+
, Typell.ABI.Soundness
13+
, Typell.ABI.InferenceSoundness
14+
, Typell.ABI.LevelMonotonicity
15+
, Typell.ABI.Foreign
16+
17+
depends = base, contrib

0 commit comments

Comments
 (0)