max.wiki - User contributions [en-ca]

Snapcast Server Setup

2026-02-22T14:57:20Z

Mxl: status -> restart

Notes for '''setting up Snapcast''' (https://github.com/badaix/snapcast) for multi-device audio playback.

== PipeWire as Player ==

To configure PipeWire as a player for Snapcast, create the file <code>10-snapcast-pipe-sink.conf</code> in <code>/etc/pipewire/pipewire.conf.d/</code> (or in <code>~/.config/pipewire/pipewire.conf.d/</code>):

<nowiki>context.modules = [
{
name = libpipewire-module-pipe-tunnel
args = {
tunnel.mode = sink
pipe.filename = "/tmp/snapfifo"
audio.format = S16LE
audio.rate = 48000
audio.channels = 2
audio.position = [ FL FR ]
stream.props = {
node.name = Snapcast
}
}
}
]</nowiki>

Then, restart PipeWire: <code>systemctl --user restart wireplumber pipewire pipewire-pulse</code>.

== Resources ==

* PipeWire wiki on virtual devices: https://gitlab.freedesktop.org/pipewire/pipewire/-/wikis/Virtual-Devices#pipe-devices
* PipeWire documentation on pipe tunnel module: https://docs.pipewire.org/page_module_pipe_tunnel.html
* Snapcast docs on player setup: https://github.com/badaix/snapcast/blob/develop/doc/player_setup.md#pulseaudio

[[Category:System Configuration]]

Main Page

2026-02-22T14:50:50Z

Mxl: fix link

Exzellenz (Font)

2026-02-20T11:48:54Z

Mxl:

[[File:Exzellenz Proof.svg|thumb|right|alt=Preview of font showing text "EXZELLENZ EXCELLENT".|Preview of Exzellenz font]]

An especially '''excellent font'''. Completely and wholly unrelated to the logo of the Technical University of Munich.

The font is available on GitHub at [https://github.com/just-max/exzellenz github.com/just-max/exzellenz]. I also put together a web page that generates PNG/SVG proofs here: [https://just-max.github.io/exzellenz/generator.html?text=Hello%20World just-max.github.io/exzellenz/generator.html].

[[Category:Fonts]]

Configuring mDNS for Easy Access to Devices

2026-02-20T11:48:30Z

Mxl:

[https://en.wikipedia.org/wiki/Zero-configuration_networking Zeroconf] consists of a number of related concepts with the common objective of making simple networked services "just work". Initially it was implemented by Apple as Bonjour, but on Linux the re-implementation [https://en.wikipedia.org/wiki/Avahi_(software) Avahi] is usually used to provide Zeroconf. Although initially intended for discovering networked devices like printers or speakers, it can also be useful for accessing other hosts or smart home devices on the local network without hard-coding their address or hosting a name server.

The relevant concept in Zeroconf that makes this work is multicast DNS (mDNS) which can resolve hostnames inside a local network by using multicast broadcasts. The mDNS client sends a multicast broadcast asking for <code><name>.local</code>, and the host with the given name (typically the device's hostname) answers it (also multicast, so all devices can update their caches). My goal was to make various devices on my home network accessible over their mDNS address. This works unreliably out of the box, I've collected the steps I took to get it working more reliably. The irony of having to configure Zeroconf is not lost on me.

MDNS is easily conflated with DNS service discovery (DNS-SD), which allows discovering specific services (e.g. print service, web server, etc.) once a host is known. Both are relevant, however technically these are two separate concepts under Zeroconf.

== Analyzing the Network ==

To get a more or less complete list of DNS-SD services on the network, use the command <code>avahi-browse --resolve --terminate --all</code>. This uses both mDNS and DNS-SD via the Avahi daemon. For more details, see https://askubuntu.com/a/1105895.

To use mDNS to resolve a hostname, use <code>avahi-resolve-host-name <name>.local</code>. This returns only a single resolved address, even if the host has multiple. To at least reliably get an IPv4 or an IPv6 address, pass <code>-4</code> or <code>-6</code>. Alternatively, an purpose-built app that bundles the binary would work. Either approach would of course conflict with the built-in mdnsd if it ever starts, as both listen on port 5353.

== Becoming Discoverable ==

While some devices are easily made accessible to mDNS queries, some need more work.

=== Avahi (Linux) ===

The Avahi Daemon, as typically configured on Linux distributions, does not answer mDNS queries, because it is not configured to provide any services. To publish a "workstation" service, effectively advertising only that the host exists, a change is required in the config file (probably <code>/etc/avahi/avahi-daemon.conf</code>):

publish-workstation=yes

This [https://superuser.com/a/1311455 supposedly used to be the default] in earlier versions, but was changed for security reasons. Using a firewall on untrusted networks is a good idea anyway!

Restart the Daemon afterwards with <code>sudo systemctl restart avahi-daemon.service</code>.

=== Android ===

Support for responding to mDNS queries on Android devices [https://android.stackexchange.com/a/242004 is poor]. A daemon <code>mdnsd</code> exists, but the address is hard-coded to <code>Android.local</code> and the daemon only starts if an app registers some service.

One idea [https://stackoverflow.com/a/70343905 is to patch mdnsd] to make the advertized hostname configurable, then run the binary at startup with Termux:Boot. But given the general direction of Android, the chance that this stops working in a future update [https://github.com/termux/termux-app/issues/2155 is always high].

== Discovering Others ==

=== Linux (Avahi/NSS) ===

Resolution of mDNS addresses on Linux is provided by Avahi via a plugin to the Nameserver Switch (NSS). Multicast DNS is distinct from plain DNS, and is thus enabled by its own entry under <code>hosts:</code> in <code>/etc/nsswitch.conf</code>. On my Fedora system, this contains <code>mdns4_minimal [NOTFOUND=return]</code>, which means mDNS is consulted over IPv4. Most applications will consult the NSS (via glibc) and thus be able to resolve <code>.local</code> addresses.

As a matter of principle, I would also like mDNS over IPv6. This can be accomplished by changing <code>mdns4_minimal [NOTFOUND=return]</code> to <code>mdns_minimal [NOTFOUND=return]</code>, which tries both IPv6 and IPv4.

On my system, <code>nsswitch.conf</code> is managed by authselect (<code>man(8) authselect</code>, <code>man(5) authselect-profiles</code>). From <code>authselect current</code>, the current profile is called <code>local</code>, while <code>authselect list-features local</code> lists the available feature <code>with-mdns6</code>. Enabling the feature with <code>authselect enable-feature with-mdns6</code> makes the appropriate change to <code>nsswitch.conf</code>.

To check that the change worked, we should find some host that advertises an IPv6 address ([[#Analyzing the Network]]). Then we can use <code>getent ahosts <name>.local</code>, which should return that IPv6 addresses. Unlike the Avahi browse/resolve tools, <code>getent</code> consults the NSS and should thus be indicative of what a normal application sees when making DNS queries.

==== Caveat on IPv6 Support ====

Consulting <code>man(5) nsswitch.conf</code>, additional services are implemented as shared libraries named <code>libnss_SERVICE.so.X</code>. Looking in the appropriate places (<code>man(8) ldconfig</code>), we can list available services:

find /lib/ /lib64/ /usr/lib/ /usr/lib64/ -name 'libnss_*.so.*' -print0
| xargs --null basename --multiple | sort | uniq

Among other things, this finds the library <code>/lib64/libnss_mdns4.so.2</code> which on my system is provided by the package [https://github.com/avahi/nss-mdns nss-mdns]. From the README, IPv6 support is as simple as changing <code>mdns4_minimal</code> to <code>mdns_minimal</code>.

However, it comes with the following warning:

<blockquote>
Due to the fact that most mDNS responders only register local IPv4 addresses via mDNS, most people will want to use <code>libnss_mdns4.so.2</code> exclusively. Using <code>libnss_mdns.so.2</code> or <code>libnss_mdns6.so.2</code> in such a situation causes long timeouts when resolving hosts since most modern Unix/Linux applications check for IPv6 addresses first, followed by a lookup for IPv4.
</blockquote>

Indeed, the only hosts advertising an IPv6 address on my home network are my Linux laptop and my Linux server. However, by using the <code>libnss_mdns_minimal</code> libraries, non-mDNS addresses will by immediately rejected, so that the timeout won't affect us when not resolving mDNS addresses.

=== Android ===

Unlike the poor support for ''responding'' to queries, Android [https://source.android.com/docs/core/ota/modular-system/dns-resolver#mdns-local-resolution supports resolving mDNS addresses directly] as of November 2021. This should be transparent to applications, as it is built in to <code>getaddrinfo()</code>.

[[Category:System_Configuration]]

Main Page

2026-02-20T11:47:45Z

Mxl:

File:GE Rapid Clean II Name.svg

2026-02-20T11:45:41Z

Mxl:

File:Exzellenz.svg

2026-02-20T11:34:51Z

Mxl: Mxl uploaded a new version of File:Exzellenz.svg

File:Exzellenz.svg

2026-02-20T11:27:59Z

Mxl:

Exzellenz (Font)

2026-02-20T11:25:36Z

Mxl: Created page with "Preview of Exzellenz font An especially '''excellent font'''. Completely and wholly unrelated to the logo of the Technical University of Munich. The font is available on GitHub at [https://github.com/just-max/exzellenz github.com/just-max/exzellenz]. I also put together a web page that generates PNG/SVG proofs here: [https://just-max.github.io/exzellenz/generator.html?text=..."

File:Exzellenz Proof.svg

2026-02-20T11:17:18Z

Mxl:

Main Page

2026-02-20T09:58:54Z

Mxl:

Configuring mDNS for Easy Access to Devices

2026-02-20T09:58:15Z

Mxl:

Configuring mDNS for Easy Access to Devices

2026-02-20T09:56:22Z

Mxl:

[https://en.wikipedia.org/wiki/Zero-configuration_networking Zeroconf] consists of a number of related concepts with the common objective of making simple networked services "just work". Initially it was implemented by Apple as Bonjour, but on Linux the re-implementation [https://en.wikipedia.org/wiki/Avahi_(software) Avahi] is usually used to provide Zeroconf. Although initially intended for discovering networked devices like printers or speakers, it can also be useful for accessing other hosts or smart home devices on the local network without hard-coding their address or hosting a name server.

The relevant concept in Zeroconf that makes this work is multicast DNS (mDNS) which can resolve hostnames inside a local network by using multicast broadcasts. The mDNS client sends a multicast broadcast asking for <code><name>.local</code>, and the host with the given name (typically the device's hostname) answers it (also multicast, so all devices can update their caches). My goal was to make various devices on my home network accessible over their mDNS address. This works unreliably out of the box, I've collected the steps I took to get it working more reliably.

MDNS is easily conflated with DNS service discovery (DNS-SD), which allows discovering specific services (e.g. print service, web server, etc.) once a host is known. Both are relevant, however technically these are two separate concepts under Zeroconf.

== Analyzing the Network ==

To get a more or less complete list of DNS-SD services on the network, use the command <code>avahi-browse --resolve --terminate --all</code>. This uses both mDNS and DNS-SD via the Avahi daemon. For more details, see https://askubuntu.com/a/1105895.

To use mDNS to resolve a hostname, use <code>avahi-resolve-host-name <name>.local</code>. This returns only a single resolved address, even if the host has multiple. To at least reliably get an IPv4 or an IPv6 address, pass <code>-4</code> or <code>-6</code>. Alternatively, an purpose-built app that bundles the binary would work. Either approach would of course conflict with the built-in mdnsd if it ever starts, as both listen on port 5353.

== Becoming Discoverable ==

While some devices are easily made accessible to mDNS queries, some need more work.

=== Avahi (Linux) ===

The Avahi Daemon, as typically configured on Linux distributions, does not answer mDNS queries, because it is not configured to provide any services. To publish a "workstation" service, effectively advertising only that the host exists, a change is required in the config file (probably <code>/etc/avahi/avahi-daemon.conf</code>):

publish-workstation=yes

This [https://superuser.com/a/1311455 supposedly used to be the default] in earlier versions, but was changed for security reasons. Using a firewall on untrusted networks is a good idea anyway!

Restart the Daemon afterwards with <code>sudo systemctl restart avahi-daemon.service</code>.

=== Android ===

Support for responding to mDNS queries on Android devices [https://android.stackexchange.com/a/242004 is poor]. A daemon <code>mdnsd</code> exists, but the address is hard-coded to <code>Android.local</code> and the daemon only starts if an app registers some service.

One idea [https://stackoverflow.com/a/70343905 is to patch mdnsd] to make the advertized hostname configurable, then run the binary at startup with Termux:Boot. But given the general direction of Android, the chance that this stops working in a future update [https://github.com/termux/termux-app/issues/2155 is always high].

== Discovering Others ==

=== Linux (Avahi/NSS) ===

Resolution of mDNS addresses on Linux is provided by Avahi via a plugin to the Nameserver Switch (NSS). Multicast DNS is distinct from plain DNS, and is thus enabled by its own entry under <code>hosts:</code> in <code>/etc/nsswitch.conf</code>. On my Fedora system, this contains <code>mdns4_minimal [NOTFOUND=return]</code>, which means mDNS is consulted over IPv4. Most applications will consult the NSS (via glibc) and thus be able to resolve <code>.local</code> addresses.

As a matter of principle, I would also like mDNS over IPv6. This can be accomplished by changing <code>mdns4_minimal [NOTFOUND=return]</code> to <code>mdns_minimal [NOTFOUND=return]</code>, which tries both IPv6 and IPv4.

On my system, <code>nsswitch.conf</code> is managed by authselect (<code>man(8) authselect</code>, <code>man(5) authselect-profiles</code>). From <code>authselect current</code>, the current profile is called <code>local</code>, while <code>authselect list-features local</code> lists the available feature <code>with-mdns6</code>. Enabling the feature with <code>authselect enable-feature with-mdns6</code> makes the appropriate change to <code>nsswitch.conf</code>.

To check that the change worked, we should find some host that advertises an IPv6 address ([[#Analyzing the Network]]). Then we can use <code>getent ahosts <name>.local</code>, which should return that IPv6 addresses. Unlike the Avahi browse/resolve tools, <code>getent</code> consults the NSS and should thus be indicative of what a normal application sees when making DNS queries.

==== Caveat on IPv6 Support ====

Consulting <code>man(5) nsswitch.conf</code>, additional services are implemented as shared libraries named <code>libnss_SERVICE.so.X</code>. Looking in the appropriate places (<code>man(8) ldconfig</code>), we can list available services:

find /lib/ /lib64/ /usr/lib/ /usr/lib64/ -name 'libnss_*.so.*' -print0
| xargs --null basename --multiple | sort | uniq

Among other things, this finds the library <code>/lib64/libnss_mdns4.so.2</code> which on my system is provided by the package [https://github.com/avahi/nss-mdns nss-mdns]. From the README, IPv6 support is as simple as changing <code>mdns4_minimal</code> to <code>mdns_minimal</code>.

However, it comes with the following warning:

<blockquote>
Due to the fact that most mDNS responders only register local IPv4 addresses via mDNS, most people will want to use <code>libnss_mdns4.so.2</code> exclusively. Using <code>libnss_mdns.so.2</code> or <code>libnss_mdns6.so.2</code> in such a situation causes long timeouts when resolving hosts since most modern Unix/Linux applications check for IPv6 addresses first, followed by a lookup for IPv4.
</blockquote>

Indeed, the only hosts advertising an IPv6 address on my home network are my Linux laptop and my Linux server. However, by using the <code>libnss_mdns_minimal</code> libraries, non-mDNS addresses will by immediately rejected, so that the timeout won't affect us when not resolving mDNS addresses.

=== Android ===

Unlike the poor support for ''responding'' to queries, Android [https://source.android.com/docs/core/ota/modular-system/dns-resolver#mdns-local-resolution supports resolving mDNS addresses directly] as of November 2021. This should be transparent to applications, as it is built in to <code>getaddrinfo()</code>.

Configuring mDNS for Easy Access to Devices

2026-02-20T07:57:00Z

Mxl:

[https://en.wikipedia.org/wiki/Zero-configuration_networking Zeroconf] consists of a number of related concepts with the common objective of making simple networked services "just work". Initially it was implemented by Apple as Bonjour, but on Linux the re-implementation [https://en.wikipedia.org/wiki/Avahi_(software) Avahi] is usually used to provide Zeroconf. Although initially intended for discovering networked devices like printers or speakers, it can also be useful for accessing other hosts or smart home devices on the local network without hard-coding their address or hosting a name server.

The relevant concept in Zeroconf that makes this work is multicast DNS (mDNS) which can resolve hostnames inside a local network by using multicast broadcasts. The mDNS client sends a multicast broadcast asking for <code><name>.local</code>, and the host with the given name (typically the device's hostname) answers it. My goal was to make various devices on my home network accessible over their mDNS address. This works unreliably out of the box, I've collected the steps I took to get it working more reliably.

MDNS is easily conflated with DNS service discovery (DNS-SD), which allows discovering specific services (e.g. print service, web server, etc.) once a host is known. Both are relevant, however technically these are two separate concepts under Zeroconf.

== Analyzing the Network ==

To get a more or less complete list of DNS-SD services on the network, use the command <code>avahi-browse --resolve --terminate --all</code>. This uses both mDNS and DNS-SD via the Avahi daemon. For more details, see https://askubuntu.com/a/1105895.

To use mDNS to resolve a hostname, use <code>avahi-resolve-host-name <name>.local</code>. This returns only a single resolved address, even if the host has multiple. To at least reliably get an IPv4 or an IPv6 address, pass <code>-4</code> or <code>-6</code>.

== Becoming Discoverable ==

While some devices are easily made accessible to mDNS queries, some need more work.

=== Avahi (Linux) ===

The Avahi Daemon, as typically configured on Linux distributions, does not answer mDNS queries, because it is not configured to provide any services. To publish a "workstation" service, effectively advertising only that the host exists, a change is required in the config file (probably <code>/etc/avahi/avahi-daemon.conf</code>):

publish-workstation=yes

This [https://superuser.com/a/1311455 supposedly used to be the default] in earlier versions, but was changed for security reasons. Using a firewall on untrusted networks is a good idea anyway!

Restart the Daemon afterwards with <code>sudo systemctl restart avahi-daemon.service</code>.

=== Android ===

Support is poor: the address is hard-coded to <code>Android.local</code> and the daemon only starts if some service is registered.

== Discovering Others ==

=== Linux (Avahi/NSS) ===

Resolution of mDNS addresses on Linux is provided by Avahi via a plugin to the Nameserver Switch (NSS). Multicast DNS is distinct from plain DNS, and is thus enabled by its own entry under <code>hosts:</code> in <code>/etc/nsswitch.conf</code>. On my Fedora system, this contains <code>mdns4_minimal [NOTFOUND=return]</code>, which means mDNS is consulted over IPv4. Most applications will consult the NSS (via glibc) and thus be able to resolve <code>.local</code> addresses.

As a matter of principle, I would also like mDNS over IPv6. This can be accomplished by changing <code>mdns4_minimal [NOTFOUND=return]</code> to <code>mdns_minimal [NOTFOUND=return]</code>, which tries both IPv6 and IPv4.

On my system, <code>nsswitch.conf</code> is managed by authselect (<code>man(8) authselect</code>, <code>man(5) authselect-profiles</code>). From <code>authselect current</code>, the current profile is called <code>local</code>, while <code>authselect list-features local</code> lists the available feature <code>with-mdns6</code>. Enabling the feature with <code>authselect enable-feature with-mdns6</code> makes the appropriate change to <code>nsswitch.conf</code>.

==== Caveat on IPv6 Support ====

Consulting <code>man(5) nsswitch.conf</code>, additional services are implemented as shared libraries named <code>libnss_SERVICE.so.X</code>. Looking in the appropriate places (<code>man(8) ldconfig</code>), we can list available services:

find /lib/ /lib64/ /usr/lib/ /usr/lib64/ -name 'libnss_*.so.*' -print0
| xargs --null basename --multiple | sort | uniq

Among other things, this finds the library <code>/lib64/libnss_mdns4.so.2</code> which on my system is provided by the package [https://github.com/avahi/nss-mdns nss-mdns]. From the README, IPv6 support is as simple as changing <code>mdns4_minimal</code> to <code>mdns_minimal</code>.

However, it comes with the following warning:

<blockquote>
Due to the fact that most mDNS responders only register local IPv4 addresses via mDNS, most people will want to use <code>libnss_mdns4.so.2</code> exclusively. Using <code>libnss_mdns.so.2</code> or <code>libnss_mdns6.so.2</code> in such a situation causes long timeouts when resolving hosts since most modern Unix/Linux applications check for IPv6 addresses first, followed by a lookup for IPv4.
</blockquote>

Indeed, the only hosts advertising an IPv6 address on my home network are my Linux laptop and my Linux server. However, by using the <code>libnss_mdns_minimal</code> libraries, non-mDNS addresses will by immediately rejected, so that the timeout won't affect us when not resolving mDNS addresses.

== mDNS and Android ==

As of November 2021, Android supports resolving mDNS addresses directly.
https://source.android.com/docs/core/ota/modular-system/dns-resolver#mdns-local-resolution

https://old.reddit.com/r/synology/comments/sk8dzz/cannot_ping_mdns_address_servernamelocal_on/hvk0v5k/

Configuring mDNS for Easy Access to Devices

2026-02-20T07:23:24Z

Mxl:

Configuring mDNS for Easy Access to Devices

2026-02-20T06:27:52Z

Mxl: Created page with "[https://en.wikipedia.org/wiki/Zero-configuration_networking Zeroconf] consists of a number of related concepts with the common objective of making simple networked services "just work". Initially it was implemented by Apple as Bonjour, but on Linux the re-implementation [https://en.wikipedia.org/wiki/Avahi_(software) Avahi] is usually used to provide Zeroconf. Although initially intended for discovering networked devices like printers or speakers, it can also be useful..."

Goopworld

2025-11-21T18:54:36Z

Mxl: Created page with "== Coordinates == * warden? 940, -31, -36"

== Coordinates ==

* warden? 940, -31, -36

Snapcast Server Setup

2025-08-31T20:54:59Z

Mxl: Category

Notes for '''setting up Snapcast''' (https://github.com/badaix/snapcast) for multi-device audio playback.

== PipeWire as Player ==

To configure PipeWire as a player for Snapcast, create the file <code>10-snapcast-pipe-sink.conf</code> in <code>/etc/pipewire/pipewire.conf.d/</code> (or in <code>~/.config/pipewire/pipewire.conf.d/</code>):

<nowiki>context.modules = [
{
name = libpipewire-module-pipe-tunnel
args = {
tunnel.mode = sink
pipe.filename = "/tmp/snapfifo"
audio.format = S16LE
audio.rate = 48000
audio.channels = 2
audio.position = [ FL FR ]
stream.props = {
node.name = Snapcast
}
}
}
]</nowiki>

Then, restart PipeWire: <code>systemctl --user status wireplumber pipewire pipewire-pulse</code>.

== Resources ==

* PipeWire wiki on virtual devices: https://gitlab.freedesktop.org/pipewire/pipewire/-/wikis/Virtual-Devices#pipe-devices
* PipeWire documentation on pipe tunnel module: https://docs.pipewire.org/page_module_pipe_tunnel.html
* Snapcast docs on player setup: https://github.com/badaix/snapcast/blob/develop/doc/player_setup.md#pulseaudio

[[Category:System Configuration]]

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-08-11T11:57:50Z

Mxl:

Progress tracking for master's thesis '''Translating Time Bounds of Functional Programs to a Deeply-Embedded Language'''.

== Progress ==

=== March 24th–April 28th ===

Read through [https://arxiv.org/pdf/2503.02975 Proof-Producing Translation of Functional Programs into a Time & Space Reasonable Model] which describes existing work on functional correctness.

Read [https://www.chargueraud.org/research/2018/bigo_credits/bigo_credits.pdf A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification] which develops a framework for interactive proofs of running time intended as part of an interface specification. The method first recursively descends through the function to calculate its running time up to recursive calls, e.g. <code>T_f(x) = 2 + T_f(x - 1)</code>. The user is asked to provide a "shape" of the running time bound they wish to specify, e.g. <code>a * x</code>, where <code>a</code> is left as a variable to solve for. Then induction is performed on the goal e.g. <code>2 + T_f(x - 1) <= a * x</code>, which through induction then becomes <code>2 + a * (x - 1) <= a * x</code>, thus providing a constraint on a suitable <code>a</code>. This is essentially the [https://enos.itcollege.ee/~japoia/algorithms/GT/Introduction_to_algorithms-3rd%20Edition.pdf#page=104 "substitution method" of Cormen et al.].

=== April 28th–May 12th ===

Investigated how to generate running time constraints in Isabelle by recursive tactics on the structure of the IMP-Tailcall term, as in previous work on correctness. The issue to overcome is that we must work with a predicate of the form \exists c. \forall s. T_f_IMP s <= c * T_f (s "x"), which requires providing a single witness c for the linear factor. Previous work on correctness split the single goal recursively at sequences and conditionals into goals for each sub-term, but this approach doesn't work directly with an existential quantor: the '''same''' constant must be a witness in both subterms.

Instead of working directly with the existential, we can "provide" a witness up-front in the form of a schematic variable, and instantiate the schematic step-by-step. Thus we work with a predicate that bounds the running time by e.g. c * T_f (s "x"), without the existential quantor, and compute suitable constraints on the way down. Once we have computed a suitable c, it is obviously a witness for the existential quantor and we can close the goal.

This poses an additional challenge when previously verified functions are called, as the scheme devised above requires a concrete running time bound, not quantified with the existence of a constant. For this, we use Isabelle's LEAST operator to materialize the existential c from the running time of the auxiliary function's bound. (The obvious approach of "obtain"ing the constant with Isabelle's proof functionality does not work, as the schematic witness c of the function being analyzed can not depend on a value obtained later). We can then work with this (LEAST c. ...) * T_aux ... term just like any other bound.

After analyzing the term, we can instantiate and apply an induction hypothesis where applicable, this essentially corresponds to Cormen's "substitution method".

We are left with constraints on the constant c which must be solved, then c can be instantiated and the goals closed.

==== To Discuss ====

Should we investigate other approaches? For example, computing the running time up-front.

How can we automatically solve for suitable constants from the resulting constraints?

==== To-do for Next Week ====

Examine more complex functions which:
* call functions with non-constant running time
* have preconditions on the well-formedness of their inputs
* use data types (this will only work to relate to HOL-Nat)

The condition of an if/else may depend on the input beyond just determining which case of the original function is being called, i.e. cannot necessarily be solved directly based on the inductive case being considered. Thus we cannot assume that we can solve the if/else if we introduce one into our timing constraint. The natural idea to use a maximum of both branches' running time won't work, consider for example the simple expression <code>if b then 1 else g y</code>; then, taking the maximum on the running time would result in a constraint like <code>max 3 ((LEAST c. ...) * T_g (s' "y")) <= ?c * T_f (s "x")</code>, which upon expanding <code>T_f</code> in the right-hand-side and taking the lower bound of the resulting if/else, would yield something like <code>max 3 ((LEAST c. ...) * T_g (s' "y")) <= ?c * 1</code>, which is obviously nonsense. Instead, we could try creating one inequality constraint for each branch.

Investigate the use of SMT-solvers or other automated solvers for the resulting inequality constraints.

=== May 12th–26th ===

Better rule for <code>if</code>. Gather running time into constraint for each terminal (tail-call or assignment to return register), "run" function, rearrange constraint to find lower bound on c, take the maximum of all lower bounds as suitable c.

==== To Discuss ====

==== To-do for Next Week ====

* Prove that the running time of compiled functions always has the assumed form. Use the definition of the compiler (Kappelmann et al.) and the definition of generated HOL running times.
* From here, argue why or why not an SMT solver could be used to solve the resulting constraints.
* Adapt the <code>running</code>/<code>gather</code> method to (tail) recursive functions.

=== May 26th–June 6th ===

Formalized a semantics for HOL-TCNat, such that <code>T_f x1 ... xn = [[e]]_(x1, ..., xn) + 1</code> for a function <code>f x1 ... xn = e</code> and its generated running time function <code>T_f</code>. The big-step predicate has the form: <code>(tail-call term :: HOL_TCNat, argument vector :: nat list) |- (term :: HOL_TCNat, let-bound variables :: Nat list) =>^(running time :: nat) (result :: nat)</code>.

So we define:

* <code>(f,xs) |- (Number n,bs) =>^0 n</code> (and similar for <code>LetBound n</code> and <code>Arg n</code>, by accessing <code>bs</code> and <code>xs</code> respectively).
* If <code>forall i. (f,xs) |- (ts_i,bs) =>^zs_i vs_i</code> and <code>g vs = v'</code> and <code>z' = sum(zs) + T_g vs</code>, then <code>(f,xs) |- (Call g ts,bs) =>^z' v'</code>
* etc.

Then, for the body <code>f</code> of a HOL-TCN function <code>F</code> assuming:
* there are correctness lemmas available for each non-primitive auxiliary function, and
* each primitive aux. function has constant running time,
we can show:

<nowiki>
forall r_0. forall t, r.
exist fs. fs_i is called in t --> exist cs, k.
forall xs, b.
forall s. s arg_f,i = xs_i -->
exist ss'.
(f,xs) |- (t,b) =>^(sum_i(fs_i ss'_i) z for some z
and [[f]]_(r_0)^([]) |- ([[t]]_r^b,s)
=>^(k + sum_i(cs_i * fs_i s's_i)) s' for some s'</nowiki>

The proof is an induction on the rule of <code>F</code>, followed by an induction on the term <code>f</code>. The <code>Let</code>-case requires a lemma about substitution.

Thus the running time always has the assumed form, and approach from last time (almost) works: for tail-recursive functions, the procedure for finding a lower bound on c would try and instantiate c with a term containing c... This can be fixed. In general, we have to show:

<nowiki>
k + sum_i(cs_i * fs_i s's_i) <= ?c * sum_i(fs_i s's_i)</nowiki>

In the case where one of the <code>fs_i</code> is <code>?c * T_f s'</code>, we rearrange to:

<nowiki>
k + sum_i(cs_i * fs_i s's_i) <= ?c * sum_i(fs_i s's_i) - ?c * T_f s'</nowiki>

removing c_f, T_f, s' from the vectors on the LHS. On the RHS, one of the fs/s's is c_f/T_f, which cancels out the subtracted term.

Then we can rearrange to find a lower bound on ?c, as before.

=== June 6th–June 23rd ===

Finished writing up the proof from last week.

==== Discussion ====

Problem: when doing induction over the structure of the term t, in the recursive call case, there is no subterm to apply the induction hypothesis to. Instead, we can do the proof by rule induction over the semantics of HOL-TCN. This means we are assuming that there is an inference for the term in the semantics (i.e. it terminates with a time+value); the justification for this assumption is that the HOL function has a termination order, from which we can construct a termination order for the HOL-TCN term.

A certified translation of Coq functions into deeply-embedded lambda terms: https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.17/LIPIcs.ITP.2019.17.pdf. Question: what about the step from lambda terms to an imperative language?

==== To-do for next week ====

Write-up proof in TeX. Start implementation in ML.

=== June 23rd–July 21st ===

Idea from last time doesn't work. Need to explicitly calculate called functions of HOL-TCN term, then relate to called IMP programs of compiled IMP-TC program. See PDF (Zulip).

==== To-do for next time ====

Talk about "traces" instead of "running to leaves", use bigstep notation (time is replaced by trace, end state/value by pre-tail state).

Instead of putting the trace semantics into one function/predicate, one could investigate an alternative approach. The trace semantics and the subsequent interpretation as running time can essentially be split into three steps: for a given state, 1. compute a linear "list" of instructions by resolving all branches from the given state, 2. from the linearization, extract the list of calls/constants that actually compose the trace, 3. interpret the trace into a concrete (i.e. just an integer) running time. Steps 1. and 2. are currently combined into one predicate, but could be split. This should be investigated, as it could lead to (potentially more but) easier/simpler proofs.

=== July 21st–August 11th ===

Formalized (in Isabelle) the trace semantics that were presented last time, along with the HOL-TCN to IMP-TC compiler. Proved the compiler correct (for terms without recursive calls), and formalized the proof that the traces of the compiled program are related to the traces of the HOL-TCN term.

==== To-do for next time ====

A few (smaller?) lemmas are still required, finish those. Prove the theorems relating traces and running times for HOL-TCN and IMP-TC. Prove the corollary of related traces that running times are also related.

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-07-21T05:19:56Z

Mxl:

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-06-23T15:19:11Z

Mxl:

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-06-06T12:31:18Z

Mxl:

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-06-06T11:39:49Z

Mxl: progress 1

Apfelkuchen Rezept von Oma

2025-05-27T15:51:29Z

Mxl: Grammatik

Rezept für einen '''Apfelkuchen''' (oder alternativ, indem man stattdessen Rhabarber nimmt, einen '''Rhabarberkuchen''') den ich mal von meiner Oma am Telefon übermittelt bekommen habe.

== Rezept ==

=== Mürbteig ===

Für den Boden 180 g Mehl, 100 g Zucker, 180 g Butter, und 1 Ei zu einem Teig verarbeiten. Den Teig anschließend mindestens 30 Minuten im Kühlschrank ruhen lassen, dann ausrollen und in einer Springform bringen.

Den Teig verarbeitet man am besten mit den Händen, da er sehr zäh ist. Die Butter sollte möglichst gleichmäßig verteilt sein, passt man nicht auf, neigt sie dazu kleine Klumpen zu bilden.

=== Füllung ===

Für eine Apfelfüllung etwa 5–6 Äpfel schälen und dünn schneiden. Den Kuchen damit dicht belegen.

Für eine Rhabarberfüllung 800 g Rhabarber in etwa 1–2 cm große Stücke schneiden und den Kuchen damit belegen. Der Rhabarber sollte eine augenscheinlich zu große Häufung bilden, schrumpft aber deutlich beim Backen.

=== Guss ===

Für den Guss 3 Eier trennen und das Eiweiß zu Schnee schlagen. Das Eigelb mit 2 EL Zucker cremig rühren, dann knapp 1 EL Mehl und ½ Becher süße Sahne einrühren. Den Eierschnee vorsichtig untermischen und den Guss auf dem Kuchen gießen.

Ein Becher Sahne sind je nach Marke etwa 200 mL, hier kann man also 100 mL nehmen. Gemeint ist ganz normale süße Sahne (15 %), "süß" als Gegensatz zu "saurer Sahne".

=== Backen ===

Den Kuchen bei 180 ° Ober-/Unterhitze (ohne Umluft) circa 40–45 Minuten backen.

[[Category:Recipes]]

Category:Recipes

2025-05-27T15:50:16Z

Mxl: Created page with "Recipes."

Recipes.

Apfelkuchen Rezept von Oma

2025-05-27T15:50:01Z

Mxl: Category

Rezept für einen '''Apfelkuchen''' (oder alternativ, indem man stattdessen Rhabarber nimmt, einen '''Rhabarberkuchen''') den ich mal von meiner Oma am Telefon übermittelt bekommen habe.

== Rezept ==

=== Mürbteig ===

Für den Boden 180 g Mehl, 100 g Zucker, 180 g Butter, und 1 Ei zu einem Teig verarbeiten. Den Teig anschließend mindestens 30 Minuten im Kühlschrank ruhen lassen, dann ausrollen und in einer Springform bringen.

Den Teig verarbeitet man am besten mit den Händen, da er sehr zäh ist. Die Butter sollte möglichst gleichmäßig verteilt sein, passt man nicht auf, neigt sie dazu kleine Klumpen zu bilden.

=== Füllung ===

Für eine Apfelfüllung etwa 5–6 Äpfel schälen und dünn schneiden. Den Kuchen damit dicht belegen.

Für eine Rhabarberfüllung 800 g Rhabarber in etwa 1–2 cm große Stücke schneiden und den Kuchen damit belegen. Der Rhabarber sollte einen augenscheinlich zu große Häufung bilden, schrumpft aber deutlich beim Backen.

=== Guss ===

Für den Guss 3 Eier trennen und das Eiweiß zu Schnee schlagen. Das Eigelb mit 2 EL Zucker cremig rühren, dann knapp 1 EL Mehl und ½ Becher süße Sahne einrühren. Den Eierschnee vorsichtig untermischen und den Guss auf dem Kuchen gießen.

Ein Becher Sahne sind je nach Marke etwa 200 mL, hier kann man also 100 mL nehmen. Gemeint ist ganz normale süße Sahne (15 %), "süß" als Gegensatz zu "saurer Sahne".

=== Backen ===

Den Kuchen bei 180 ° Ober-/Unterhitze (ohne Umluft) circa 40–45 Minuten backen.

[[Category:Recipes]]

Main Page

2025-05-27T15:49:30Z

Mxl: Recipes

Apfelkuchen Rezept von Oma

2025-05-27T15:48:19Z

Mxl: Oapfelkuchen

Rezept für einen '''Apfelkuchen''' (oder alternativ, indem man stattdessen Rhabarber nimmt, einen '''Rhabarberkuchen''') den ich mal von meiner Oma am Telefon übermittelt bekommen habe.

== Rezept ==

=== Mürbteig ===

Für den Boden 180 g Mehl, 100 g Zucker, 180 g Butter, und 1 Ei zu einem Teig verarbeiten. Den Teig anschließend mindestens 30 Minuten im Kühlschrank ruhen lassen, dann ausrollen und in einer Springform bringen.

Den Teig verarbeitet man am besten mit den Händen, da er sehr zäh ist. Die Butter sollte möglichst gleichmäßig verteilt sein, passt man nicht auf, neigt sie dazu kleine Klumpen zu bilden.

=== Füllung ===

Für eine Apfelfüllung etwa 5–6 Äpfel schälen und dünn schneiden. Den Kuchen damit dicht belegen.

Für eine Rhabarberfüllung 800 g Rhabarber in etwa 1–2 cm große Stücke schneiden und den Kuchen damit belegen. Der Rhabarber sollte einen augenscheinlich zu große Häufung bilden, schrumpft aber deutlich beim Backen.

=== Guss ===

Für den Guss 3 Eier trennen und das Eiweiß zu Schnee schlagen. Das Eigelb mit 2 EL Zucker cremig rühren, dann knapp 1 EL Mehl und ½ Becher süße Sahne einrühren. Den Eierschnee vorsichtig untermischen und den Guss auf dem Kuchen gießen.

Ein Becher Sahne sind je nach Marke etwa 200 mL, hier kann man also 100 mL nehmen. Gemeint ist ganz normale süße Sahne (15 %), "süß" als Gegensatz zu "saurer Sahne".

=== Backen ===

Den Kuchen bei 180 ° Ober-/Unterhitze (ohne Umluft) circa 40–45 Minuten backen.

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-16T14:34:04Z

Mxl:

Automated Running Time Equivalences (Thesis Project Tracking)

2025-05-16T14:26:45Z

Mxl: Mxl moved page Automated Running Time Equivalences (Thesis Project Tracking) to Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking): Better title

#REDIRECT [[Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)]]

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-16T14:26:45Z

== Progress ==

=== March 24th–April 28th ===

Read through [https://arxiv.org/pdf/2503.02975 Proof-Producing Translation of Functional Programs into a Time & Space Reasonable Model] which describes existing work on functional correctness.

Read [https://www.chargueraud.org/research/2018/bigo_credits/bigo_credits.pdf A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification] which develops a framework for interactive proofs of running time intended as part of an interface specification. The method first recursively descends through the function to calculate its running time up to recursive calls, e.g. <code>T_f(x) = 2 + T_f(x - 1)</code>. The user is asked to provide a "shape" of the running time bound they wish to specify, e.g. <code>a * x</code>, where <code>a</code> is left as a variable to solve for. Then induction is performed on the goal e.g. <code>2 + T_f(x - 1) <= a * x</code>, which through induction then becomes <code>2 + a * (x - 1) <= a * x</code>, thus providing a constraint on a suitable <code>a</code>. This is essentially the [https://enos.itcollege.ee/~japoia/algorithms/GT/Introduction_to_algorithms-3rd%20Edition.pdf#page=104 "substitution method" of Cormen et al.].

=== April 28th–May 12th ===

Investigated how to generate running time constraints in Isabelle by recursive tactics on the structure of the IMP-Tailcall term, as in previous work on correctness. The issue to overcome is that we must work with a predicate of the form \exists c. \forall s. T_f_IMP s <= c * T_f (s "x"), which requires providing a single witness c for the linear factor. Previous work on correctness split the single goal recursively at sequences and conditionals into goals for each sub-term, but this approach doesn't work directly with an existential quantor: the '''same''' constant must be a witness in both subterms.

Instead of working directly with the existential, we can "provide" a witness up-front in the form of a schematic variable, and instantiate the schematic step-by-step. Thus we work with a predicate that bounds the running time by e.g. c * T_f (s "x"), without the existential quantor, and compute suitable constraints on the way down. Once we have computed a suitable c, it is obviously a witness for the existential quantor and we can close the goal.

This poses an additional challenge when previously verified functions are called, as the scheme devised above requires a concrete running time bound, not quantified with the existence of a constant. For this, we use Isabelle's LEAST operator to materialize the existential c from the running time of the auxiliary function's bound. (The obvious approach of "obtain"ing the constant with Isabelle's proof functionality does not work, as the schematic witness c of the function being analyzed can not depend on a value obtained later). We can then work with this (LEAST c. ...) * T_aux ... term just like any other bound.

After analyzing the term, we can instantiate and apply an induction hypothesis where applicable, this essentially corresponds to Cormen's "substitution method".

We are left with constraints on the constant c which must be solved, then c can be instantiated and the goals closed.

==== To Discuss ====

Should we investigate other approaches? For example, computing the running time up-front.

How can we automatically solve for suitable constants from the resulting constraints?

==== To do for next week ====

Examine more complex functions which:
* call functions with non-constant running time
* have preconditions on the well-formedness of their inputs
* use data types (this will only work to relate to HOL-Nat)

The condition of an if/else may depend on the input beyond just determining which case of the original function is being called, i.e. cannot necessarily be solved directly based on the inductive case being considered. Thus we cannot assume that we can solve the if/else if we introduce one into our timing constraint. The natural idea to use a maximum of both branches' running time won't work, consider for example the simple expression <code>if b then 1 else g y</code>; then, taking the maximum on the running time would result in a constraint like <code>max 3 ((LEAST c. ...) * T_g (s' "y")) <= ?c * T_f (s "x")</code>, which upon expanding <code>T_f</code> in the right-hand-side and taking the lower bound of the resulting if/else, would yield something like <code>max 3 ((LEAST c. ...) * T_g (s' "y")) <= ?c * 1</code>, which is obviously nonsense. Instead, we could try creating one inequality constraint for each branch.

Investigate the use of SMT-solvers or other automated solvers for the resulting inequality constraints.

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-14T23:46:58Z

Mxl:

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-14T21:17:22Z

Mxl: Summarize preliminary readings

== Progress ==

=== March 24th–April 28th ===

Read through [https://arxiv.org/pdf/2503.02975 Proof-Producing Translation of Functional Programs into a Time & Space Reasonable Model] which describes existing work on functional correctness.

Read [https://www.chargueraud.org/research/2018/bigo_credits/bigo_credits.pdf A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification] which develops a framework for interactive proofs of running time intended as part of an interface specification. The method first recursively descends through the function to calculate its running time up to recursive calls, e.g. <code>T_f(x) = 2 + T_f(x - 1)</code>. The user is asked to provide a "shape" of the running time bound they wish to specify, e.g. <code>a * x</code>, where <code>a</code> is left as a variable to solve for. Then induction is performed on the goal e.g. <code>2 + T_f(x - 1) <= a * x</code>, which through induction then becomes <code>2 + a * (x - 1) <= a * x</code>, thus providing a constraint on a suitable <code>a</code>. This is essentially the [https://enos.itcollege.ee/~japoia/algorithms/GT/Introduction_to_algorithms-3rd%20Edition.pdf#page=104 "substitution method" of Cormen et al.].

=== April 28th–May 12th ===

Investigated how to generate running time constraints in Isabelle by recursive tactics on the structure of the IMP-Tailcall term, as in previous work on correctness. The issue to overcome is that we must work with a predicate of the form \exists c. \forall s. T_f_IMP s <= c * T_f (s "x"), which requires providing a single witness c for the linear factor. Previous work on correctness split the single goal recursively at sequences and conditionals into goals for each sub-term, but this approach doesn't work directly with an existential quantor: the '''same''' constant must be a witness in both subterms.

Instead of working directly with the existential, we can "provide" a witness up-front in the form of a schematic variable, and instantiate the schematic step-by-step. Thus we work with a predicate that bounds the running time by e.g. c * T_f (s "x"), without the existential quantor, and compute suitable constraints on the way down. Once we have computed a suitable c, it is obviously a witness for the existential quantor and we can close the goal.

This poses an additional challenge when previously verified functions are called, as the scheme devised above requires a concrete running time bound, not quantified with the existence of a constant. For this, we use Isabelle's LEAST operator to materialize the existential c from the running time of the auxiliary function's bound. (The obvious approach of "obtain"ing the constant with Isabelle's proof functionality does not work, as the schematic witness c of the function being analyzed can not depend on a value obtained later). We can then work with this (LEAST c. ...) * T_aux ... term just like any other bound.

After analyzing the term, we can instantiate and apply an induction hypothesis where applicable, this essentially corresponds to Cormen's "substitution method".

We are left with constraints on the constant c which must be solved, then c can be instantiated and the goals closed.

==== To do for next week ====

Examine more complex functions which:
* call functions with non-constant running time
* have preconditions on the well-formedness of their inputs
* use data types (this will only work to relate to HOL-Nat)

==== To Discuss ====

Should we investigate other approaches? For example, computing the running time up-front.

How can we automatically solve for suitable constants from the resulting constraints?

Main Page

2025-05-14T18:22:24Z

Mxl:

File:TransTUM.svg

2025-05-14T18:20:58Z

Mxl:

== Summary ==
Font is Helvetica.

[[Category:Stickers]]

File:TransTUM.svg

2025-05-14T18:20:10Z

Mxl: Font is Helvetica.

== Summary ==
Font is Helvetica.

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-14T11:21:52Z

Mxl: Fixes

== Progress ==

=== April 14th–28th ===

=== April 14th–28th ===

=== April 28th–May 12th ===

Investigated how to generate running time constraints in Isabelle by recursive tactics on the structure of the IMP-Tailcall term, as in previous work on correctness. The issue to overcome is that we must work with a predicate of the form \exists c. \forall s. T_f_IMP s <= c * T_f (s "x"), which requires providing a single witness c for the linear factor. Previous work on correctness split the single goal recursively at sequences and conditionals into goals for each sub-term, but this approach doesn't work directly with an existential quantor: the '''same''' constant must be a witness in both subterms.

Instead of working directly with the existential, we can "provide" a witness up-front in the form of a schematic variable, and instantiate the schematic step-by-step. Thus we work with a predicate that bounds the running time by e.g. c * T_f (s "x"), without the existential quantor, and compute suitable constraints on the way down. Once we have computed a suitable c, it is obviously a witness for the existential quantor and we can close the goal.

This poses an additional challenge when previously verified functions are called, as the scheme devised above requires a concrete running time bound, not quantified with the existence of a constant. For this, we use Isabelle's LEAST operator to materialize the existential c from the running time of the auxiliary function's bound. (The obvious approach of "obtain"ing the constant with Isabelle's proof functionality does not work, as the schematic witness c of the function being analyzed can not depend on a value obtained later). We can then work with this (LEAST c. ...) * T_aux ... term just like any other bound.

After analyzing the term, we can instantiate and apply an induction hypothesis where applicable, this essentially corresponds to Cormen's "substitution method".

We are left with constraints on the constant c which must be solved, then c can be instantiated and the goals closed.

==== To do for next week ====

Examine more complex functions which:
* call functions with non-constant running time
* have preconditions on the well-formedness of their inputs
* use data types (this will only work to relate to HOL-Nat)

==== To Discuss ====

Should we investigate other approaches? For example, computing the running time up-front.

How can we automatically solve for suitable constants from the resulting constraints?

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-12T11:03:33Z

Mxl: April 28 - May 12

== Progress ==

=== April 14th–28th ===

=== April 14th–28th ===

=== April 28th–May 12th ===

Investigated how to generate running time constraints in Isabelle by recursive tactics on the structure of the IMP-Tailcall term, as in previous work on correctness. The issue to overcome is that we must work with a predicate of the form \exists c. \forall s. T_f_IMP s <= c * T_f (s "x"), which requires providing a single witness c for the linear factor. Previous work on correctness split the single goal recursively at sequences and conditionals into goals for each sub-term, but this approach doesn't work directly with an existential quantor: the '''same''' constant must be a witness in both subterms.

Instead of working directly with the existential, we can "provide" a witness up-front in the form of a schematic variable, and instantiate the schematic step-by-step. Thus we work with a predicate that bounds the running time by e.g. c * T_f (s "x"), without the existential quantor, and compute suitable constraints on the way down. Once we have computed a suitable c, it is obviously a witness for the existential quantor and we can close the goal.

This poses an additional challenge when previously verified functions are called, as the scheme devised above requires a concrete running time bound, not quantified with the existence of a consant. For this, we use Isabelle's LESS operator to materialize the existential c from the running time of the auxiliary function's bound. (The obvious approach of "obtain"ing the constant with Isabelle's proof functionality does not work, as the schenatic witness c of the function being analyzed can not depend on a value obtained later). We can then work with this (LESS c. ...) * T_aux ... term jist like any other bound.

After analyzing the term, we can instantiate and apply an induction hypothesis where applicable, this essentially corresponds to Cormen's "substitution method".

We are left with constraints on the constant c which must be solved, then c can be instantiated and the goals closed.

==== To do for next week ====

Examine more complex functions which:
* call functions with non-constant running time
* have preconditions on the well-formedness of their inputs
* use data types (this will only work to relate to HOL-Nat)

==== To Discuss ====

Should we investigate other approaches? For example, computing the running time up-front.

How can we automatically solve for suitable constants from the resulting constraints?

Translating Time Bounds of Functional Programs to a Deeply-Embedded Language (Thesis Project Tracking)

2025-05-12T10:39:02Z

Mxl: Created page with "== Progress == === April 14th–28th === === April 14th–28th === === April 28th–May 12th === ==== Recap Last Week ==== ==== To do for next week ==== ==== To Discuss ==== ==== Notes ===="

== Progress ==

=== April 14th–28th ===

=== April 14th–28th ===

=== April 28th–May 12th ===

==== Recap Last Week ====

==== To do for next week ====

==== To Discuss ====

==== Notes ====

Main Page

2025-04-27T13:16:33Z

Mxl:

Snapcast Server Setup

2025-04-27T13:16:10Z

Mxl: Created page with "Notes for '''setting up Snapcast''' (https://github.com/badaix/snapcast) for multi-device audio playback. == PipeWire as Player == To configure PipeWire as a player for Snapcast, create the file <code>10-snapcast-pipe-sink.conf</code> in <code>/etc/pipewire/pipewire.conf.d/</code> (or in <code>~/.config/pipewire/pipewire.conf.d/</code>): <nowiki>context.modules = [ { name = libpipewire-module-pipe-tunnel args = { tunnel.mode = sink..."

Notes for '''setting up Snapcast''' (https://github.com/badaix/snapcast) for multi-device audio playback.

== PipeWire as Player ==

To configure PipeWire as a player for Snapcast, create the file <code>10-snapcast-pipe-sink.conf</code> in <code>/etc/pipewire/pipewire.conf.d/</code> (or in <code>~/.config/pipewire/pipewire.conf.d/</code>):

<nowiki>context.modules = [
{
name = libpipewire-module-pipe-tunnel
args = {
tunnel.mode = sink
pipe.filename = "/tmp/snapfifo"
audio.format = S16LE
audio.rate = 48000
audio.channels = 2
audio.position = [ FL FR ]
stream.props = {
node.name = Snapcast
}
}
}
]</nowiki>

Then, restart PipeWire: <code>systemctl --user status wireplumber pipewire pipewire-pulse</code>.

== Resources ==

* PipeWire wiki on virtual devices: https://gitlab.freedesktop.org/pipewire/pipewire/-/wikis/Virtual-Devices#pipe-devices
* PipeWire documentation on pipe tunnel module: https://docs.pipewire.org/page_module_pipe_tunnel.html
* Snapcast docs on player setup: https://github.com/badaix/snapcast/blob/develop/doc/player_setup.md#pulseaudio

Main Page

2025-01-15T03:39:14Z

Mxl:

Category:System Configuration

2025-01-15T03:37:34Z

Mxl: Created page with "Best practices, references, and guides."

Best practices, references, and guides.

Managing and Adding APT Repositories

2025-01-15T03:36:43Z

Mxl:

Best practices, references, and helpers for '''managing custom APT repositories''' on Debian-derived systems.

The general advice is to put source lists in <code>/etc/apt/sources.list.d/</code> and keys in <code>/etc/apt/keyrings/</code>, referenced by <code>Signed-By</code> entries. The use of DEB822 Source Format is encouraged, as it simplifies managing repositories manually.

== Resources ==

* Debian Wiki's general instructions on third-party repositories: https://wiki.debian.org/DebianRepository/UseThirdParty
* Repolib's documentation of the DEB822 Source Format: https://repolib.readthedocs.io/en/latest/deb822-format.html
* Man page for APT <code>sources.list</code>: https://manpages.debian.org/unstable/apt/sources.list.5.en.html

== Converting list format to DEB822 ==

Given a line in the traditional list format <code><nowiki>deb [arch=arch1,arch2,... signed-by=/path/to/key] https://repo.url distribution component1 component2 ...</nowiki></code>, the corresponding DEB822 sources entry becomes:

<nowiki>Enabled: yes
Types: deb
URIs: https://repo.url
Suites: distribution ...
Components: component1 component2 ...
Architectures: arch1 arch2 ...
Signed-By: /path/to/key</nowiki>

Note: the <code>distribution</code> in the traditional entry becomes (one of) the <code>Suites</code> in the DEB822 entry.

== Signing Keys ==

Signing keys should be placed in <code>/etc/apt/keyrings/</code> and then by referenced by their file path in the <code>Signed-By</code> option in the source list entry.

Alternatively, keys can be ASCII-armored and referenced inline in a DEB822 source list:

<nowiki>Signed-By:
-----BEGIN PGP PUBLIC KEY BLOCK-----
.
mQINBGdCz4IBEACqA2UybPzUDw81EG0nXNUJ4Fk64pRkKqC5FwWUg7dPA4rtdMao
-----END PGP PUBLIC KEY BLOCK-----</nowiki>

Note that a single dot <code>.</code> must be used to replace the empty line, otherwise the empty line will split the file into multiple entries.


== Pinning ==


Add a <code>.pref</code> file in <code>/etc/apt/preferences.d/</code> to allow only specified packages to be installed by using pinning.

See "Standard pinning" in the linked Debian Wiki page.

For example, to disable packages from <code>contrib</code> and <code>non-free</code>, but allow installation of <code>libdvd-pkg</code>:

<nowiki>Explanation: Disable packages from debian contrib and non-free components by default
Package: *
Pin: release o=Debian,a=/^(stable|stable-updates|stable-security)$/,l=/^(Debian|Debian-Security)$/,c=/^(contrib|non-free)$/
Pin-Priority: -1

Explanation: Install libdvd-pkg from contrib
Package: libdvd-pkg
Pin: release o=Debian,a=stable,l=Debian,c=contrib
Pin-Priority: 500</nowiki>

Or alternatively <code>Pin: origin repo.url</code>

[[Category:System Configuration]]

Managing and Adding APT Repositories

2025-01-15T03:35:10Z

Mxl:

Managing and Adding APT Repositories

2025-01-15T03:33:08Z

Mxl: Created page with "Best practices, references, and helpers for '''managing custom APT repositories''' on Debian-derived systems. The general advice is to put source lists in <code>/etc/apt/sources.list.d/</code> and keys in <code>/etc/apt/keyrings/</code>, referenced by <code>Signed-By</code> entries. The use of DEB822 Source Format is encouraged, as it simplifies managing repositories manually. == Resources == * Debian Wiki's general instructions on third-party repositories: https://wi..."

Best practices, references, and helpers for '''managing custom APT repositories''' on Debian-derived systems.

The general advice is to put source lists in <code>/etc/apt/sources.list.d/</code> and keys in <code>/etc/apt/keyrings/</code>, referenced by <code>Signed-By</code> entries. The use of DEB822 Source Format is encouraged, as it simplifies managing repositories manually.

== Resources ==

* Debian Wiki's general instructions on third-party repositories: https://wiki.debian.org/DebianRepository/UseThirdParty
* Repolib's documentation of the DEB822 Source Format: https://repolib.readthedocs.io/en/latest/deb822-format.html
* Man page for APT <code>sources.list</code>: https://manpages.debian.org/unstable/apt/sources.list.5.en.html

== Converting list format to DEB822 ==

Given a line in the traditional list format <code><nowiki>deb [arch=arch1,arch2,... signed-by=/path/to/key] https://repo.url distribution component1 component2 ...</nowiki></code>, the corresponding DEB822 sources entry becomes:

<nowiki>Enabled: yes
Types: deb
URIs: https://repo.url
Suites: distribution ...
Components: component1 component2 ...
Architectures: arch1 arch2 ...
Signed-By: /path/to/key</nowiki>

Note: the <code>distribution</code> in the traditional entry becomes (one of) the <code>Suites</code> in the DEB822 entry.

== Signing Keys ==

Signing keys should be placed in <code>/etc/apt/keyrings/</code> and then by referenced by their file path in the <code>Signed-By</code> option in the source list entry.

Alternatively, keys can be ASCII-armored and referenced inline in a DEB822 source list:

<nowiki>Signed-By:
-----BEGIN PGP PUBLIC KEY BLOCK-----
.
mQINBGdCz4IBEACqA2UybPzUDw81EG0nXNUJ4Fk64pRkKqC5FwWUg7dPA4rtdMao
-----END PGP PUBLIC KEY BLOCK-----</nowiki>

Note that a single dot <code>.</code> must be used to replace the empty line, otherwise the empty line will split the file into multiple entries.





== Pinning ==

Add a <code>.pref</code> file in <code>/etc/apt/preferences.d/</code> to allow only specified packages to be installed by using pinning.

See "Standard pinning" in the linked Debian Wiki page.

For example, to disable packages from <code>contrib</code> and <code>non-free</code>, but allow installation of <code>libdvd-pkg</code>:

<nowiki>Explanation: Disable packages from debian contrib and non-free components by default
Package: *
Pin: release o=Debian,a=/^(stable|stable-updates|stable-security)$/,l=/^(Debian|Debian-Security)$/,c=/^(contrib|non-free)$/
Pin-Priority: -1

Explanation: Install libdvd-pkg from contrib
Package: libdvd-pkg
Pin: release o=Debian,a=stable,l=Debian,c=contrib
Pin-Priority: 500</nowiki>

Or alternatively <code>Pin: origin repo.url</code>

GE Rapid Clean II (seven-segment display font)

2025-01-06T03:04:19Z

Mxl:

[[File:GE Rapid Clean II Proof.svg|thumb|right|alt=Preview of font showing digits 0 through 9, alphabet, and a collection of words.|Preview of GE Rapid Clean II font]]

A digital recreation of the '''font''' used by the seven-segment display in the '''General Electric Rapid Clean II''' stove, which was installed in the kitchen at my mother's house.

First, the segment shapes were recreated in [https://solvespace.com SolveSpace]. The exported vector graphic was then imported into [https://fontforge.org/ FontForge] and split into "virtual" glyphs, which the real glyphs then reference.

== Download ==

* Latest FontForge export: [[Media:GE Rapid Clean II.otf|GE Rapid Clean II (OpenType font, .otf)]]

== Files ==

The design files (SolveSpace, FontForge) are in the repository [https://github.com/just-max/ge-rapid-clean-ii-font just-max/ge-rapid-clean-ii-font] on GitHub.

== Reference Images ==

<gallery>
GE Rapid Clean II (character 8).jpg|Close-up of all segments lit
GE Rapid Clean II (8-34).jpg|Showing the time 8:34
GE_Rapid_Clean_II_(9-09).jpg|Showing the time 9:09
</gallery>

[[Category:Fonts]]

File:GE Rapid Clean II (9-02).jpg

2025-01-06T03:03:57Z

Mxl: Mxl moved page File:GE Rapid Clean II (9-02).jpg to File:GE Rapid Clean II (9-09).jpg: Misspelled title

#REDIRECT [[File:GE Rapid Clean II (9-09).jpg]]

File:GE Rapid Clean II (9-09).jpg

2025-01-06T03:03:57Z

Mxl: Mxl moved page File:GE Rapid Clean II (9-02).jpg to File:GE Rapid Clean II (9-09).jpg: Misspelled title

GE Rapid Clean II (seven-segment display font)

2025-01-03T05:24:50Z

Mxl:

[[File:GE Rapid Clean II Proof.svg|thumb|right|alt=Preview of font showing digits 0 through 9, alphabet, and a collection of words.|Preview of GE Rapid Clean II font]]

A digital recreation of the '''font''' used by the seven-segment display in the '''General Electric Rapid Clean II''' stove, which was installed in the kitchen at my mother's house.

First, the segment shapes were recreated in [https://solvespace.com SolveSpace]. The exported vector graphic was then imported into [https://fontforge.org/ FontForge] and split into "virtual" glyphs, which the real glyphs then reference.

== Download ==

* Latest FontForge export: [[Media:GE Rapid Clean II.otf|GE Rapid Clean II (OpenType font, .otf)]]

== Files ==

The design files (SolveSpace, FontForge) are in the repository [https://github.com/just-max/ge-rapid-clean-ii-font just-max/ge-rapid-clean-ii-font] on GitHub.

== Reference Images ==

<gallery>
GE Rapid Clean II (character 8).jpg|Close-up of all segments lit
GE Rapid Clean II (8-34).jpg|Showing the time 8:34
GE_Rapid_Clean_II_(9-02).jpg|Showing the time 9:09
</gallery>

[[Category:Fonts]]