Skip to content

Commit 941409c

Browse files
hyperpolymathhyperpolymath
committed
Auto-commit before sync: Wed 15 Apr 15:29:53 BST 2026
1 parent 3ba07f1 commit 941409c

2 files changed

Lines changed: 357 additions & 166 deletions

File tree

‎src/abi/Foreign.idr‎

Lines changed: 210 additions & 166 deletions
Original file line numberDiff line numberDiff line change
@@ -1,173 +1,217 @@
1-
-- SPDX-License-Identifier: PMPL-1.0-or-later
2-
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3-
--
4-
-- Foreign.idr — Bennett reversibility proofs for the OPSM uninstall ABI.
5-
--
6-
-- This module contains the formal verification that every install action
7-
-- can be exactly reversed: applying an action and then its reverse returns
8-
-- the system to its original state.
9-
--
10-
-- Named after Bennett's reversible computation principle: any computation
11-
-- can be made reversible by recording enough information to undo each step.
12-
-- In OPSM, the action log serves as that record, and these proofs guarantee
13-
-- that the reversal is faithful.
14-
--
15-
-- Key theorems:
16-
-- reversibilityProof — single-action round-trip identity
17-
-- compositionProof — sequence round-trip identity
18-
-- idempotenceProof — double reversal is no-op beyond first
19-
20-
module Foreign
21-
22-
import Types
23-
import Layout
24-
import Data.List
25-
26-
%default total
27-
28-
-- ════════════════════════════════════════════════════════════════════
29-
-- Section 1: Single-Action Reversibility
30-
-- ════════════════════════════════════════════════════════════════════
31-
32-
||| THE KEY THEOREM: For any action `a` and system state `s`,
33-
||| applying the action and then its reverse returns to the original state.
1+
||| SPDX-License-Identifier: PMPL-1.0-or-later
2+
||| Foreign Function Interface Declarations for ODDS_AND_SODS_PACKAGE_MANAGER
343
|||
35-
||| This is the Bennett reversibility guarantee: no information is lost
36-
||| during install, so uninstall can perfectly restore the prior state.
4+
||| This module declares all C-compatible functions that will be
5+
||| implemented in the Zig FFI layer.
376
|||
38-
||| The proof proceeds by case-splitting on the action constructor.
39-
||| In each case, `apply` pushes an element onto a list field, and
40-
||| `unapply` pops it via `drop 1`, which reduces `drop 1 (x :: xs)`
41-
||| to `xs` by definition. Since every other field is untouched,
42-
||| the entire record is restored.
43-
public export
44-
reversibilityProof : (a : Action) -> (s : SystemState) ->
45-
unapply (reverse a) (apply a s) = s
46-
reversibilityProof (CreateFile p c) (MkSystemState fs ds ps de ev su mt au) = Refl
47-
reversibilityProof (CreateDir p) (MkSystemState fs ds ps de ev su mt au) = Refl
48-
reversibilityProof (SetPermission p o n) (MkSystemState fs ds ps de ev su mt au) = Refl
49-
reversibilityProof (RegisterDesktop e) (MkSystemState fs ds ps de ev su mt au) = Refl
50-
reversibilityProof (AddEnvVar b) (MkSystemState fs ds ps de ev su mt au) = Refl
51-
reversibilityProof (EnableSystemd u) (MkSystemState fs ds ps de ev su mt au) = Refl
52-
reversibilityProof (RegisterMime pkg xml) (MkSystemState fs ds ps de ev su mt au) = Refl
53-
reversibilityProof (AddAutostart pkg) (MkSystemState fs ds ps de ev su mt au) = Refl
54-
55-
56-
-- ════════════════════════════════════════════════════════════════════
57-
-- Section 2: Sequence Composition
58-
-- ════════════════════════════════════════════════════════════════════
59-
60-
||| Helper: applying actions one at a time composes correctly.
61-
||| applySequence (a :: as) s = applySequence as (apply a s)
62-
||| This holds by definition and Idris2 can see it directly.
63-
public export
64-
applySequenceCons : (a : Action) -> (as : ActionSequence) -> (s : SystemState) ->
65-
applySequence (a :: as) s = applySequence as (apply a s)
66-
applySequenceCons a as s = Refl
7+
||| All functions are declared here with type signatures and safety proofs.
8+
||| Implementations live in ffi/zig/
679

68-
||| Helper: unapplying reverse actions one at a time composes correctly.
69-
public export
70-
unapplySequenceCons : (r : ReverseAction) -> (rs : List ReverseAction) -> (s : SystemState) ->
71-
unapplySequence (r :: rs) s = unapplySequence rs (unapply r s)
72-
unapplySequenceCons r rs s = Refl
10+
module OddsAndSodsPackageManager.ABI.Foreign
7311

74-
||| Composition theorem for a single action: reversing a singleton
75-
||| sequence restores the original state.
76-
public export
77-
singletonComposition : (a : Action) -> (s : SystemState) ->
78-
unapplySequence [reverse a] (applySequence [a] s) = s
79-
singletonComposition a s = reversibilityProof a s
12+
import OddsAndSodsPackageManager.ABI.Types
13+
import OddsAndSodsPackageManager.ABI.Layout
8014

81-
||| Two-action composition: reversing a two-action sequence in reverse
82-
||| order restores the original state.
83-
|||
84-
||| If we install with [a1, a2], the reverse sequence is [reverse a2, reverse a1].
85-
||| Uninstalling with that sequence undoes a2 first (most recent), then a1.
86-
public export
87-
twoActionComposition : (a1 : Action) -> (a2 : Action) -> (s : SystemState) ->
88-
unapplySequence [reverse a2, reverse a1] (applySequence [a1, a2] s) = s
89-
twoActionComposition a1 a2 s =
90-
rewrite reversibilityProof a2 (apply a1 s) in
91-
reversibilityProof a1 s
92-
93-
94-
-- ════════════════════════════════════════════════════════════════════
95-
-- Section 3: Idempotence of Unapply
96-
-- ════════════════════════════════════════════════════════════════════
97-
98-
||| Idempotence: after one round-trip (apply then unapply), the state is
99-
||| restored. A second unapply on the already-restored state using the
100-
||| *same* reverse action simply pops from the list again — but since the
101-
||| artifact is no longer there (it was already removed), this is a
102-
||| different operation.
103-
|||
104-
||| What we actually prove here is the stronger statement that the
105-
||| round-trip itself is idempotent: doing the full apply-then-unapply
106-
||| cycle twice gives the same result as doing it once.
107-
public export
108-
roundTripIdempotent : (a : Action) -> (s : SystemState) ->
109-
unapply (reverse a) (apply a (unapply (reverse a) (apply a s)))
110-
= unapply (reverse a) (apply a s)
111-
roundTripIdempotent a s =
112-
-- Goal: unapply (reverse a) (apply a (unapply (reverse a) (apply a s)))
113-
-- = unapply (reverse a) (apply a s)
114-
-- Rewriting the inner (unapply (reverse a) (apply a s)) to s gives:
115-
-- unapply (reverse a) (apply a s) = unapply (reverse a) (apply a s)
116-
-- which is Refl.
117-
rewrite reversibilityProof a s in
118-
reversibilityProof a s
119-
120-
121-
-- ════════════════════════════════════════════════════════════════════
122-
-- Section 4: Additional Safety Properties
123-
-- ════════════════════════════════════════════════════════════════════
124-
125-
||| Reverse is involutive at the type level: reversing the reverse
126-
||| of an action gives back an action with the same data.
127-
||| (We cannot state reverse . unreverse = id directly since Action
128-
||| and ReverseAction are different types, but we can show the data
129-
||| round-trips through a reconstruction function.)
130-
public export
131-
unreverse : ReverseAction -> Action
132-
unreverse (RemoveFile p c) = CreateFile p c
133-
unreverse (RemoveDir p) = CreateDir p
134-
unreverse (RestorePermission p o n) = SetPermission p o n
135-
unreverse (UnregisterDesktop e) = RegisterDesktop e
136-
unreverse (RemoveEnvVar b) = AddEnvVar b
137-
unreverse (DisableSystemd u) = EnableSystemd u
138-
unreverse (UnregisterMime pkg xml) = RegisterMime pkg xml
139-
unreverse (RemoveAutostart pkg) = AddAutostart pkg
140-
141-
||| Reverse then unreverse is the identity on actions.
142-
public export
143-
reverseInvolution : (a : Action) -> unreverse (reverse a) = a
144-
reverseInvolution (CreateFile p c) = Refl
145-
reverseInvolution (CreateDir p) = Refl
146-
reverseInvolution (SetPermission p o n) = Refl
147-
reverseInvolution (RegisterDesktop e) = Refl
148-
reverseInvolution (AddEnvVar b) = Refl
149-
reverseInvolution (EnableSystemd u) = Refl
150-
reverseInvolution (RegisterMime pkg xml) = Refl
151-
reverseInvolution (AddAutostart pkg) = Refl
152-
153-
||| Unreverse then reverse is the identity on reverse actions.
154-
public export
155-
unreverseInvolution : (r : ReverseAction) -> reverse (unreverse r) = r
156-
unreverseInvolution (RemoveFile p c) = Refl
157-
unreverseInvolution (RemoveDir p) = Refl
158-
unreverseInvolution (RestorePermission p o n) = Refl
159-
unreverseInvolution (UnregisterDesktop e) = Refl
160-
unreverseInvolution (RemoveEnvVar b) = Refl
161-
unreverseInvolution (DisableSystemd u) = Refl
162-
unreverseInvolution (UnregisterMime pkg xml) = Refl
163-
unreverseInvolution (RemoveAutostart pkg) = Refl
164-
165-
||| Empty action sequence is a no-op.
166-
public export
167-
emptySequenceIdentity : (s : SystemState) -> applySequence [] s = s
168-
emptySequenceIdentity s = Refl
15+
%default total
16916

170-
||| Empty reverse sequence is a no-op.
17+
--------------------------------------------------------------------------------
18+
-- Library Lifecycle
19+
--------------------------------------------------------------------------------
20+
21+
||| Initialize the library
22+
||| Returns a handle to the library instance, or Nothing on failure
23+
export
24+
%foreign "C:odds_and_sods_package_manager_init, libodds_and_sods_package_manager"
25+
prim__init : PrimIO Bits64
26+
27+
||| Safe wrapper for library initialization
28+
export
29+
init : IO (Maybe Handle)
30+
init = do
31+
ptr <- primIO prim__init
32+
pure (createHandle ptr)
33+
34+
||| Clean up library resources
35+
export
36+
%foreign "C:odds_and_sods_package_manager_free, libodds_and_sods_package_manager"
37+
prim__free : Bits64 -> PrimIO ()
38+
39+
||| Safe wrapper for cleanup
40+
export
41+
free : Handle -> IO ()
42+
free h = primIO (prim__free (handlePtr h))
43+
44+
--------------------------------------------------------------------------------
45+
-- Core Operations
46+
--------------------------------------------------------------------------------
47+
48+
||| Example operation: process data
49+
export
50+
%foreign "C:odds_and_sods_package_manager_process, libodds_and_sods_package_manager"
51+
prim__process : Bits64 -> Bits32 -> PrimIO Bits32
52+
53+
||| Safe wrapper with error handling
54+
export
55+
process : Handle -> Bits32 -> IO (Either Result Bits32)
56+
process h input = do
57+
result <- primIO (prim__process (handlePtr h) input)
58+
pure $ case result of
59+
0 => Left Error
60+
n => Right n
61+
62+
--------------------------------------------------------------------------------
63+
-- String Operations
64+
--------------------------------------------------------------------------------
65+
66+
||| Convert C string to Idris String
67+
export
68+
%foreign "support:idris2_getString, libidris2_support"
69+
prim__getString : Bits64 -> String
70+
71+
||| Free C string
72+
export
73+
%foreign "C:odds_and_sods_package_manager_free_string, libodds_and_sods_package_manager"
74+
prim__freeString : Bits64 -> PrimIO ()
75+
76+
||| Get string result from library
77+
export
78+
%foreign "C:odds_and_sods_package_manager_get_string, libodds_and_sods_package_manager"
79+
prim__getResult : Bits64 -> PrimIO Bits64
80+
81+
||| Safe string getter
82+
export
83+
getString : Handle -> IO (Maybe String)
84+
getString h = do
85+
ptr <- primIO (prim__getResult (handlePtr h))
86+
if ptr == 0
87+
then pure Nothing
88+
else do
89+
let str = prim__getString ptr
90+
primIO (prim__freeString ptr)
91+
pure (Just str)
92+
93+
--------------------------------------------------------------------------------
94+
-- Array/Buffer Operations
95+
--------------------------------------------------------------------------------
96+
97+
||| Process array data
98+
export
99+
%foreign "C:odds_and_sods_package_manager_process_array, libodds_and_sods_package_manager"
100+
prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
101+
102+
||| Safe array processor
103+
export
104+
processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
105+
processArray h buf len = do
106+
result <- primIO (prim__processArray (handlePtr h) buf len)
107+
pure $ case resultFromInt result of
108+
Just Ok => Right ()
109+
Just err => Left err
110+
Nothing => Left Error
111+
where
112+
resultFromInt : Bits32 -> Maybe Result
113+
resultFromInt 0 = Just Ok
114+
resultFromInt 1 = Just Error
115+
resultFromInt 2 = Just InvalidParam
116+
resultFromInt 3 = Just OutOfMemory
117+
resultFromInt 4 = Just NullPointer
118+
resultFromInt _ = Nothing
119+
120+
--------------------------------------------------------------------------------
121+
-- Error Handling
122+
--------------------------------------------------------------------------------
123+
124+
||| Get last error message
125+
export
126+
%foreign "C:odds_and_sods_package_manager_last_error, libodds_and_sods_package_manager"
127+
prim__lastError : PrimIO Bits64
128+
129+
||| Retrieve last error as string
130+
export
131+
lastError : IO (Maybe String)
132+
lastError = do
133+
ptr <- primIO prim__lastError
134+
if ptr == 0
135+
then pure Nothing
136+
else pure (Just (prim__getString ptr))
137+
138+
||| Get error description for result code
139+
export
140+
errorDescription : Result -> String
141+
errorDescription Ok = "Success"
142+
errorDescription Error = "Generic error"
143+
errorDescription InvalidParam = "Invalid parameter"
144+
errorDescription OutOfMemory = "Out of memory"
145+
errorDescription NullPointer = "Null pointer"
146+
147+
--------------------------------------------------------------------------------
148+
-- Version Information
149+
--------------------------------------------------------------------------------
150+
151+
||| Get library version
152+
export
153+
%foreign "C:odds_and_sods_package_manager_version, libodds_and_sods_package_manager"
154+
prim__version : PrimIO Bits64
155+
156+
||| Get version as string
157+
export
158+
version : IO String
159+
version = do
160+
ptr <- primIO prim__version
161+
pure (prim__getString ptr)
162+
163+
||| Get library build info
164+
export
165+
%foreign "C:odds_and_sods_package_manager_build_info, libodds_and_sods_package_manager"
166+
prim__buildInfo : PrimIO Bits64
167+
168+
||| Get build information
169+
export
170+
buildInfo : IO String
171+
buildInfo = do
172+
ptr <- primIO prim__buildInfo
173+
pure (prim__getString ptr)
174+
175+
--------------------------------------------------------------------------------
176+
-- Callback Support
177+
--------------------------------------------------------------------------------
178+
179+
||| Callback function type (C ABI)
171180
public export
172-
emptyUnapplyIdentity : (s : SystemState) -> unapplySequence [] s = s
173-
emptyUnapplyIdentity s = Refl
181+
Callback : Type
182+
Callback = Bits64 -> Bits32 -> Bits32
183+
184+
||| Register a callback
185+
export
186+
%foreign "C:odds_and_sods_package_manager_register_callback, libodds_and_sods_package_manager"
187+
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
188+
189+
||| Safe callback registration
190+
export
191+
registerCallback : Handle -> Callback -> IO (Either Result ())
192+
registerCallback h cb = do
193+
result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
194+
pure $ case resultFromInt result of
195+
Just Ok => Right ()
196+
Just err => Left err
197+
Nothing => Left Error
198+
where
199+
resultFromInt : Bits32 -> Maybe Result
200+
resultFromInt 0 = Just Ok
201+
resultFromInt _ = Just Error
202+
203+
--------------------------------------------------------------------------------
204+
-- Utility Functions
205+
--------------------------------------------------------------------------------
206+
207+
||| Check if library is initialized
208+
export
209+
%foreign "C:odds_and_sods_package_manager_is_initialized, libodds_and_sods_package_manager"
210+
prim__isInitialized : Bits64 -> PrimIO Bits32
211+
212+
||| Check initialization status
213+
export
214+
isInitialized : Handle -> IO Bool
215+
isInitialized h = do
216+
result <- primIO (prim__isInitialized (handlePtr h))
217+
pure (result /= 0)

0 commit comments

Comments
 (0)