From 06e0550b3889c0ef105bf4b5fc4e6388d6d60607 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 20 May 2024 13:52:48 -0600 Subject: [PATCH] Shifts and law of monotonicity. --- .../plugins/obsidian-to-anki-plugin/data.json | 16 ++- notes/_journal/2024-05-20.md | 12 ++ notes/_journal/{ => 2024-05}/2024-05-19.md | 3 +- notes/encoding/integer.md | 2 +- notes/hashing/direct-addressing.md | 6 +- notes/programming/pred-trans.md | 45 +++++- notes/set/classes.md | 2 +- notes/set/index.md | 2 +- notes/x86-64/instructions.md | 130 ++++++++++++++++++ 9 files changed, 202 insertions(+), 16 deletions(-) create mode 100644 notes/_journal/2024-05-20.md rename notes/_journal/{ => 2024-05}/2024-05-19.md (82%) diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index a59e8a6..4a66852 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -260,7 +260,7 @@ "filesystems/cas.md": "d41c0d2e943adecbadd10a03fd1e4274", "git/objects.md": "8c1da67ac3f568624c3f9623eb2133e1", "git/index.md": "ca842957bda479dfa1170ae85f2f37b8", - "encoding/integer.md": "17387c74064bc738c4b4929ab37a0f56", + "encoding/integer.md": "ab0db8d48734867d42279fb2f2362d25", "_journal/2024-02-29.md": "f610f3caed659c1de3eed5f226cab508", "_journal/2024-02/2024-02-28.md": "7489377c014a2ff3c535d581961b5b82", "_journal/2024-03-01.md": "a532486279190b0c12954966cbf8c3fe", @@ -309,7 +309,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "85eef335afe27f8c0308c9ef5aa5d3ca", + "set/index.md": "b8165da42a81b5dc01b0a44ce365804e", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -328,7 +328,7 @@ "_journal/2024-03-22.md": "8da8cda07d3de74f7130981a05dce254", "_journal/2024-03/2024-03-21.md": "cd465f71800b080afa5c6bdc75bf9cd3", "x86-64/declarations.md": "75bc7857cf2207a40cd7f0ee056af2f2", - "x86-64/instructions.md": "6f18c3e6d01c80dc5ce6ec05c66ff627", + "x86-64/instructions.md": "a9fa4596009395c4161fd8601a669c6c", "git/refs.md": "e20c2c9b14ba6c2bd235416017c5c474", "set/trees.md": "c29347ec0ac2e8d5339514c869ecaedf", "_journal/2024-03-24.md": "1974cdb9fc42c3a8bebb8ac76d4b1fd6", @@ -432,7 +432,7 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b", - "programming/pred-trans.md": "9ea72ae99f4de83531b27f4621d21616", + "programming/pred-trans.md": "fe30f0cab01fd31640f0778bf983747f", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -446,12 +446,14 @@ "_journal/2024-05-17.md": "fb880d68077b655ede36d994554f3aba", "_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c", "_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", - "hashing/direct-addressing.md": "05c93ad0fe50092f2abff696888147d0", + "hashing/direct-addressing.md": "17daf22ed3dfcc465924a175e8f11ce3", "hashing/index.md": "340f8583eb51eaef011e3302bddb7ff8", - "set/classes.md": "a0bb2532284dea67bbfe7c1e3d714fd1", + "set/classes.md": "c933ca5dfebc3a0298e8ad948c6877a3", "_journal/2024-05-19.md": "fddd90fae08fab9bd83b0ef5d362c93a", "_journal/2024-05/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", - "_journal/2024-05/2024-05-17.md": "fb880d68077b655ede36d994554f3aba" + "_journal/2024-05/2024-05-17.md": "fb880d68077b655ede36d994554f3aba", + "_journal/2024-05-20.md": "350024abe16438d4cdd2ceaf95cb53c4", + "_journal/2024-05/2024-05-19.md": "fc14fc23d4ddca3628df7eec71a07e27" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-20.md b/notes/_journal/2024-05-20.md new file mode 100644 index 0000000..f32d174 --- /dev/null +++ b/notes/_journal/2024-05-20.md @@ -0,0 +1,12 @@ +--- +title: "2024-05-20" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Flashcards for x86-64 [[instructions#Shift Operations|shift operations]]. +* Flashcards on the [[pred-trans#Law of Monotonicity|Law of Monotonicity]]. \ No newline at end of file diff --git a/notes/_journal/2024-05-19.md b/notes/_journal/2024-05/2024-05-19.md similarity index 82% rename from notes/_journal/2024-05-19.md rename to notes/_journal/2024-05/2024-05-19.md index cd191bc..c9c0cc3 100644 --- a/notes/_journal/2024-05-19.md +++ b/notes/_journal/2024-05/2024-05-19.md @@ -8,4 +8,5 @@ title: "2024-05-19" - [ ] Go (1 Life & Death Problem) - [ ] Korean (Read 1 Story) -* Flashcards on x86-64 [[instructions#Unary Operations|unary operations]] and [[instructions#Binary Operations|binary operations]]. \ No newline at end of file +* Flashcards on x86-64 [[instructions#Unary Operations|unary operations]] and [[instructions#Binary Operations|binary operations]]. +* Struggled with getting Flutter up and running on NixOS. \ No newline at end of file diff --git a/notes/encoding/integer.md b/notes/encoding/integer.md index ad4fed8..46a74cb 100644 --- a/notes/encoding/integer.md +++ b/notes/encoding/integer.md @@ -1440,7 +1440,7 @@ END%% %%ANKI Basic What kinds of right shift operations are there? -Back: Logical and arithmetic +Back: Logical and arithmetic. Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. END%% diff --git a/notes/hashing/direct-addressing.md b/notes/hashing/direct-addressing.md index 3b10bff..f415cac 100644 --- a/notes/hashing/direct-addressing.md +++ b/notes/hashing/direct-addressing.md @@ -53,7 +53,7 @@ END%% %%ANKI Basic Write pseudocode to test membership of $x$ in direct-address table `T[0:m-1]`. -Back +Back: ```c bool membership(T, x) { return T[x.key] != NIL; @@ -66,7 +66,7 @@ END%% %%ANKI Basic Write pseudocode to insert $x$ into direct-address table `T[0:m-1]`. -Back +Back: ```c void insert(T, x) { T[x.key] = x; @@ -79,7 +79,7 @@ END%% %%ANKI Basic Write pseudocode to delete $x$ from direct-address table `T[0:m-1]`. -Back +Back: ```c void delete(T, x) { T[x.key] = NIL; diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index 22373f8..26e2ee6 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -297,6 +297,14 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon END%% +%%ANKI +Basic +In Gries's exposition, is the Law of the Excluded Miracle taken as an axiom or a theorem? +Back: An axiom. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + ### Distributivity of Conjunction Given command $S$ and predicates $Q$ and $R$, $$wp(S, Q \land R) = wp(S, Q) \land wp(S, R)$$ @@ -326,7 +334,7 @@ END%% %%ANKI Basic -Does $wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R)$ hold when $S$ is nondeterministic? +Is $wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R)$ true if $S$ is nondeterministic? Back: Yes. Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -334,7 +342,7 @@ END%% %%ANKI Basic -Does $wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R)$ hold when $S$ is nondeterministic? +Is $wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R)$ true if $S$ is nondeterministic? Back: Yes. Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -348,6 +356,39 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon END%% +### Law of Monotonicity + +Given command $S$ and predicates $Q$ and $R$, if $Q \Rightarrow R$, then $wp(S, Q) \Rightarrow wp(S, R)$. + +%%ANKI +What does the Law of Monotonicity state? +Back: Given command $S$ and predicates $Q$ and $R$, if $Q \Rightarrow R$, then $wp(S, Q) \Rightarrow wp(S, R)$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Cloze +Given command $S$, the Law of Monotonicity states that if {1:$Q$} $\Rightarrow$ {2:$R$}, then {2:$wp(S, Q)$} $\Rightarrow$ {1:$wp(S, R)$}. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In Gries's exposition, is the Law of Monotonicity taken as an axiom or a theorem? +Back: A theorem. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Is the Law of Monotonicity true if the relevant command is nondeterministic? +Back: Yes. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + ## Bibliography * Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file diff --git a/notes/set/classes.md b/notes/set/classes.md index aba5d4d..fbae150 100644 --- a/notes/set/classes.md +++ b/notes/set/classes.md @@ -30,7 +30,7 @@ END%% %%ANKI Basic What does the Zermelo-Fraenkel alternative say about classes? -Back: It gives it no ontological status at all. +Back: It gives them no ontological status at all. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% diff --git a/notes/set/index.md b/notes/set/index.md index 38bf1c8..aa4e669 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -418,7 +418,7 @@ For each formula $\_\_\_$ not containing $B$, the following is an axiom: $$\fora %%ANKI Basic What do the subset axioms state? -Back: For each formula $\phi$ not containing $B$, the following is an axiom: $$\forall t_1, \cdots, \forall t_k, \forall c, \exists B, \forall x, (x \in B \Leftrightarrow x \in c \land \_\_\_)$$ +Back: For each formula $\_\_\_$ not containing $B$, the following is an axiom: $$\forall t_1, \cdots, \forall t_k, \forall c, \exists B, \forall x, (x \in B \Leftrightarrow x \in c \land \_\_\_)$$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% diff --git a/notes/x86-64/instructions.md b/notes/x86-64/instructions.md index edd172a..ce2a62e 100644 --- a/notes/x86-64/instructions.md +++ b/notes/x86-64/instructions.md @@ -1069,6 +1069,136 @@ Tags: c17 END%% +### Shift Operations + +| Instruction | Operands | Effect | Description | +| ----------- | -------- | ------------ | ---------------------- | +| `sal[bwlq]` | k, D | D <- D << k | Left shift | +| `shl[bwlq]` | k, D | D <- D << k | Left shift | +| `sar[bwlq]` | k, D | D <- D >> k | Arithmetic right shift | +| `shr[bwlq]` | k, D | D <- D >>> k | Logical right shift | + +%%ANKI +Basic +What do instructions in the `SAL` instruction class do? +Back: Performs a left shift. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What do instructions in the `SHL` instruction class do? +Back: Performs a left shift. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Which instruction classes are related to left shifts? +Back: `SAL` and `SHL`. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + + +%%ANKI +Basic +Which instruction classes are related to right shifts? +Back: `SAR` and `SHR`. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What do instructions in the `SAR` instruction class do? +Back: Performs an arithmetic right shift. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What do instructions in the `SHR` instruction class do? +Back: Performs a logical right shift. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What distinguishes the `SAR` and `SHR` instruction classes? +Back: The former is arithmetic whereas the latter is logical. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What distinguishes the `SAL` and `SHL` instruction classes? +Back: N/A. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Which register are shift operations limited to? +Back: `%cl` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +How many lower-order bits of `%cl` does e.g. `salb` look at? +Back: $3$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What can the source of a shift operation be? +Back: An immediate or the `%cl` register. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What can the destination of a shift operation be? +Back: A register or memory location. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +How many lower-order bits of `%cl` does e.g. `salw` look at? +Back: $4$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +How many lower-order bits of `%cl` does e.g. `sall` look at? +Back: $5$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +How many lower-order bits of `%cl` does e.g. `salq` look at? +Back: $6$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + ## Bibliography * Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.